RationalTree.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Recursive rational tree data

The product coefficient is an index of the data type. At every split, its child indices encode exactly the consistency conditions on the fixed constants in src36.

inductive OAI.Ostmann.RationalTreeData line 18
def OAI.Ostmann.RationalTreeData.frequency line 24
def OAI.Ostmann.rationalTreeArgument line 29
def OAI.Ostmann.rationalTreeMoment line 32
theorem OAI.Ostmann.rationalTreeArgument_child line 46
theorem OAI.Ostmann.rationalTreeArgument_node line 54
theorem OAI.Ostmann.rationalTreeMoment_nonneg line 61

theorem OAI.Ostmann.rationalTreeMoment_le_majorant line 78

Source documentation

The actual recursive rational-node moment is bounded by the uniform density majorant.

theorem rationalTreeMoment_le_majorant {p : ℕ} [Fact p.Prime]
    (w : ZMod p → ℝ) (hw : ∀ x, 0 ≤ w x) (D : (ZMod p)ˣ)
    {n : ℕ} {C : (ZMod p)ˣ} (T : RationalTreeData (ZMod p)ˣ n C)
    (XL XR P : (ZMod p)ˣ) :
    rationalTreeMoment w D T XL XR P ≤
      treeDensityMajorant w n (rationalTreeArgument T.frequency C D XL XR P) := by
…

Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.rationalTreeMoment, OAI.Ostmann.treeDensityMajorant, OAI.Ostmann.rationalTreeArgument

def OAI.Ostmann.rationalTreeArgumentEquiv line 119
Source documentation
With the other root data fixed, exposing the total leaf product gives a uniform argument.
```
noncomputable def rationalTreeArgumentEquiv {p : ℕ} [Fact p.Prime]
    (s C D XL XR : (ZMod p)ˣ) : (ZMod p)ˣ ≃ (ZMod p)ˣ where
…
```
theorem OAI.Ostmann.rationalTreeMoment_mean_le line 126

theorem OAI.Ostmann.rationalTreeMoment_l2_bound line 147

Source documentation

The actual rational tree, averaged in its root product, satisfies src37.

theorem rationalTreeMoment_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)ˣ) :
    (∑ P : (ZMod p)ˣ, rationalTreeMoment (fun x => ‖g x‖ ^ 2) D T XL XR P) /
      (Fintype.card (ZMod p)ˣ : ℝ) ≤ (3 : ℝ) ^ (2 ^ n) := by
…

Mentions: OAI.Ostmann.RationalTreeData, OAI.Ostmann.rationalTreeMoment