AdditiveFourier.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Probability-normalized additive Fourier identities

These finite identities provide the normalization used in Section 6. Fourier inversion is the library's discrete Fourier inversion theorem.

theorem OAI.Ostmann.stdAddChar_conj line 18
def OAI.Ostmann.additiveFourier line 24
Source documentation
The additive Fourier transform with probability normalization.
```
noncomputable def additiveFourier {p : ℕ} [NeZero p]
    (f : ZMod p → ℂ) (a : ZMod p) : ℂ :=
…
```
theorem OAI.Ostmann.additiveFourier_apply line 28
theorem OAI.Ostmann.additiveFourier_inversion line 33
theorem OAI.Ostmann.additiveFourier_conjugate_coefficient line 48
theorem OAI.Ostmann.additiveFourier_energy line 60

theorem OAI.Ostmann.additiveFourier_parseval line 91

Source documentation

Additive Parseval with the manuscript's probability convention.

theorem additiveFourier_parseval {p : ℕ} [NeZero p] (f : ZMod p → ℂ) :
    (∑ a : ZMod p, ‖additiveFourier f a‖ ^ 2) =
      (p : ℝ)⁻¹ * ∑ x : ZMod p, ‖f x‖ ^ 2 := by
…

Mentions: OAI.Ostmann.additiveFourier

theorem OAI.Ostmann.additiveFourier_sub line 98
theorem OAI.Ostmann.additiveFourier_const line 103