OAI/MeasureTheory/Falconer/Geometry/RetainedEndpointGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The geometric profile bounds survive each actual class refinement. Both endpoint sets use the same original dyadic centers and local similarity.

  1. theorem OAI.Falconer.blockClass_retained_endpoint_geometry line 12