OAI/Analysis/LipschitzHilbert/Trees/LineGridMartingale.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.FiniteLineGrid.measurable_index line 18
2. def OAI.LipschitzHilbert.FiniteLineGrid.nextParent line 21
3. theorem OAI.LipschitzHilbert.FiniteLineGrid.index_nextParent line 25
4. def OAI.LipschitzHilbert.FiniteLineGrid.filtration line 36

   Source documentation

   At level n, the sigma algebra consists precisely of unions of the concrete mesh-index fibers. The grid is frozen after its final depth.

   def filtration (g : FiniteLineGrid) : Filtration ℕ (inferInstance : MeasurableSpace ℝ) where
   …

   Mentions: OAI.LipschitzHilbert.FiniteLineGrid

5. def OAI.LipschitzHilbert.FiniteLineGrid.average line 43
6. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_martingale line 46
7. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_memLp line 50
8. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_constant line 54
9. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_eq_fiber_mean line 62

   Source documentation

   Conditional expectation is the actual integral average on every positive-measure index fiber, pointwise for its canonical representative.

   theorem average_eq_fiber_mean (g : FiniteLineGrid) (μ : Measure ℝ) [IsFiniteMeasure μ]
       (f : ℝ → ℝ) (hf : Integrable f μ) (n : ℕ) (x : ℝ)
       (hpos : μ.real {y | g.index n y = g.index n x} ≠ 0) :
       g.average μ f n x =
         (∫ y in {y | g.index n y = g.index n x}, f y ∂μ) /
           μ.real {y | g.index n y = g.index n x} := by
   …

   Mentions: OAI.LipschitzHilbert.FiniteLineGrid

10. def OAI.LipschitzHilbert.FiniteLineGrid.lineMeasure line 82
11. instance OAI.LipschitzHilbert.FiniteLineGrid.lineMeasure_finite line 84
12. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineMeasure_fiber line 89
13. theorem OAI.LipschitzHilbert.FiniteLineGrid.average_eq_cell_mean line 104

    Source documentation

    On a nonempty mesh interval, the canonical dyadic conditional expectation is exactly the usual Lebesgue average over that interval.

    theorem average_eq_cell_mean (g : FiniteLineGrid) (f : ℝ → ℝ)
        (hf : Integrable f g.lineMeasure) {level i : ℕ}
        (hl : level ≤ g.depth) (hi : i < g.branching ^ level)
        {x : ℝ} (hx : x ∈ g.cell level i) :
        g.average g.lineMeasure f level x =
          (∫ y in g.cell level i, f y) / g.meshWidth level := by
    …

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid