theorem
LineSumDecomposition.norm_sq_lineSumFn_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)
:
L² bound for a sum of line indicators. Let ℒ be a finite collection of lines
in 𝔽_p × 𝔽_p, each of size p and pairwise intersecting in at most one point. For
f = ∑_{L ∈ ℒ} 1_L, the L² norm decomposes as f = f₀ + f_h with f₀ constant and
$\|f\|_2^2 = \|f_0\|_2^2 + \|f_h\|_2^2 \le |\mathcal L|^2 + |\mathcal L| \cdot p$.