OAI/NumberTheory/Ostmann/Characters/QuartetSamePairBound.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.samePairLeftLeaves line 13
2. theorem OAI.Ostmann.samePair_left_product line 16
3. theorem OAI.Ostmann.samePair_total_product line 20
4. def OAI.Ostmann.samePairParentMultiplier line 24
5. theorem OAI.Ostmann.samePair_parent_ratio line 28
6. theorem OAI.Ostmann.samePairLeftLeaves_amplitude line 39

   Source documentation

   The held coordinates are the product and split of the right pair; the second left leaf is the moving Mellin coordinate.

   theorem samePairLeftLeaves_amplitude {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR P a b r : (ZMod p)ˣ) :
       rationalTreeAmplitude g D Q.tree XL XR ((false, true), (false, true))
         (samePairLeftLeaves P a b r) =
       quartetRatioValue g g true true
         (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P)
         (quartetLeftHeld D Q XL * r ^ 2) (quartetRightHeld D Q XR * b ^ 2)
         (samePairParentMultiplier Q XL XR P * a ^ 2) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.samePairLeftLeaves, OAI.Ostmann.quartetRatioValue, OAI.Ostmann.rationalTreeArgument, OAI.Ostmann.quartetLeftHeld, OAI.Ostmann.quartetRightHeld, OAI.Ostmann.samePairParentMultiplier

7. theorem OAI.Ostmann.rationalQuartet_samePair_left_held_bound line 54
8. def OAI.Ostmann.samePairRightLeaves line 67
9. theorem OAI.Ostmann.samePair_right_total_product line 70
10. def OAI.Ostmann.samePairRightParentMultiplier line 75
11. theorem OAI.Ostmann.samePair_right_parent_ratio line 79
12. theorem OAI.Ostmann.samePairRightLeaves_amplitude line 88
13. theorem OAI.Ostmann.rationalQuartet_samePair_right_held_bound line 103