GaussFourier.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Additive Fourier coefficients of multiplicative characters

The Gauss identity already proved in Mathlib gives the exact normalized squared modulus needed for the two-bad quartet estimate in Section 6.

theorem OAI.Ostmann.gaussSum_norm_sq line 18
theorem OAI.Ostmann.additiveFourier_mulChar_unit line 27

theorem OAI.Ostmann.additiveFourier_mulChar_norm_sq_unit line 44

Source documentation

The nonzero additive Fourier coefficients have squared modulus 1/p.

theorem additiveFourier_mulChar_norm_sq_unit {p : ℕ} [Fact p.Prime]
    (χ : MulChar (ZMod p) ℂ) (hχ : χ ≠ 1) (a : (ZMod p)ˣ) :
    ‖additiveFourier χ (a : ZMod p)‖ ^ 2 = (p : ℝ)⁻¹ := by
…

Mentions: OAI.Ostmann.additiveFourier

theorem OAI.Ostmann.additiveFourier_mulChar_zero line 54
Source documentation
A nonprincipal character has zero additive Fourier coefficient at zero.
```
theorem additiveFourier_mulChar_zero {p : ℕ} [Fact p.Prime]
    (χ : MulChar (ZMod p) ℂ) (hχ : χ ≠ 1) : additiveFourier χ 0 = 0 := by
…
```
Mentions: OAI.Ostmann.additiveFourier
theorem OAI.Ostmann.additiveFourier_mulChar line 58

theorem OAI.Ostmann.additiveFourier_pointwise_mul line 69

Source documentation

The Fourier transform exchanges pointwise multiplication and convolution.

theorem additiveFourier_pointwise_mul {p : ℕ} [NeZero p]
    (f g : ZMod p → ℂ) (a : ZMod p) :
    additiveFourier (fun x => f x * g x) a =
      ∑ b : ZMod p, additiveFourier f b * additiveFourier g (a - b) := by
…

Mentions: OAI.Ostmann.additiveFourier

theorem OAI.Ostmann.additiveFourier_mul_character line 97

Source documentation

Exact Gauss convolution formula, including the vanishing zero term.

theorem additiveFourier_mul_character {p : ℕ} [Fact p.Prime]
    (f : ZMod p → ℂ) (χ : MulChar (ZMod p) ℂ) (hχ : χ ≠ 1) (a : ZMod p) :
    additiveFourier (fun x => f x * χ x) a =
      ((p : ℂ)⁻¹ * gaussSum χ (ZMod.stdAddChar (N := p))) *
…

Mentions: OAI.Ostmann.additiveFourier