OAI/MeasureTheory/Falconer/Shells/HighShellMixture.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PlanarFalconer.PositiveDistanceData.inversePhasedFormline 11 - def
OAI.PlanarFalconer.PositiveDistanceData.inverseSpatialMixtureline 18 - def
OAI.PlanarFalconer.PositiveDistanceData.inversePhasedBoundline 22 - theorem
OAI.PlanarFalconer.PositiveDistanceData.inversePhasedBound_nonnegline 27 - theorem
OAI.PlanarFalconer.PositiveDistanceData.inversePhasedForm_dataline 33 - theorem
OAI.PlanarFalconer.PositiveDistanceData.inverseSpatialMixture_dataline 58 - theorem
OAI.PlanarFalconer.PositiveDistanceData.inverseSpatialMixture_shellline 71