OAI/MeasureTheory/Falconer/Slicing/GaussianOriginalCosts.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Original incidence selects a controlled slice with both radial costs small
- theorem
OAI.Falconer.gaussian_select_original_costsline 13