noncomputable def LineSumDecomposition.lineSumFn {p : ℕ} (ℒ : Finset (Finset (ZMod p × ZMod p))) (x : ZMod p × ZMod p) : ℝ

The line counting function $f(x) = \sum_{L \in \mathcal{L}} \mathbf{1}_L(x)$, counting how many lines from $\mathcal{L}$ pass through the point $x \in \mathbb{F}_p^2$.

noncomputable def LineSumDecomposition.lineSumConst {p : ℕ} (ℒ : Finset (Finset (ZMod p × ZMod p))) : ℝ

The constant (zero-frequency) part $f_0 = |\mathcal{L}| / p$ in the Fourier decomposition $f = f_0 + f_h$ of the line counting function.

noncomputable def LineSumDecomposition.lineSumHighFreq {p : ℕ} (ℒ : Finset (Finset (ZMod p × ZMod p))) (x : ZMod p × ZMod p) : ℝ

The high-frequency part $f_h = f - f_0$ of the line counting function, i.e. the mean-zero remainder after subtracting the constant component.

theorem LineSumDecomposition.decomposition {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) (x : ZMod p × ZMod p) : lineSumFn ℒ x = lineSumConst ℒ + lineSumHighFreq ℒ x

The decomposition $f(x) = f_0 + f_h(x)$: the line counting function equals the sum of its constant and high-frequency parts.

theorem LineSumDecomposition.lineSumHighFreq_eq_sum {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) (x : ZMod p × ZMod p) : lineSumHighFreq ℒ x = ∑ L ∈ ℒ, ((if x ∈ L then 1 else 0) - (↑p)⁻¹)

Rewrites $f_h(x) = \sum_{L \in \mathcal{L}} (\mathbf{1}_L(x) - p^{-1})$ as a sum of individual mean-zero indicator residues.

theorem LineSumDecomposition.sum_lineSumFn {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) (hlines : ∀ L ∈ ℒ, L.card = p) : ∑ x : ZMod p × ZMod p, lineSumFn ℒ x = ↑ℒ.card * ↑p

Total mass of the line counting function: $\sum_{x \in \mathbb{F}_p^2} f(x) = |\mathcal{L}| \cdot p$, since each line has exactly $p$ points.

theorem LineSumDecomposition.orthogonal_const_highFreq {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) (hlines : ∀ L ∈ ℒ, L.card = p) : ∑ x : ZMod p × ZMod p, lineSumConst ℒ * lineSumHighFreq ℒ x = 0

Orthogonality of the constant and high-frequency parts: $\sum_{x \in \mathbb{F}_p^2} f_0 \cdot f_h(x) = 0$.

theorem LineSumDecomposition.norm_sq_const_eq {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) : ∑ _x : ZMod p × ZMod p, lineSumConst ℒ ^ 2 = ↑ℒ.card ^ 2

$L^2$ norm of the constant part: $\sum_x f_0^2 = |\mathcal{L}|^2$.

theorem LineSumDecomposition.cross_term_eq {p : ℕ} [Fact (Nat.Prime p)] (L₁ L₂ : Finset (ZMod p × ZMod p)) (hL₁ : L₁.card = p) (hL₂ : L₂.card = p) : ∑ x : ZMod p × ZMod p, ((if x ∈ L₁ then 1 else 0) - (↑p)⁻¹) * ((if x ∈ L₂ then 1 else 0) - (↑p)⁻¹) = ↑(L₁ ∩ L₂).card - 1

Exact inner product of the mean-zero indicator residues of two lines $L_1, L_2$ (each of size $p$): $\sum_x (\mathbf{1}_{L_1}(x) - p^{-1})(\mathbf{1}_{L_2}(x) - p^{-1}) = |L_1 \cap L_2| - 1$.

theorem LineSumDecomposition.cross_term_nonpos {p : ℕ} [Fact (Nat.Prime p)] (L₁ L₂ : Finset (ZMod p × ZMod p)) (hL₁ : L₁.card = p) (hL₂ : L₂.card = p) (_hne : L₁ ≠ L₂) (hinter : (L₁ ∩ L₂).card ≤ 1) : ∑ x : ZMod p × ZMod p, ((if x ∈ L₁ then 1 else 0) - (↑p)⁻¹) * ((if x ∈ L₂ then 1 else 0) - (↑p)⁻¹) ≤ 0

If two distinct lines $L_1, L_2$ in $\mathbb{F}_p^2$ intersect in at most one point then the cross-term inner product of their mean-zero indicator residues is $\leq 0$.

theorem LineSumDecomposition.norm_sq_highFreq_le {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) (hlines : ∀ L ∈ ℒ, L.card = p) (hinter : ∀ L₁ ∈ ℒ, ∀ L₂ ∈ ℒ, L₁ ≠ L₂ → (L₁ ∩ L₂).card ≤ 1) : ∑ x : ZMod p × ZMod p, lineSumHighFreq ℒ x ^ 2 ≤ ↑ℒ.card * ↑p

$L^2$ bound on the high-frequency part: if every pair of distinct lines in $\mathcal{L}$ meets in at most one point, then $\sum_{x \in \mathbb{F}_p^2} f_h(x)^2 \leq |\mathcal{L}| \cdot p$.

theorem LineSumDecomposition.main_lemma_2F {p : ℕ} [Fact (Nat.Prime p)] (ℒ : Finset (Finset (ZMod p × ZMod p))) (hlines : ∀ L ∈ ℒ, L.card = p) (hinter : ∀ L₁ ∈ ℒ, ∀ L₂ ∈ ℒ, L₁ ≠ L₂ → (L₁ ∩ L₂).card ≤ 1) : (∀ (x : ZMod p × ZMod p), lineSumFn ℒ x = lineSumConst ℒ + lineSumHighFreq ℒ x) ∧ ∑ x : ZMod p × ZMod p, lineSumConst ℒ * lineSumHighFreq ℒ x = 0 ∧ ∑ _x : ZMod p × ZMod p, lineSumConst ℒ ^ 2 = ↑ℒ.card ^ 2 ∧ ∑ x : ZMod p × ZMod p, lineSumHighFreq ℒ x ^ 2 ≤ ↑ℒ.card * ↑p

Main Lemma 2F (finite field Fourier line decomposition). For a collection $\mathcal{L}$ of lines in $\mathbb{F}_p^2$ (each of size $p$, pairwise intersecting in at most one point), the line-counting function $f = \sum_{L \in \mathcal{L}} \mathbf{1}_L$ admits a decomposition $f = f_0 + f_h$ into a constant part $f_0 = |\mathcal{L}|/p$ and a mean-zero high-frequency part $f_h$ with: (i) orthogonality $\sum_x f_0 f_h = 0$, (ii) $\sum_x f_0^2 = |\mathcal{L}|^2$, and (iii) the $L^2$ bound $\sum_x f_h^2 \leq |\mathcal{L}| \cdot p$.