OAI/MeasureTheory/Falconer/Slicing/GaussianSlabBox.lean
5 declarations, 0 contain sorry, 0 declared as axioms
Positive Gaussian mass in a bounded coordinate slab
- theorem
OAI.Falconer.gaussian_lower_volume_boundedline 13 - def
OAI.Falconer.coordinateSlabBoxline 30 - theorem
OAI.Falconer.coordinateSlabBox_measurableline 33 - theorem
OAI.Falconer.coordinateSlabBox_volumeline 39 - theorem
OAI.Falconer.coordinateSlabBox_distanceline 62