OAI/Analysis/LipschitzHilbert/Trees/FiniteLineGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Actual finite line partitions, nested at an integer branching ratio.

  1. structure OAI.LipschitzHilbert.FiniteLineGrid line 15
  2. def OAI.LipschitzHilbert.FiniteLineGrid.root line 27
  3. def OAI.LipschitzHilbert.FiniteLineGrid.rawIndex line 29
  4. theorem OAI.LipschitzHilbert.FiniteLineGrid.rawIndex_lt line 32
  5. def OAI.LipschitzHilbert.FiniteLineGrid.index line 51
  6. def OAI.LipschitzHilbert.FiniteLineGrid.parent line 54
  7. theorem OAI.LipschitzHilbert.FiniteLineGrid.rawIndex_parent line 58
  8. theorem OAI.LipschitzHilbert.FiniteLineGrid.index_parent line 71

    Source documentation

    The partitions refine on the entire line, including outside the root.

    theorem index_parent (g : FiniteLineGrid) {level : ℕ} (hlevel : level < g.depth) (x : ℝ) :
    g.index level x = g.parent (g.index (level + 1) x) := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid

  9. theorem OAI.LipschitzHilbert.FiniteLineGrid.measurable_rawIndex line 79
  10. theorem OAI.LipschitzHilbert.FiniteLineGrid.measurable_index_fiber line 84
  11. theorem OAI.LipschitzHilbert.FiniteLineGrid.same_index_distance line 94

    Source documentation

    Two points of one finer cell differ by at most its mesh width.

    theorem same_index_distance (g : FiniteLineGrid) {level : ℕ} (hlevel : level ≤ g.depth)
    {x y : ℝ} (hx : x ∈ g.root) (hy : y ∈ g.root)
    (hxy : g.index level x = g.index level y) :
    |x - y| ≤ g.width / (g.branching : ℝ) ^ level := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid