OAI/Geometry/Immersion/ClosedSurface/QuadraticCorrection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.RealModes.FreeBudget.mono_order line 13
2. def OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.sizeFactor line 33
3. def OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.errorFactor line 38
4. lemma OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.sizeFactor_nonneg line 45
5. lemma OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.errorFactor_nonneg line 54
6. lemma OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.toSolveBudget_size line 64
7. lemma OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.toSolveBudget_residual line 73
8. theorem OAI.ClosedSurfaceR4.RealModes.constructed_quadratic_correction line 86