OAI/MeasureTheory/Falconer/Geometry/FarCellGeometry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual cell geometry used by the far transition

The fixed separation constant may be chosen as 2000(d+1). Comparable point displacements at a dyadic depth then give cells satisfying that separation, while a center displacement outside the near graph remains large throughout both cells.

  1. theorem OAI.Falconer.DyadicCube.point_center_bound line 17
  2. theorem OAI.Falconer.DyadicCube.far_centers_force_far_points line 24
  3. theorem OAI.Falconer.DyadicCube.comparable_points_separate_cells line 37