SkippedLineAverage.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Averaging along selected generations of the actual line grid. Angular blocks may have different numbers of steps; no uniform block length is needed.

def OAI.LipschitzHilbert.FiniteLineGrid.ancestor line 14
Source documentation
The ancestor map across any number of generations of the same grid.
```
def ancestor (g : FiniteLineGrid) (steps : ℕ) (i : Fin (g.branching^g.depth)) :
    Fin (g.branching^g.depth) :=
…
```
Mentions: OAI.LipschitzHilbert.FiniteLineGrid
theorem OAI.LipschitzHilbert.FiniteLineGrid.rawIndex_add_div line 18
theorem OAI.LipschitzHilbert.FiniteLineGrid.index_ancestor line 26
theorem OAI.LipschitzHilbert.FiniteLineGrid.nonnegative_profile line 37

theorem OAI.LipschitzHilbert.FiniteLineGrid.skipped_product_average line 56

Source documentation

The conditional-average product estimate on any increasing list of actual generations, including the initial short angular block.

theorem skipped_product_average (g : FiniteLineGrid) (μ : Measure ℝ) [IsFiniteMeasure μ]
    (level : ℕ → ℕ) (N : ℕ) (hlevel : ∀ n ≤ N, level n ≤ g.depth)
    (hmono : ∀ n < N, level n ≤ level (n+1)) (Γ : ℕ → ℝ → ℝ)
    (hΓ : ∀ n < N, ∀ x, 0 ≤ Γ n x)
    (hconstant : ∀ n < N, ∀ x y,
      g.index (level (n+1)) x = g.index (level (n+1)) y → Γ n x = Γ n y)
    (haverage : ∀ n < N, ∀ i : Fin (g.branching^g.depth),
      (∫ x in {x | g.index (level n) x = i}, Γ n x ∂μ) ≤
        μ.real {x | g.index (level n) x = i}) :
    Integrable (fun x => ∏ n ∈ Finset.range N, Γ n x) μ ∧
      (∫ x, ∏ n ∈ Finset.range N, Γ n x ∂μ) ≤ μ.real Set.univ := by
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid

theorem OAI.LipschitzHilbert.FiniteLineGrid.top_weight_skipped_average line 102

Source documentation

The same skipped-generation product can be integrated against the original decaying top weight.

theorem top_weight_skipped_average (g : FiniteLineGrid) (T : SlopeBox) (y : ℝ)
    {K D : ℝ} (hK : 1 ≤ K) (hD : 0 ≤ D) (hwidth : g.width ≤ T.length)
    (level : ℕ → ℕ) (N : ℕ) (hlevel : ∀ n ≤ N, level n ≤ g.depth)
    (hmono : ∀ n < N, level n ≤ level (n+1)) (Γ : ℕ → ℝ → ℝ)
    (hΓ : ∀ n < N, ∀ x, 0 ≤ Γ n x)
    (hconstant : ∀ n < N, ∀ x z,
      g.index (level (n+1)) x = g.index (level (n+1)) z → Γ n x = Γ n z)
    (haverage : ∀ n < N, ∀ i : Fin (g.branching^g.depth),
      (∫ x in {x | g.index (level n) x = i}, Γ n x ∂volume.restrict g.root) ≤
        (volume.restrict g.root).real {x | g.index (level n) x = i}) :
    Integrable (fun x => T.weight K D (x,y+T.slope*x)*
      ∏ n ∈ Finset.range N, Γ n x) (volume.restrict g.root) ∧
…

Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.SlopeBox