OAI/Analysis/LipschitzHilbert/Trees/LineGridPoincare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Low-frequency averaging errors on the actual nested line grid.

  1. theorem OAI.LipschitzHilbert.FiniteLineGrid.index_lt_level line 15
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.cells_cover_root line 22
  3. theorem OAI.LipschitzHilbert.FiniteLineGrid.cells_disjoint line 33
  4. theorem OAI.LipschitzHilbert.FiniteLineGrid.cell_poincare line 43
  5. theorem OAI.LipschitzHilbert.FiniteLineGrid.poincare line 66

    Source documentation

    Summing the actual disjoint cells gives the low-frequency part of the smooth/dyadic comparison, with no loss from their number.

    theorem poincare (g : FiniteLineGrid) (f : ℝ → ℝ)
    (hf : MemLp f 2 g.lineMeasure) (hdf : Differentiable ℝ f)
    (hd : MemLp (deriv f) 2 volume) {level : ℕ} (hl : level ≤ g.depth) :
    (∫ x, |f x - g.average g.lineMeasure f level x| ^ 2 ∂g.lineMeasure) ≤
      g.meshWidth level ^ 2 * ∫ x in g.root, |deriv f x| ^ 2 := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid