TreeDensity.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Iterating the elementary tree density estimate

A split plan allows the remaining unit parameters to depend on every previous split coordinate. The bound is uniform over those choices. The separate rational-coordinate lemmas identify the manuscript's tree with this inverse-square split law on valid ancestor data.

def OAI.Ostmann.BinarySplitPlan line 20

Source documentation

Parameters for an ordered binary tree, with adaptive descendant data.

def BinarySplitPlan (U : Type) : ℕ → Type
  | 0 => Unit
  | n + 1 => U × (U → BinarySplitPlan U n) × (U → BinarySplitPlan U n)

def OAI.Ostmann.splitTreeMoment line 24

def OAI.Ostmann.treeDensityMajorant line 37

Source documentation

Parameter-free density majorant, including the zero convention.

noncomputable def treeDensityMajorant {p : ℕ} [Fact p.Prime] (w : ZMod p → ℝ) :
    ℕ → ZMod p → ℝ
  | 0, d => if d = 0 then 0 else w d
  | n + 1, d => if d = 0 then 0 else
      (2 / (Fintype.card (ZMod p)ˣ : ℝ)) *
        differenceMoment (treeDensityMajorant w n) (treeDensityMajorant w n) d

/-- The successive bounds are `E`, `2 E²`, `8 E⁴`, and so on. -/

Mentions: OAI.Ostmann.differenceMoment

def OAI.Ostmann.binaryMomentBound line 45
Source documentation
The successive bounds are E, 2 E², 8 E⁴, and so on.
```
def binaryMomentBound (E : ℝ) : ℕ → ℝ
  | 0 => E
  | n + 1 => 2 * binaryMomentBound E n ^ 2
```
theorem OAI.Ostmann.treeDensityMajorant_zero line 49
theorem OAI.Ostmann.treeDensityMajorant_nonneg line 53
theorem OAI.Ostmann.splitTreeMoment_nonneg line 64

theorem OAI.Ostmann.splitTreeMoment_le_majorant line 83

Source documentation

Each valid split costs at most the factor two in the square-fiber bound.

theorem splitTreeMoment_le_majorant {p : ℕ} [Fact p.Prime]
    (w : ZMod p → ℝ) (hw : ∀ x, 0 ≤ w x) (n : ℕ)
    (plan : BinarySplitPlan (ZMod p)ˣ n) (d : ZMod p) :
    splitTreeMoment w n plan d ≤ treeDensityMajorant w n d := by
…

Mentions: OAI.Ostmann.BinarySplitPlan, OAI.Ostmann.splitTreeMoment, OAI.Ostmann.treeDensityMajorant

theorem OAI.Ostmann.treeDensityMajorant_mean_le line 116

theorem OAI.Ostmann.splitTreeMoment_mean_le line 153

Source documentation

Uniform root averaging permits a different descendant plan at each root value.

theorem splitTreeMoment_mean_le {p : ℕ} [Fact p.Prime]
    (w : ZMod p → ℝ) (hw : ∀ x, 0 ≤ w x) (E : ℝ)
    (hE : (∑ d : (ZMod p)ˣ, w d) / (Fintype.card (ZMod p)ˣ : ℝ) ≤ E)
    (n : ℕ) (plans : (ZMod p)ˣ → BinarySplitPlan (ZMod p)ˣ n) :
    (∑ d : (ZMod p)ˣ, splitTreeMoment w n (plans d) d) /
      (Fintype.card (ZMod p)ˣ : ℝ) ≤ binaryMomentBound E n := by
…

Mentions: OAI.Ostmann.BinarySplitPlan, OAI.Ostmann.splitTreeMoment, OAI.Ostmann.binaryMomentBound

theorem OAI.Ostmann.binaryMomentBound_eq line 164
Source documentation
The recursive density bound in closed form.
```
theorem binaryMomentBound_eq (E : ℝ) (n : ℕ) :
    binaryMomentBound E n = (2 * E) ^ (2 ^ n) / 2 := by
…
```
Mentions: OAI.Ostmann.binaryMomentBound

theorem OAI.Ostmann.splitTreeMoment_l2_bound line 173

Source documentation

The 3^r estimate for an L²-normalized test at an odd prime.

theorem splitTreeMoment_l2_bound {p : ℕ} [Fact p.Prime]
    (hp : 3 ≤ p) (g : ZMod p → ℂ) (hg : g 0 = 0)
    (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
    (n : ℕ) (plans : (ZMod p)ˣ → BinarySplitPlan (ZMod p)ˣ n) :
    (∑ d : (ZMod p)ˣ, splitTreeMoment (fun x => ‖g x‖ ^ 2) n (plans d) d) /
      (Fintype.card (ZMod p)ˣ : ℝ) ≤ (3 : ℝ) ^ (2 ^ n) := by
…

Mentions: OAI.Ostmann.BinarySplitPlan, OAI.Ostmann.splitTreeMoment