OAI/MeasureTheory/Falconer/Slicing/GaussianSelectActive.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Choosing a quantitatively nonempty slice with its original active tube covers
- theorem
OAI.Falconer.gaussian_select_active_sliceline 12