OAI/NumberTheory/Ostmann/Characters/QuartetLocalBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.Ostmann.QuartetMovingCase line 14
2. def OAI.Ostmann.quartetMovingLeaves line 19
3. def OAI.Ostmann.quartetMovingMajorant line 26
4. theorem OAI.Ostmann.quartetMovingMajorant_nonneg line 39
5. theorem OAI.Ostmann.quartetMoving_coefficient_le line 54

   Source documentation

   No local-diagram estimate is assumed: this assembles the six previously proved coefficient bounds on the actual rational-tree value.

   theorem quartetMoving_coefficient_le {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR P : (ZMod p)ˣ) (cL cR : Bool) (choice : QuartetMovingCase)
       (ρ : 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 ((cL, !cL), (cR, !cR))
               (quartetMovingLeaves choice P a b r)) ρ‖ ^ 2) ≤
         quartetMovingMajorant g cL cR choice ρ
           (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.QuartetMovingCase, OAI.Ostmann.mellinCoefficient, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.quartetMovingLeaves, OAI.Ostmann.quartetMovingMajorant, OAI.Ostmann.rationalTreeArgument

6. def OAI.Ostmann.quartetLocalMeanError line 70
7. theorem OAI.Ostmann.quartetMovingMajorant_mean_le line 75
8. theorem OAI.Ostmann.quartetMovingMajorant_total_mean_le line 113