OAI/Analysis/LipschitzHilbert/Fourier/DyadicLineNesting.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary-depth nesting and uniqueness in the alternating line grids.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.ancestor line 13
  2. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_subset_ancestor line 17
  3. theorem OAI.LipschitzHilbert.DyadicLineGrid.index_eq_of_mem line 25
  4. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_nonempty line 30
  5. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_subset_of_intersect line 39

    Source documentation

    Intersecting cells at ordered scales are nested, including across arbitrarily many generations.

    theorem cell_subset_of_intersect {q k l i j : ℤ} (hkl : k ≤ l)
    (hij : (cell q k i ∩ cell q l j).Nonempty) :
    cell q k i ⊆ cell q l j := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.cell

  6. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_subset_index line 50
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.cells_nested_or_disjoint line 54