OAI/Geometry/Immersion/ClosedSurface/GeometryBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.FreeBudget.slowSize_nonneg line 13
2. lemma OAI.ClosedSurfaceR4.RealModes.FreeBudget.size_nonneg line 23
3. lemma OAI.ClosedSurfaceR4.RealModes.weighted_quadraticAmplitude line 34
4. theorem OAI.ClosedSurfaceR4.RealModes.weighted_free_quadraticAmplitude line 55
5. structure OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget line 85
6. def OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.forcingFactor line 106
7. lemma OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.forcingFactor_nonneg line 112
8. def OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.toSolveBudget line 122