OAI/Geometry/Immersion/ClosedSurface/ForcedSolve.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.contDiffOn_displacement line 17
2. structure OAI.ClosedSurfaceR4.RealModes.SupportedSolveChart line 27
3. def OAI.ClosedSurfaceR4.RealModes.SupportedSolveChart.solve line 43
4. structure OAI.ClosedSurfaceR4.RealModes.SolveBudget line 49
5. def OAI.ClosedSurfaceR4.RealModes.SolveBudget.size line 67
6. def OAI.ClosedSurfaceR4.RealModes.SolveBudget.residual line 72
7. theorem OAI.ClosedSurfaceR4.RealModes.SupportedSolveChart.solve_spec line 79
8. theorem OAI.ClosedSurfaceR4.RealModes.finite_forced_solve line 105
9. lemma OAI.ClosedSurfaceR4.RealModes.quadraticPhase_smooth line 151
10. theorem OAI.ClosedSurfaceR4.RealModes.finite_quadratic_cancellation line 164