DensityFourierBounds.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The two local Fourier bounds in the large-kernel correlation

theorem OAI.Ostmann.additiveFourier_twice line 13

theorem OAI.Ostmann.densityFourier_coefficient_le line 21

Source documentation

A prime occurring in exactly one of the divisors costs q^(-1/2).

theorem densityFourier_coefficient_le {q : ℕ} [NeZero q] (f : ZMod q → ℂ)
    (hf : ∀ x, ‖f x‖ ≤ 1) (a : ZMod q) :
    ‖additiveFourier (densityFourier f) a‖ ≤ (Real.sqrt (q : ℝ))⁻¹ := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.densityFourier

theorem OAI.Ostmann.densityFourier_unit_coefficient_le line 36

Source documentation

Unit dilations preserve the local coefficient bound.

theorem densityFourier_unit_coefficient_le {q : ℕ} [NeZero q]
    (f : ZMod q → ℂ) (hf : ∀ x, ‖f x‖ ≤ 1) (a : (ZMod q)ˣ) (u : ZMod q) :
    ‖additiveFourier (fun x => densityFourier f ((a : ZMod q) * x)) u‖ ≤ (Real.sqrt (q : ℝ))⁻¹ := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.densityFourier

theorem OAI.Ostmann.additiveFourier_cross_le_one line 43

Source documentation

At a common prime, the product costs only one, by Cauchy--Schwarz.

theorem additiveFourier_cross_le_one {q : ℕ} [NeZero q]
    (f g : ZMod q → ℂ) (hf : (∑ x, ‖f x‖ ^ 2) ≤ q)
    (hg : (∑ x, ‖g x‖ ^ 2) ≤ q) (u : ZMod q) :
    ‖additiveFourier (fun x => f x * conj (g x)) u‖ ≤ 1 := by
…

Mentions: OAI.Ostmann.additiveFourier

theorem OAI.Ostmann.additiveFourier_conj line 68
Source documentation
Conjugation reverses the Fourier frequency.
Distinct definitions of this name: OAI/NumberTheory/Ostmann/Characters/MixedFourier.lean:21 (different declaration text). Qualify references as OAI.Ostmann.additiveFourier_conj@path.
```
theorem additiveFourier_conj {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (a : ZMod q) :
    additiveFourier (fun x => conj (f x)) a = conj (additiveFourier f (-a)) := by
…
```
Mentions: OAI.Ostmann.additiveFourier

theorem OAI.Ostmann.unit_dilation_energy line 74

Source documentation

Unit dilations preserve the counting-measure energy.

theorem unit_dilation_energy {q : ℕ} [NeZero q] (f : ZMod q → ℂ) (a : (ZMod q)ˣ) :
    (∑ x : ZMod q, ‖f ((a : ZMod q) * x)‖ ^ 2) = ∑ x : ZMod q, ‖f x‖ ^ 2 :=
…

theorem OAI.Ostmann.densityFourier_unit_cross_le_one line 79

Source documentation

The common-prime factor of the original density correlation.

theorem densityFourier_unit_cross_le_one {q : ℕ} [NeZero q]
    (f g : ZMod q → ℂ) (hf : ∀ x, ‖f x‖ ≤ 1) (hg : ∀ x, ‖g x‖ ≤ 1)
    (a b : (ZMod q)ˣ) (u : ZMod q) :
    ‖additiveFourier (fun x => densityFourier f ((a : ZMod q) * x) *
      conj (densityFourier g ((b : ZMod q) * x))) u‖ ≤ 1 := by
…

Mentions: OAI.Ostmann.additiveFourier, OAI.Ostmann.densityFourier