FriendlyQuartet.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The friendly quartet estimate

The exact held-parameter average is bounded by the uniform Mellin estimate on one side and total Fourier energy on the other side.

theorem OAI.Ostmann.left_friendly_fourier_sum_le line 20

theorem OAI.Ostmann.quartetParameterValue_left_friendly_bound line 58

Source documentation

A left-friendly source quartet has the quantitative src42 bound.

theorem quartetParameterValue_left_friendly_bound {p : ℕ} [Fact p.Prime]
    (g h : ZMod p → ℂ) (hg : g 0 = 0)
    (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
    (ε : ℝ) (hmixed : MixedFourierBound g ε) (S : ℝ)
    (hS : (∑ ψ : MulChar (ZMod p) ℂ, ∑ a : ZMod p,
      ‖additiveFourier (pairAutocorrelation h ψ) a‖ ^ 2) ≤ S)
    (right : Bool) (ν : MulChar (ZMod p) ℂ) :
    (p : ℝ)⁻¹ * (∑ y : ZMod p,
      (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ z : (ZMod p)ˣ,
        (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ *
          ∑ t : (ZMod p)ˣ, ‖quartetParameterValue g h true right ν y z t‖ ^ 2)) ≤
      (((p : ℝ) / ((p : ℝ) - 1)) * (ε ^ 4 + Real.sqrt (3 / (p : ℝ)))) * S := by
…

Mentions: OAI.Ostmann.MixedFourierBound, OAI.Ostmann.additiveFourier, OAI.Ostmann.pairAutocorrelation, OAI.Ostmann.quartetParameterValue