SourceLineMaximal.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Actual integer-indexed dyadic line averages. The alternating grids are handled directly, with no alignment premise between a packet and a root.

theorem OAI.LipschitzHilbert.DyadicLineGrid.index_fiber line 15
theorem OAI.LipschitzHilbert.DyadicLineGrid.index_measurable line 24
theorem OAI.LipschitzHilbert.DyadicLineGrid.parent_index_eq line 31
def OAI.LipschitzHilbert.DyadicLineGrid.lineFiltration line 35
def OAI.LipschitzHilbert.DyadicLineGrid.rootMeasure line 48
instance OAI.LipschitzHilbert.DyadicLineGrid.rootMeasure_finite line 50
def OAI.LipschitzHilbert.DyadicLineGrid.lineAverage line 55
theorem OAI.LipschitzHilbert.DyadicLineGrid.lineAverage_martingale line 58
theorem OAI.LipschitzHilbert.DyadicLineGrid.lineAverage_memLp line 62
theorem OAI.LipschitzHilbert.DyadicLineGrid.lineAverage_constant line 66
theorem OAI.LipschitzHilbert.DyadicLineGrid.lineAverage_eq_cell_mean line 74
Source documentation
Each conditional expectation equals the literal average on the actual dyadic cell containing the point.
```
theorem lineAverage_eq_cell_mean (q top j : ℤ) {f : ℝ → ℝ}
    (hf : Integrable f (rootMeasure q top j)) (n : ℕ) {x : ℝ}
    (hx : x∈cell q top j) :
    lineAverage q top j f n x =
      (∫ y in cell q (top-(n:ℤ)) (index q (top-(n:ℤ)) x), f y)/scale (top-(n:ℤ)) := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.rootMeasure, OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.lineAverage, OAI.LipschitzHilbert.DyadicLineGrid.index, OAI.LipschitzHilbert.DyadicLineGrid.scale
theorem OAI.LipschitzHilbert.DyadicLineGrid.lineAverage_maximal_energy line 105
Source documentation
Doob's bound on a root has a constant independent of the root, grid, and number of retained scales.
```
theorem lineAverage_maximal_energy (q top j : ℤ) {f : ℝ → ℝ}
    (hf : MemLp f 2 (rootMeasure q top j)) (N : ℕ) :
    (∫ x, (finiteMaxSignal (lineAverage q top j f) N x)^2 ∂rootMeasure q top j) ≤
      4*∫ x, (f x)^2 ∂rootMeasure q top j := by
…
```
Mentions: OAI.LipschitzHilbert.DyadicLineGrid.rootMeasure, OAI.LipschitzHilbert.finiteMaxSignal, OAI.LipschitzHilbert.DyadicLineGrid.lineAverage