OAI/NumberTheory/Ostmann/Characters/MixedQuartetBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.crossQuartetLeaves_amplitude_conjugation line 14
2. theorem OAI.Ostmann.rationalQuartet_cross_held_bound_conjugation line 32
3. theorem OAI.Ostmann.samePairLeftLeaves_amplitude_conjugation line 48
4. theorem OAI.Ostmann.rationalQuartet_samePair_left_held_bound_conjugation line 64
5. theorem OAI.Ostmann.samePairRightLeaves_amplitude_conjugation line 78
6. theorem OAI.Ostmann.rationalQuartet_samePair_right_held_bound_conjugation line 94
7. theorem OAI.Ostmann.rationalQuartet_fiber_secondMoment_le_any_conjugation line 109

   Source documentation

   Squared magnitude is independent even of the opposite-sibling restriction.

   theorem rationalQuartet_fiber_secondMoment_le_any_conjugation {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (XL XR P : (ZMod p)ˣ) (c : TreeLeafTuple Bool 2) :
       (Fintype.card (TreeLeafFiber (ZMod p)ˣ 2 P) : ℝ)⁻¹ *
         (∑ m : TreeLeafFiber (ZMod p)ˣ 2 P,
           ‖rationalTreeAmplitude g D Q.tree XL XR c m.1‖ ^ 2) ≤
         8 * differenceMajorant (fieldPairMoment g) (fieldPairMoment g)
           (rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR P) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.differenceMajorant, OAI.Ostmann.fieldPairMoment, OAI.Ostmann.rationalTreeArgument