OAI/MeasureTheory/Falconer/Measures/LocalPruningGain.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Original cellwise deletions followed by radial density multiplication
- theorem
OAI.Falconer.radial_gain_of_local_pruningsline 13