ProgressionFourier.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Additive Fourier resolution of every progression class

The coefficient mass is exactly one. There is no invertibility assumption on the class, and no frequency supremum is put inside an integral.

theorem OAI.TwoPointCorrelations.additiveCharacter_add line 17
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ProgressionFourier.lean:17 (same declaration text).
theorem OAI.TwoPointCorrelations.stdAddChar_nat_mul line 25
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ProgressionFourier.lean:25 (same declaration text).
theorem OAI.TwoPointCorrelations.zmod_indicator_fourier line 34
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ProgressionFourier.lean:34 (same declaration text).
theorem OAI.TwoPointCorrelations.progression_fourier_identity line 44
Also declared: OAI/NumberTheory/TwoPoint/Bounds/ProgressionFourier.lean:44 (same declaration text).

theorem OAI.TwoPointCorrelations.norm_progression_fourier_le line 75

Source documentation

The progression mask averages l shifted frequencies with total absolute coefficient mass one.

Also declared: OAI/NumberTheory/TwoPoint/Bounds/ProgressionFourier.lean:75 (same declaration text).

theorem norm_progression_fourier_le (S : Finset ℕ) (v : ℕ → ℂ)
    (l : ℕ) [NeZero l] (b : ZMod l) (α : ℝ) :
    ‖∑ n ∈ S, if (n : ZMod l) = b then v n * additiveCharacter α n else 0‖ ≤
      (l : ℝ)⁻¹ * ∑ a : ZMod l,
        ‖∑ n ∈ S, v n * additiveCharacter (α + (a.val : ℝ) / l) n‖ := by
…

Mentions: OAI.TwoPointCorrelations.additiveCharacter