OAI/MeasureTheory/Falconer/Estimates/DyadicTree.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite dyadic trees in the original ambient dimension

All descendants use half-open carriers. Equal-depth cells are disjoint and partition the parent, so restriction to them is an exact measure splitting.

  1. def OAI.Falconer.cubePaths line 18
  2. theorem OAI.Falconer.mem_cubePaths line 22
  3. theorem OAI.Falconer.card_cubePaths line 31
  4. def OAI.Falconer.DyadicCube.descendant line 50
  5. theorem OAI.Falconer.DyadicCube.descendant_nil line 55
  6. theorem OAI.Falconer.DyadicCube.descendant_append line 58
  7. theorem OAI.Falconer.DyadicCube.descendant_side line 65
  8. theorem OAI.Falconer.DyadicCube.descendant_side_pos line 74
  9. theorem OAI.Falconer.DyadicCube.descendant_subset line 80
  10. theorem OAI.Falconer.DyadicCube.descendants_disjoint line 86
  11. theorem OAI.Falconer.DyadicCube.mem_descendant_at_depth line 104
  12. theorem OAI.Falconer.DyadicCube.cover_descendants line 115
  13. theorem OAI.Falconer.DyadicCube.restrict_descendants line 125

    Source documentation

    Exact disjoint measure decomposition; no boundaries or extra spatial cutoffs are added to the original law.

    theorem DyadicCube.restrict_descendants {d : ℕ} (Q : DyadicCube d)
    (μ : Measure (Space d)) (n : ℕ) :
    μ.restrict Q.carrier = ∑ p ∈ cubePaths d n, μ.restrict (Q.descendant p).carrier := by
…

    Mentions: OAI.Falconer.DyadicCube, OAI.Falconer.Space, OAI.Falconer.cubePaths, OAI.Falconer.DyadicCube.carrier

  14. def OAI.Falconer.DyadicCube.occupiedPaths line 138
  15. theorem OAI.Falconer.DyadicCube.card_occupiedPaths_le line 142
  16. theorem OAI.Falconer.DyadicCube.restrict_occupiedPaths line 148