OAI/MeasureTheory/Falconer/Estimates/LocalPrefixCenters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Geometric realization of the endpoint cells inside their actual parent. The local similarity preserves the number of cells and gives the separation at the relative depth, as well as a bounded point chart.

  1. theorem OAI.Falconer.localPacketPoint_separated line 14
  2. theorem OAI.Falconer.local_prefix_centers_geometry line 24