OAI/MeasureTheory/Falconer/Estimates/RoundedEndpointGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the actual normal/good cell estimates to an inward-rounded profile partition and close the finite endpoint induction.

  1. theorem OAI.Falconer.rounded_profile_endpoint_gain line 11