GaussSums.lean

1 import Mathlib.NumberTheory.GaussSum
2 import Mathlib.Analysis.Complex.Basic
3 import Mathlib.Analysis.SpecialFunctions.Sqrt
4 import Mathlib.Tactic
5 
6 /-! Finite-field Gauss sums with the manuscript's sum over the unit group.
7 The additive character is explicitly required to be nontrivial. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperXI.GaussSums
11 open scoped Classical
12 
13 variable {k : Type*} [Field k] [Fintype k]
14 
15 /-- The literal sum over nonzero field elements, represented by units. -/
16 def unitSum (χ : MulChar k ℂ) (ψ : AddChar k ℂ) : ℂ :=
17   ∑ x : kˣ, χ x * ψ x
18 
19 /-- Mathlib's sum includes zero, where the extended multiplicative character vanishes. -/
20 theorem unitSum_eq_gaussSum (χ : MulChar k ℂ) (ψ : AddChar k ℂ) :
21     unitSum χ ψ = gaussSum χ ψ := by
22   classical
23   rw [gaussSum, Fintype.sum_eq_add_sum_subtype_ne _ 0]
24   simp only [MulChar.map_zero, zero_mul, zero_add]
25   exact Fintype.sum_equiv (unitsEquivNeZero (G₀ := k)) _ _ (fun _ => rfl)
26 
27 /-- The product with both characters inverted is the field cardinality. -/
28 theorem sum_mul_inverse {χ : MulChar k ℂ} {ψ : AddChar k ℂ}
29     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
30     unitSum χ ψ * unitSum χ⁻¹ ψ⁻¹ = Fintype.card k := by
31   simpa only [unitSum_eq_gaussSum] using
32     gaussSum_mul_gaussSum_eq_card hχ (AddChar.IsPrimitive.of_ne_one hψ)
33 
34 /-- Complex conjugation inverts both characters. -/
35 theorem conjugate_sum (χ : MulChar k ℂ) (ψ : AddChar k ℂ) :
36     star (unitSum χ ψ) = unitSum χ⁻¹ ψ⁻¹ := by
37   simpa only [unitSum_eq_gaussSum] using star_gaussSum_eq χ ψ
38 
39 /-- The squared norm is the cardinality, before taking the positive square root. -/
40 theorem norm_sq {χ : MulChar k ℂ} {ψ : AddChar k ℂ}
41     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
42     ‖unitSum χ ψ‖ ^ 2 = (Fintype.card k : ℝ) := by
43   have h := sum_mul_inverse hχ hψ
44   rw [← conjugate_sum] at h
45   have he : ((‖unitSum χ ψ‖ ^ 2 : ℝ) : ℂ) = Fintype.card k := by
46     simpa only [Complex.star_def, Complex.mul_conj', Complex.ofReal_pow] using h
47   exact_mod_cast he
48 
49 /-- Proposition 6.1: the magnitude of a nontrivial Gauss sum. -/
50 theorem magnitude {χ : MulChar k ℂ} {ψ : AddChar k ℂ}
51     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
52     ‖unitSum χ ψ‖ = Real.sqrt (Fintype.card k) := by
53   rw [← norm_sq hχ hψ, Real.sqrt_sq (norm_nonneg _)]
54 
55 /-- The product identity with the same additive character on both factors. -/
56 theorem sum_duality {χ : MulChar k ℂ} {ψ : AddChar k ℂ}
57     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
58     unitSum χ ψ * unitSum χ⁻¹ ψ = χ (-1) * Fintype.card k := by
59   simp only [unitSum_eq_gaussSum]
60   rw [← mul_gaussSum_inv_eq_gaussSum χ⁻¹, mul_left_comm,
61     gaussSum_mul_gaussSum_eq_card hχ (AddChar.IsPrimitive.of_ne_one hψ),
62     MulChar.inv_apply', inv_neg_one]
63 
64 /-- Definition 6.2: positive real square-root normalization. -/
65 def phase (χ : MulChar k ℂ) (ψ : AddChar k ℂ) : ℂ :=
66   unitSum χ ψ / (Real.sqrt (Fintype.card k) : ℂ)
67 
68 /-- The normalization is defined using a strictly positive real denominator. -/
69 theorem sqrt_card_pos : 0 < Real.sqrt (Fintype.card k : ℝ) := by
70   exact Real.sqrt_pos.2 (by exact_mod_cast Fintype.card_pos)
71 
72 /-- The asserted unit-circle property in Definition 6.2. -/
73 theorem phase_norm {χ : MulChar k ℂ} {ψ : AddChar k ℂ}
74     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) : ‖phase χ ψ‖ = 1 := by
75   rw [phase, norm_div, magnitude hχ hψ, Complex.norm_real,
76     Real.norm_eq_abs, abs_of_pos (sqrt_card_pos (k := k))]
77   exact div_self (ne_of_gt (sqrt_card_pos (k := k)))
78 
79 /-- Proposition 6.3: normalized Gauss phases are dual with sign χ(-1). -/
80 theorem phase_duality {χ : MulChar k ℂ} {ψ : AddChar k ℂ}
81     (hχ : χ ≠ 1) (hψ : ψ ≠ 1) :
82     phase χ ψ * phase χ⁻¹ ψ = χ (-1) := by
83   have hq : (Fintype.card k : ℂ) ≠ 0 := by
84     exact_mod_cast (ne_of_gt (Fintype.card_pos : 0 < Fintype.card k))
85   have hs : (Real.sqrt (Fintype.card k) : ℂ) ^ 2 = Fintype.card k := by
86     exact_mod_cast Real.sq_sqrt (show (0 : ℝ) ≤ Fintype.card k by positivity)
87   rw [phase, phase, div_mul_div_comm, ← pow_two, hs, sum_duality hχ hψ,
88     mul_div_cancel_right₀ _ hq]
89 
90 end PaperXI.GaussSums

Back to source controls