OAI/Analysis/LipschitzHilbert/Trees/SourceLineWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An actual coarse line cell carries a local grid with exactly the same fine partitions as the global line grid. This identifies the local prediction factors before they are patched over coarse cells.

  1. def OAI.LipschitzHilbert.FiniteLineGrid.lineWindow line 13
  2. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineWindow_root line 21
  3. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineWindow_meshWidth line 29
  4. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineWindow_coordinate line 35

    Source documentation

    The local normalized coordinate differs from the global one by an integer number of fine cells, with the same integer branching power.

    theorem lineWindow_coordinate (g : FiniteLineGrid) (coarse i depth k : ℕ) (x : ℝ) :
    ((x-(g.lineWindow coarse i depth).origin)/(g.lineWindow coarse i depth).width)*
        ((g.lineWindow coarse i depth).branching:ℝ)^k+
      ((i*g.branching^k:ℕ):ℝ) =
        ((x-g.origin)/g.width)*(g.branching:ℝ)^(coarse+k) := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid

  5. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineWindow_rawIndex line 45
  6. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineWindow_index_of_global line 63

    Source documentation

    On the coarse cell, equality of the actual global fine indices is exactly strong enough to preserve a local prediction's constancy.

    theorem lineWindow_index_of_global (g : FiniteLineGrid) (coarse i depth k : ℕ)
    (hi : i < g.branching^coarse) (hk : k ≤ depth) (hglobal : coarse+k ≤ g.depth)
    {x y : ℝ} (hx : x ∈ g.cell coarse i) (hy : y ∈ g.cell coarse i)
    (hxy : g.index (coarse+k) x = g.index (coarse+k) y) :
    (g.lineWindow coarse i depth).index k x = (g.lineWindow coarse i depth).index k y := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.FiniteLineGrid.index

  7. theorem OAI.LipschitzHilbert.FiniteLineGrid.lineWindow_index_iff_global line 82

    Source documentation

    The converse also holds, so local and global partitions agree exactly after restricting them to the selected coarse cell.

    theorem lineWindow_index_iff_global (g : FiniteLineGrid) (coarse i depth k : ℕ)
    (hi : i < g.branching^coarse) (hk : k ≤ depth) (hglobal : coarse+k ≤ g.depth)
    {x y : ℝ} (hx : x ∈ g.cell coarse i) (hy : y ∈ g.cell coarse i) :
    (g.lineWindow coarse i depth).index k x = (g.lineWindow coarse i depth).index k y ↔
      g.index (coarse+k) x = g.index (coarse+k) y := by
…

    Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.FiniteLineGrid.index