OAI/MeasureTheory/Falconer/Geometry/DyadicCube.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Dyadic cubes in the ambient dimension of the manuscript

Half-open cubes partition without boundary overlaps. Their centers and Euclidean diameter bounds use the same original ambient coordinates as the distance measure.

  1. structure OAI.Falconer.DyadicCube line 19
  2. def OAI.Falconer.DyadicCube.carrier line 23
  3. def OAI.Falconer.DyadicCube.child line 26
  4. def OAI.Falconer.DyadicCube.center line 30
  5. theorem OAI.Falconer.DyadicCube.measurable line 33
  6. theorem OAI.Falconer.DyadicCube.child_subset line 40
  7. theorem OAI.Falconer.DyadicCube.cover_children line 48
  8. theorem OAI.Falconer.DyadicCube.children_disjoint line 66
  9. theorem OAI.Falconer.DyadicCube.center_mem line 83
  10. theorem OAI.Falconer.DyadicCube.dist_le line 91

    Source documentation

    The cube diameter estimate used when choosing a same-ancestor witness.

    theorem DyadicCube.dist_le {d : ℕ} (Q : DyadicCube d) (hQ : 0 ≤ Q.side)
    {x y : Space d} (hx : x ∈ Q.carrier) (hy : y ∈ Q.carrier) :
    dist x y ≤ Real.sqrt d * Q.side := by
…

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