OAI/NumberTheory/Ostmann/Tree/SamePairHeldAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.quartetRatioValue_samePair_coordinates line 12
2. theorem OAI.Ostmann.samePair_held_coefficient_le line 29

   Source documentation

   The two held averages cost four; the moving square pullback costs two. All fixed unit parameters disappear from the resulting majorant.

   theorem samePair_held_coefficient_le {p : ℕ} [Fact p.Prime]
       (g h : ZMod p → ℂ) (y J K L : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
       (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ a : (ZMod p)ˣ,
         (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * ∑ b : (ZMod p)ˣ,
           ‖mellinCoefficient (fun r : (ZMod p)ˣ =>
             quartetRatioValue g h true true y (K * r ^ 2) (L * b ^ 2) (J * a ^ 2)) ρ‖ ^ 2) ≤
         8 * samePairMajorant (fieldPairCoefficientMoment g) (fieldPairMoment h) ρ y := by
   …

   Mentions: OAI.Ostmann.mellinCoefficient, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.samePairMajorant, OAI.Ostmann.fieldPairCoefficientMoment, OAI.Ostmann.fieldPairMoment