def FourierBound.piSlope {F : Type u_1} [Ring F] (θ : F) : F × F → F

Projection of (x, y) ∈ F × F onto the line of slope θ: π_θ(x, y) = x + θ y. This is the standard projection used throughout finite-field projection theory.

theorem FourierBound.piSlope_pair_injective {F : Type u_1} [Field F] {θ₁ θ₂ : F} (hne : θ₁ ≠ θ₂) : Function.Injective fun (p : F × F) => (piSlope θ₁ p, piSlope θ₂ p)

For two distinct slopes θ₁ ≠ θ₂, the pair of projections p ↦ (π_{θ₁}(p), π_{θ₂}(p)) is injective on F². This is the algebraic fact that two non-parallel lines uniquely determine a point.

theorem FourierBound.piSlope_pair_bijective {F : Type u_1} [Field F] [Fintype F] {θ₁ θ₂ : F} (hne : θ₁ ≠ θ₂) : Function.Bijective fun (p : F × F) => (piSlope θ₁ p, piSlope θ₂ p)

For distinct slopes, the pair-of-projections map F × F → F × F is a bijection; follows from piSlope_pair_injective and equal cardinalities.

theorem FourierBound.joint_preimage_card {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {θ₁ θ₂ : F} (hne : θ₁ ≠ θ₂) (A₁ A₂ : Finset F) : {p : F × F | piSlope θ₁ p ∈ A₁ ∧ piSlope θ₂ p ∈ A₂}.card = A₁.card * A₂.card

Counts the number of points p ∈ F² whose two projections π_{θ₁}(p) and π_{θ₂}(p) lie in given sets A₁ and A₂. For distinct slopes, the bijectivity of the joint projection gives |{p : π_{θ₁}(p) ∈ A₁ ∧ π_{θ₂}(p) ∈ A₂}| = |A₁| · |A₂|.

theorem FourierBound.piSlope_fiber_card {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (θ b : F) : {p : F × F | piSlope θ p = b}.card = Fintype.card F

Every fiber of the projection π_θ : F² → F has cardinality |F| = q: the line π_θ^{-1}(b) contains exactly |F| points.

theorem FourierBound.fourier_numerical (Xc Dc S q : ℕ) (hS_le : 2 * S ≤ q) (hq_pos : 0 < q) (hDc_pos : 0 < Dc) (hvar : Xc * Dc * Dc * (q - S) * (q - S) ≤ S * Dc * q * q * q) : Dc * Xc ≤ 4 * S * q

Numerical bookkeeping step in the Fourier proof of Theorem 2.3. Given the variance bound |X| · |D|² · (q - S)² ≤ S · |D| · q³ and 2S ≤ q, deduce the projection bound |D| · |X| ≤ 4 S q. The factor of 4 comes from q ≤ 2(q - S).

theorem FourierBound.preimage_card_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (θ : F) (A : Finset F) : {x : F × F | piSlope θ x ∈ A}.card = Fintype.card F * A.card

The preimage π_θ^{-1}(A) ⊂ F² of a set A ⊂ F of "values" under the direction-θ projection has cardinality |F| · |A| = q · |A|. Obtained by disjointly unioning the fibers π_θ^{-1}(b) for b ∈ A.

theorem FourierBound.variance_bound {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (X : Finset (F × F)) (D : Finset F) (hX : X.Nonempty) (M : ℕ) (hM_def : M = ∑ θ ∈ D, (Finset.image (piSlope θ) X).card) (hM_le_qD : M ≤ Fintype.card F * D.card) : X.card * (Fintype.card F * D.card - M) * (Fintype.card F * D.card - M) ≤ Fintype.card F * Fintype.card F * Fintype.card F * M

Variance / second moment bound underlying the Fourier proof of Theorem 2.3. Let f(x) = |{θ ∈ D : π_θ(x) ∈ π_θ(X)}| and M = ∑_{θ ∈ D} |π_θ(X)|. Then $$|X| \cdot (q|D| - M)^2 \;\le\; q^3 \, M,$$ a consequence of the first and second moments of f over F² via Cauchy-Schwarz (equivalently, an L² orthogonality / Parseval-type computation).

theorem FourierBound.fourier_bound_finite_field {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (X : Finset (F × F)) (D : Finset F) (S : ℕ) (hS : ∀ θ ∈ D, (Finset.image (piSlope θ) X).card ≤ S) (hS_le : 2 * S ≤ Fintype.card F) (hX : X.Nonempty) (hD : D.Nonempty) : D.card * X.card ≤ 4 * S * Fintype.card F

Theorem 2.3 (Fourier / orthogonality projection bound over 𝔽_q). If X ⊂ F², D ⊂ F, and S = max_{θ ∈ D} |π_θ(X)| satisfies 2S ≤ q = |F|, then $$|D| \;\lesssim\; \frac{S q}{|X|},$$ explicitly |D| · |X| ≤ 4 S q. Proved by combining the variance bound |X|(q|D| - M)² ≤ q³ M (with M = ∑_{θ ∈ D}|π_θ(X)| ≤ S|D|) with the numerical inequality q ≤ 2(q - S).