DensityFourier.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The normalized Fourier transform of the actual centered density

def OAI.Ostmann.centeredDensity line 12
def OAI.Ostmann.densityFourier line 15
theorem OAI.Ostmann.centeredDensity_abs_le line 18
theorem OAI.Ostmann.centeredDensity_sum line 28
theorem OAI.Ostmann.densityFourier_energy line 40
theorem OAI.Ostmann.densityFourier_energy_le line 47
theorem OAI.Ostmann.densityFourier_centered_zero line 55
theorem OAI.Ostmann.densityFourier_centered_energy line 62

theorem OAI.Ostmann.densityFourier_crt line 70

Source documentation

Probability-normalized CRT Fourier factorization remains exact after multiplication by the square root of the modulus.

theorem densityFourier_crt {m n : ℕ} [NeZero m] [NeZero n]
    (h : m.Coprime n) (f : ZMod m → ℂ) (g : ZMod n → ℂ) (u : ZMod (m * n)) :
    densityFourier (fun x => f ((ZMod.chineseRemainder h) x).1 *
      g ((ZMod.chineseRemainder h) x).2) u =
      densityFourier f ((n : ZMod m)⁻¹ * ((ZMod.chineseRemainder h) u).1) *
      densityFourier g ((m : ZMod n)⁻¹ * ((ZMod.chineseRemainder h) u).2) := by
…

Mentions: OAI.Ostmann.densityFourier

theorem OAI.Ostmann.densityFourier_crt_nonunit line 82

Source documentation

Each local centered Fourier transform vanishes at zero. The CRT product therefore vanishes at every nonunit of the composite modulus.

theorem densityFourier_crt_nonunit {m n : ℕ} [NeZero m] [NeZero n]
    (h : m.Coprime n) (f : ZMod m → ℂ) (g : ZMod n → ℂ)
    (hf : ∀ x, ¬IsUnit x → densityFourier f x = 0)
    (hg : ∀ x, ¬IsUnit x → densityFourier g x = 0)
    (u : ZMod (m * n)) (hu : ¬IsUnit u) :
    densityFourier (fun x => f ((ZMod.chineseRemainder h) x).1 *
      g ((ZMod.chineseRemainder h) x).2) u = 0 := by
…

Mentions: OAI.Ostmann.densityFourier

theorem OAI.Ostmann.densityFourier_centered_prime_nonunit line 106
Source documentation
This supplies the local hypotheses for every prime factor of L.
```
theorem densityFourier_centered_prime_nonunit {p : ℕ} [Fact p.Prime]
    (S : Finset (ZMod p)) (x : ZMod p) (hx : ¬IsUnit x) :
    densityFourier (fun y => (centeredDensity S y : ℂ)) x = 0 := by
…
```
Mentions: OAI.Ostmann.densityFourier, OAI.Ostmann.centeredDensity