OAI/Geometry/Immersion/ClosedSurface/SecondForms.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.real_second_coordDeriv line 13
2. lemma OAI.ClosedSurfaceR4.RealModes.real_second_coordDeriv_comm line 21
3. lemma OAI.ClosedSurfaceR4.RealModes.base_eq_basis line 29
4. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_eq_basis line 31
5. lemma OAI.ClosedSurfaceR4.RealModes.second_coordDeriv_quadratic line 36
6. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_comp_linear line 53
7. lemma OAI.ClosedSurfaceR4.RealModes.second_coordDeriv_comp_linear line 59
8. def OAI.ClosedSurfaceR4.RealModes.realSecondForm line 68
9. def OAI.ClosedSurfaceR4.RealModes.realSecondTensor line 71
10. lemma OAI.ClosedSurfaceR4.RealModes.realSecondForm_quadratic line 74
11. lemma OAI.ClosedSurfaceR4.RealModes.gramDet_comp_linear line 82
12. lemma OAI.ClosedSurfaceR4.RealModes.realSecondForm_comp_linear line 90
13. lemma OAI.ClosedSurfaceR4.RealModes.second_coordDeriv_bilinear line 106
14. lemma OAI.ClosedSurfaceR4.RealModes.realSecondForm_bilinear line 123
15. lemma OAI.ClosedSurfaceR4.RealModes.realSecondTensor_ne_zero_iff line 134
16. theorem OAI.ClosedSurfaceR4.RealModes.actual_positive_phase_data line 150