Documentation

GQ2.SectionEight.Fourier

§8: the finite Fourier and Gauss engines (Lemmas 8.4, 8.5) #

The sign calculus over 𝔽₂ and the two multiplied-out integer identities it powers: Lemma 8.4 (Fourier inversion, display (125)) and Lemma 8.5 (the constrained quadratic Gauss transform, display (126)).

The sign calculus over 𝔽₂ #

(−1)^{(·).val} : ZMod 2 → ℤ is the additive character; the two orthogonality relations (over the group and over its dual) are the single lemma sum_sign_eq_zero below.

source
def GQ2.SectionEight.sign (s : ZMod 2) :
ℤ

The sign (−1)^s of s : 𝔽₂, as an integer.

Equations
Instances For
    source
    @[simp]
    theorem GQ2.SectionEight.sign_zero :
    sign 0 = 1
    source
    @[simp]
    theorem GQ2.SectionEight.sign_one :
    sign 1 = -1
    source
    theorem GQ2.SectionEight.sign_add (s t : ZMod 2) :
    sign (s + t) = sign s * sign t
    source
    theorem GQ2.SectionEight.one_add_sign (u : ZMod 2) :
    1 + sign u = if u = 0 then 2 else 0

    1 + (−1)^u = 2·[u = 0].

    source
    theorem GQ2.SectionEight.sum_sign_eq_zero {A : Type u_1} [AddCommGroup A] [Finite A] (ψ : A → ZMod 2) (hadd : ∀ (a b : A), ψ (a + b) = ψ a + ψ b) (hne : ¬∀ (a : A), ψ a = 0) :
    ∑ᶠ (a : A), sign (ψ a) = 0

    Character orthogonality: a nonzero additive functional to 𝔽₂ on a finite abelian group has sign-sum zero. (Both orthogonality relations of §8 — over the group for (126), over the dual for (125) — are instances.)

    source
    theorem GQ2.SectionEight.sign_eq_indicator (u : ZMod 2) :
    sign u = (if u = 0 then 2 else 0) - 1

    The sign is the ±1-indicator: sign u = 2·[u = 0] − 1.

    source
    theorem GQ2.SectionEight.sum_dual_sign {W : Type u_1} [AddCommGroup W] [Module (ZMod 2) W] [Finite W] (w : W) :
    ∑ᶠ (φ : Module.Dual (ZMod 2) W), sign (φ w) = if w = 0 then ↑(Nat.card (Module.Dual (ZMod 2) W)) else 0

    Orthogonality over the dual, summed form: Σ_{φ ∈ W^∨} (−1)^{φ w} = |W^∨|·[w = 0].

    Lemma 8.4: Fourier inversion (display (125)) #

    source
    theorem GQ2.SectionEight.lemma_8_4 {X : Type u_1} {W : Type u_2} [Finite X] [AddCommGroup W] [Module (ZMod 2) W] [Finite W] (o : X → W) :
    ↑(Nat.card (Module.Dual (ZMod 2) W)) * ↑(Nat.card { x : X // o x = 0 }) = ∑ᶠ (φ : Module.Dual (ZMod 2) W), (2 * ↑(Nat.card { x : X // φ (o x) = 0 }) - ↑(Nat.card X))

    Lemma 8.4 (Fourier inversion, eq. (125)), multiplied-out integer form: for a finite 𝔽₂-obstruction space W, an obstruction assignment o : X → W on a finite index set, and m_φ = #{x ∣ φ(o(x)) = 0}, |W^∨| · #{x ∣ o(x) = 0} = Σ_{φ ∈ W^∨} (2 m_φ − |X|). (Paper form: divide by |D|, D = W^∨.) Proved — the 𝔽₂-character engine of the final R-lifting stage (136).

    Lemma 8.5: the constrained quadratic Gauss transform (display (126)) #

    source
    noncomputable def GQ2.SectionEight.gaussSum {W : Type u_1} [Finite W] (Q : W → ZMod 2) :
    ℤ

    The Gauss sum G(Q) = Σ_{x ∈ W} (−1)^{Q(x)} of an 𝔽₂-valued form.

    Equations
    Instances For
      source
      theorem GQ2.SectionEight.add_self_fp2 {M : Type u_1} [AddCommGroup M] [Module (ZMod 2) M] (m : M) :
      m + m = 0

      In an 𝔽₂-module, every element is self-inverse.

      source
      theorem GQ2.SectionEight.lemma_8_5 {W : Type u_1} {E : Type u_2} [AddCommGroup W] [Module (ZMod 2) W] [Finite W] [AddCommGroup E] [Module (ZMod 2) E] [Finite E] (L : W →ₗ[ZMod 2] E) (hL : Function.Surjective ⇑L) (Q : W → ZMod 2) (a : Module.Dual (ZMod 2) E → W) (ha : ∀ (χ : Module.Dual (ZMod 2) E) (x : W), QuadraticFp2.polar Q (a χ) x = χ (L x)) (κ : E) (ε : ZMod 2) :
      2 * ↑(Nat.card (Module.Dual (ZMod 2) E)) * ↑(Nat.card { x : W // L x = κ ∧ Q x = ε }) = ↑(Nat.card W) + gaussSum Q * ∑ᶠ (χ : Module.Dual (ZMod 2) E), sign (χ κ + ε + Q (a χ))

      Lemma 8.5 (constrained quadratic Gauss transform, eq. (126)), multiplied-out form: for finite 𝔽₂-spaces W, E, a surjective linear L : W ↠ E, a form Q : W → 𝔽₂ with polar form B_Q, and data a : E^∨ → W with the paper's defining property B_Q(a_χ, x) = χ(L x) (the paper produces a_χ from nonsingularity of Q; the identity needs only the property), the constrained count N(κ,ε) = #{x ∣ Lx = κ, Q(x) = ε} satisfies 2|E^∨| · N(κ,ε) = |W| + G(Q) · Σ_{χ ∈ E^∨} (−1)^{χ(κ)+ε+Q(a_χ)}. (|E^∨| = |E| for finite 𝔽₂-spaces, giving the paper's 1/(2|E|)-form.) Proved — the affine-fibre engine of the (140)-clause of Prop 8.9.