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