OAI/Geometry/Immersion/ClosedSurface/SmoothCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_comp_smooth line 13
2. lemma OAI.ClosedSurfaceR4.RealModes.second_coordDeriv_comp_smooth line 19
3. lemma OAI.ClosedSurfaceR4.RealModes.realNormalPart_fderiv line 38
4. lemma OAI.ClosedSurfaceR4.RealModes.realSecondForm_comp_smooth line 49
5. def OAI.ClosedSurfaceR4.RealModes.coordDet line 70
6. def OAI.ClosedSurfaceR4.RealModes.pullCovector line 73
7. lemma OAI.ClosedSurfaceR4.RealModes.linear_apply_basis line 76
8. lemma OAI.ClosedSurfaceR4.RealModes.rotated_pullCovector line 81
9. lemma OAI.ClosedSurfaceR4.RealModes.phase_length_comp_smooth line 86
10. lemma OAI.ClosedSurfaceR4.RealModes.norm_phase_length_comp_smooth line 97
11. lemma OAI.ClosedSurfaceR4.RealModes.norm_realSecondForm_le line 108
12. lemma OAI.ClosedSurfaceR4.RealModes.norm_realSecondTensor_comp_smooth line 143