OAI/NumberTheory/Ostmann/Tree/RationalTreeLeaves.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.rationalTreeLeafValue line 12
2. theorem OAI.Ostmann.rationalTreeLeafValue_fiber_sum line 25
3. theorem OAI.Ostmann.rationalTreeLeafValue_mean_eq line 81
4. theorem OAI.Ostmann.rationalTreeLeafValue_l2_bound line 98

   Source documentation

   The first part of the tree comparison: independent uniform leaves give the 3^r bound.

   theorem rationalTreeLeafValue_l2_bound {p : ℕ} [Fact p.Prime]
       (hp : 3 ≤ p) (g : ZMod p → ℂ) (hg : g 0 = 0)
       (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
       (D : (ZMod p)ˣ) {n : ℕ} {C : (ZMod p)ˣ}
       (T : RationalTreeData (ZMod p)ˣ n C) (XL XR : (ZMod p)ˣ) :
       (∑ x : TreeLeafTuple (ZMod p)ˣ n,
         rationalTreeLeafValue (fun y => ‖g y‖ ^ 2) D T XL XR x) /
         (Fintype.card (TreeLeafTuple (ZMod p)ˣ n) : ℝ) ≤ (3 : ℝ) ^ (2 ^ n) := by
   …

   Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.rationalTreeLeafValue

5. def OAI.Ostmann.rationalTreeAmplitude line 110

   Source documentation

   The manuscript's diagram value, permitting arbitrary conjugation choices at the leaves.

   noncomputable def rationalTreeAmplitude {p : ℕ} [Fact p.Prime]
       (g : ZMod p → ℂ) (D : (ZMod p)ˣ) :
       {n : ℕ} → {C : (ZMod p)ˣ} → RationalTreeData (ZMod p)ˣ n C →
         (ZMod p)ˣ → (ZMod p)ˣ → TreeLeafTuple Bool n → TreeLeafTuple (ZMod p)ˣ n → ℂ
     | _, _, .leaf s C, XL, XR, c, m =>
       match (c : Bool) with
       | true => star (g (rationalTreeArgument s C D XL XR m))
       | false => g (rationalTreeArgument s C D XL XR m)
     | n + 1, _, .node s CL CR u left right, XL, XR, c, ab =>
       let HL : (ZMod p)ˣ := XL * CL * treeLeafProduct n ab.1
   …

   Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.rationalTreeArgument, OAI.Ostmann.treeLeafProduct

6. theorem OAI.Ostmann.norm_rationalTreeAmplitude_sq line 126
7. theorem OAI.Ostmann.rationalTreeAmplitude_l2_bound line 142

   Source documentation

   Equation src37, with the actual reconstructed-node diagram and uniform independent leaves.

   theorem rationalTreeAmplitude_l2_bound {p : ℕ} [Fact p.Prime]
       (hp : 3 ≤ p) (g : ZMod p → ℂ) (hg : g 0 = 0)
       (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
       (D : (ZMod p)ˣ) {n : ℕ} {C : (ZMod p)ˣ}
       (T : RationalTreeData (ZMod p)ˣ n C) (XL XR : (ZMod p)ˣ)
       (c : TreeLeafTuple Bool n) :
       (∑ m : TreeLeafTuple (ZMod p)ˣ n, ‖rationalTreeAmplitude g D T XL XR c m‖ ^ 2) /
         (Fintype.card (TreeLeafTuple (ZMod p)ˣ n) : ℝ) ≤ (3 : ℝ) ^ (2 ^ n) := by
   …

   Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.rationalTreeAmplitude