OAI/Geometry/Immersion/ClosedSurface/FreeCharts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart line 17
2. def OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart.amplitude line 33
3. structure OAI.ClosedSurfaceR4.RealModes.FreeBudget line 39
4. def OAI.ClosedSurfaceR4.RealModes.FreeBudget.seedConstant line 60
5. def OAI.ClosedSurfaceR4.RealModes.FreeBudget.size line 64
6. def OAI.ClosedSurfaceR4.RealModes.FreeBudget.residual line 69
7. lemma OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart.amplitude_smooth line 76
8. theorem OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart.displacement_spec line 87
9. theorem OAI.ClosedSurfaceR4.RealModes.finite_free_displacement line 127
10. def OAI.ClosedSurfaceR4.RealModes.FreeBudget.slowSize line 174
11. lemma OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart.amplitude_bound line 179