OAI/NumberTheory/Ostmann/Characters/TreeTupleProfiles.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.treeLeafTupleEquiv_map line 11
2. theorem OAI.Ostmann.treeLeafZipProduct_eq_prod line 21
3. theorem OAI.Ostmann.treeWeightsNonneg_iff line 36
4. theorem OAI.Ostmann.treeProfileMean_eq_prod line 54
5. theorem OAI.Ostmann.quartetProducts_eq_map line 71
6. theorem OAI.Ostmann.rationalTreeAmplitude_product_of_cut line 78
7. theorem OAI.Ostmann.rationalTreeAmplitude_cut_secondMoment line 98

   Source documentation

   On any fixed valid cut, the conditional second moment factors into the exact independent quartet second moments.

   theorem rationalTreeAmplitude_cut_secondMoment {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) (n : ℕ) {C : (ZMod p)ˣ}
       (T : RationalTreeData (ZMod p)ˣ (n + 2) C) (XL XR : (ZMod p)ˣ)
       (c : TreeLeafTuple Bool (n + 2)) (P : TreeLeafIndex n → (ZMod p)ˣ)
       (S : TreeLeafTuple (RationalQuartetState p) n)
       (hS : rationalQuartetStates n T XL XR c ((treeLeafTupleEquiv _ n).symm P) = some S) :
       (Fintype.card (QuartetProductFiber (ZMod p)ˣ n P) : ℝ)⁻¹ *
         (∑ m : QuartetProductFiber (ZMod p)ˣ n P,
           ‖rationalTreeAmplitude g D T XL XR c m.1‖ ^ 2) =
         ∏ i : TreeLeafIndex n, (Fintype.card (TreeLeafFiber (ZMod p)ˣ 2 (P i)) : ℝ)⁻¹ *
           ∑ m : TreeLeafFiber (ZMod p)ˣ 2 (P i),
             ‖rationalQuartetStateAmplitude g D (treeLeafTupleEquiv _ n S i) m.1‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.RationalQuartetState, OAI.Ostmann.rationalQuartetStates, OAI.Ostmann.treeLeafTupleEquiv, OAI.Ostmann.QuartetProductFiber, OAI.Ostmann.rationalTreeAmplitude, OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.rationalQuartetStateAmplitude