OAI/MeasureTheory/Falconer/Geometry/EndpointMidscaleCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The square-root cover required by the regular gain follows from an upper profile chord even when its midpoint lies between selected blocks.

  1. theorem OAI.Falconer.blockClass_retained_midscale_cover line 13