OAI/NumberTheory/Ostmann/Characters/QuartetCrossBound.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.crossLeftLeaves line 11
2. def OAI.Ostmann.crossRightLeaves line 14
3. def OAI.Ostmann.crossQuartetLeaves line 18
4. theorem OAI.Ostmann.crossLeftLeaves_product line 22
5. theorem OAI.Ostmann.crossRightLeaves_product line 27
6. theorem OAI.Ostmann.crossLeftLeaves_parameter line 33
7. theorem OAI.Ostmann.crossRightLeaves_parameter line 41
8. theorem OAI.Ostmann.crossQuartetLeaves_amplitude line 51

   Source documentation

   The product-fiber coordinates preserve both held leaves and expose the same inverse-square moving ratio for all four orientations.

   theorem crossQuartetLeaves_amplitude {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR P a b r : (ZMod p)ˣ) (left right : Bool) :
       rationalTreeAmplitude g D Q.tree XL XR ((false, true), (false, true))
         (crossQuartetLeaves left right P a b r) =
       quartetRatioValue (orientedPairBase g left) (orientedPairBase g right) left right
         (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P)
         ((if left then quartetLeftHeld D Q XL else quartetLeftBadHeld D Q XL XR P) * a ^ 2)
         ((if right then quartetRightHeld D Q XR else quartetRightBadHeld D Q XL XR P) * b ^ 2)
         (quartetMovingMultiplier Q XL XR P a * r ^ 2) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.crossQuartetLeaves, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.orientedPairBase, OAI.Ostmann.rationalTreeArgument, OAI.Ostmann.quartetLeftHeld, OAI.Ostmann.quartetLeftBadHeld, OAI.Ostmann.quartetRightHeld, OAI.Ostmann.quartetRightBadHeld, OAI.Ostmann.quartetMovingMultiplier

9. theorem OAI.Ostmann.rationalQuartet_cross_held_bound line 71

   Source documentation

   Every choice of one moving leaf in each pair has the already proved square-pullback majorant, directly on the actual recursive tree amplitude.

   theorem rationalQuartet_cross_held_bound {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR P : (ZMod p)ˣ) (left right : Bool) (ρ : 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))
               (crossQuartetLeaves left right P a b r)) ρ‖ ^ 2) ≤
       8 * ((p : ℝ) / (Fintype.card (ZMod p)ˣ : ℝ)) ^ 2 *
         crossPairMajorant (orientedPairBase g left) (orientedPairBase g right) left right ρ⁻¹
           (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P) := by
   …

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