QuartetSymmetry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Interchanging the two bottom pairs

Swapping the pairs inverts the quotient character and negates additive frequency. This supplies the right-friendly estimate from the left one.

def OAI.Ostmann.quartetFourierEnergy line 19
theorem OAI.Ostmann.quartetFourierEnergy_swap line 26
theorem OAI.Ostmann.right_friendly_fourier_sum_le line 58

theorem OAI.Ostmann.quartetParameterValue_right_friendly_bound line 72

Source documentation

The symmetric source estimate when the right pair is friendly.

theorem quartetParameterValue_right_friendly_bound {p : ℕ} [Fact p.Prime]
    (g h : ZMod p → ℂ) (hh : h 0 = 0)
    (henergy : (∑ x : ZMod p, ‖h x‖ ^ 2) ≤ (p : ℝ))
    (ε : ℝ) (hmixed : MixedFourierBound h ε) (S : ℝ)
    (hS : (∑ χ : MulChar (ZMod p) ℂ, ∑ a : ZMod p,
      ‖additiveFourier (pairAutocorrelation g χ) a‖ ^ 2) ≤ S)
    (left : 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 left true ν 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