OAI/MeasureTheory/Falconer/Slicing/GaussianSelectionBudget.lean
1 declarations, 0 contain sorry, 0 declared as axioms
A quantitative retained slice from the proved Gaussian moment bounds
- theorem
OAI.Falconer.gaussian_select_slice_of_budgetline 14