OAI/Analysis/LipschitzHilbert/Trees/DyadicLineGrid.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The nested alternating one-third grids in the line-counting argument.

  1. def OAI.LipschitzHilbert.DyadicLineGrid.scale line 16
  2. def OAI.LipschitzHilbert.DyadicLineGrid.shift line 18
  3. def OAI.LipschitzHilbert.DyadicLineGrid.left line 20
  4. def OAI.LipschitzHilbert.DyadicLineGrid.cell line 22
  5. def OAI.LipschitzHilbert.DyadicLineGrid.parent line 24
  6. def OAI.LipschitzHilbert.DyadicLineGrid.index line 26
  7. theorem OAI.LipschitzHilbert.DyadicLineGrid.scale_pos line 28
  8. theorem OAI.LipschitzHilbert.DyadicLineGrid.scale_succ line 30
  9. theorem OAI.LipschitzHilbert.DyadicLineGrid.shift_succ line 34
  10. theorem OAI.LipschitzHilbert.DyadicLineGrid.mem_index_cell line 39

    Source documentation

    Every point has the usual unique half-open floor cell.

    theorem mem_index_cell (q k : ℤ) (x : ℝ) : x ∈ cell q k (index q k x) := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.index

  11. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_subset_parent line 55

    Source documentation

    The alternating shift gives actual nesting at successive dyadic scales.

    theorem cell_subset_parent (q k j : ℤ) : cell q k j ⊆ cell q (k + 1) (parent q k j) := by
…

    Mentions: OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.parent

  12. theorem OAI.LipschitzHilbert.DyadicLineGrid.cells_disjoint line 88
  13. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_measurable line 105
  14. theorem OAI.LipschitzHilbert.DyadicLineGrid.cell_length line 107