noncomputable def MainLemmaFF.lineIndicator {F : Type u_1} [DecidableEq F] (L : Finset (F × F)) (x : F × F) : ℝ

The indicator function $\mathbf{1}_L(x)$ of a line $L \subseteq \mathbb{F}_q^2$, valued in $\mathbb{R}$.

noncomputable def MainLemmaFF.lineHighFreq {F : Type u_1} [Fintype F] [DecidableEq F] (L : Finset (F × F)) (x : F × F) : ℝ

The mean-zero indicator residue $\mathbf{1}_L(x) - 1/q$ of a single line $L \subseteq \mathbb{F}_q^2$ (with $q = |\mathbb{F}|$).

noncomputable def MainLemmaFF.lineSumFunc {F : Type u_1} [DecidableEq F] (ℒ : Finset (Finset (F × F))) (x : F × F) : ℝ

The line counting function $L(x) = \sum_{L \in \mathcal{L}} \mathbf{1}_L(x)$ on $\mathbb{F}_q^2$.

noncomputable def MainLemmaFF.constPart {F : Type u_1} [Fintype F] (ℒ : Finset (Finset (F × F))) (_x : F × F) : ℝ

The constant (zero-frequency) part $L_0 = |\mathcal{L}| / q$ of the line counting function (independent of x).

noncomputable def MainLemmaFF.highFreqPart {F : Type u_1} [Fintype F] [DecidableEq F] (ℒ : Finset (Finset (F × F))) (x : F × F) : ℝ

The high-frequency part $L_h(x) = \sum_{L \in \mathcal{L}} (\mathbf{1}_L(x) - 1/q)$ of the line counting function.

theorem MainLemmaFF.decomposition {F : Type u_1} [Fintype F] [DecidableEq F] (ℒ : Finset (Finset (F × F))) (x : F × F) : lineSumFunc ℒ x = constPart ℒ x + highFreqPart ℒ x

The line-counting function splits as $L(x) = L_0 + L_h(x)$.

theorem MainLemmaFF.l2_norm_constPart {F : Type u_1} [Field F] [Fintype F] (ℒ : Finset (Finset (F × F))) : ∑ x : F × F, constPart ℒ x ^ 2 = ↑ℒ.card ^ 2

$L^2$ norm of the constant part: $\sum_{x \in \mathbb{F}_q^2} L_0^2 = |\mathcal{L}|^2$.

theorem MainLemmaFF.innerProduct_lineHighFreq_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (L₁ L₂ : Finset (F × F)) (hL₁ : L₁.card = Fintype.card F) (hL₂ : L₂.card = Fintype.card F) : ∑ x : F × F, lineHighFreq L₁ x * lineHighFreq L₂ x = ↑(L₁ ∩ L₂).card - 1

Exact inner product formula for two line residues on $\mathbb{F}_q^2$ (each line of size $q$): $\sum_x (\mathbf{1}_{L_1} - 1/q)(\mathbf{1}_{L_2} - 1/q) = |L_1 \cap L_2| - 1$.

theorem MainLemmaFF.l2_bound_highFreqPart {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (ℒ : Finset (Finset (F × F))) (hsize : ∀ L ∈ ℒ, L.card = Fintype.card F) (hinter : ∀ L₁ ∈ ℒ, ∀ L₂ ∈ ℒ, L₁ ≠ L₂ → (L₁ ∩ L₂).card = 1) : ∑ x : F × F, highFreqPart ℒ x ^ 2 = ↑ℒ.card * (↑(Fintype.card F) - 1)

Exact $L^2$ norm of the high-frequency part: when every pair of distinct lines in $\mathcal{L}$ meets in exactly one point, $\sum_x L_h(x)^2 = |\mathcal{L}| \cdot (q - 1)$.

theorem MainLemmaFF.l2_bound_highFreqPart_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (ℒ : Finset (Finset (F × F))) (hsize : ∀ L ∈ ℒ, L.card = Fintype.card F) (hinter : ∀ L₁ ∈ ℒ, ∀ L₂ ∈ ℒ, L₁ ≠ L₂ → (L₁ ∩ L₂).card = 1) : ∑ x : F × F, highFreqPart ℒ x ^ 2 ≤ ↑ℒ.card * ↑(Fintype.card F)

Looser $L^2$ bound on the high-frequency part: $\sum_x L_h(x)^2 \leq |\mathcal{L}| \cdot q$.

theorem MainLemmaFF.constPart_const {F : Type u_1} [Fintype F] (ℒ : Finset (Finset (F × F))) (x y : F × F) : constPart ℒ x = constPart ℒ y

The constant part $L_0$ is genuinely constant: $L_0(x) = L_0(y)$ for all $x, y$.

theorem MainLemmaFF.sum_highFreqPart_eq_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (ℒ : Finset (Finset (F × F))) (hsize : ∀ L ∈ ℒ, L.card = Fintype.card F) : ∑ x : F × F, highFreqPart ℒ x = 0

The high-frequency part has total mass zero: $\sum_{x \in \mathbb{F}_q^2} L_h(x) = 0$.

theorem MainLemmaFF.main_lemma_ff {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (ℒ : Finset (Finset (F × F))) (hsize : ∀ L ∈ ℒ, L.card = Fintype.card F) (hinter : ∀ L₁ ∈ ℒ, ∀ L₂ ∈ ℒ, L₁ ≠ L₂ → (L₁ ∩ L₂).card = 1) : (∀ (x : F × F), lineSumFunc ℒ x = constPart ℒ x + highFreqPart ℒ x) ∧ (∀ (x y : F × F), constPart ℒ x = constPart ℒ y) ∧ ∑ x : F × F, highFreqPart ℒ x = 0 ∧ ∑ x : F × F, constPart ℒ x ^ 2 = ↑ℒ.card ^ 2 ∧ ∑ x : F × F, highFreqPart ℒ x ^ 2 = ↑ℒ.card * (↑(Fintype.card F) - 1) ∧ ∑ x : F × F, highFreqPart ℒ x ^ 2 ≤ ↑ℒ.card * ↑(Fintype.card F)

Main Lemma in finite field. Let $\mathcal{L}$ be a collection of lines in $\mathbb{F}_q^2$ (each of cardinality $q$, with any two distinct lines meeting in exactly one point) and let $L(x) = \sum_{L \in \mathcal{L}} \mathbf{1}_L(x)$. Then $L = L_0 + L_h$ with $L_0$ constant and $L_h$ mean-zero, satisfying (i) $\sum_x L_h = 0$, (ii) $\sum_x L_0^2 = |\mathcal{L}|^2$, (iii) $\sum_x L_h^2 = |\mathcal{L}|(q - 1)$, and consequently $\sum_x L_h^2 \leq |\mathcal{L}| q$.