OAI/NumberTheory/Ostmann/Characters/QuartetFriendlyBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.rationalQuartet_friendly_held_bound line 13

   Source documentation

   The held-leaf coefficient bound applied to the actual recursive diagram, with no hypothesis asserting an unidentified local quartet estimate.

   theorem rationalQuartet_friendly_held_bound {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR P : (ZMod p)ˣ) (ρ : MulChar (ZMod p) ℂ) :
       (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ a : (ZMod p)ˣ,
         (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * ∑ b : (ZMod p)ˣ,
           ‖mellinCoefficient (fun (r : (ZMod p)ˣ) => rationalTreeAmplitude g D Q.tree XL XR
             ((false, true), (false, true))
             (((r⁻¹ : (ZMod p)ˣ), a), ((P * r / (a * b) : (ZMod p)ˣ), b))) ρ‖ ^ 2) ≤
         8 * ((p : ℝ) / (Fintype.card (ZMod p)ˣ : ℝ)) ^ 2 *
           crossPairMajorant g g true true ρ⁻¹
             (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.mellinCoefficient, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.crossPairMajorant, OAI.Ostmann.rationalTreeArgument