OAI/Geometry/TamingCompatibility/DifferentialForms/MetricTensor.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalJets.MetricTensor line 12
2. abbrev OAI.TamingCompatibility.GeometricHilbert.NormalJets.MetricDerivative line 13
3. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelValue line 15
4. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelValue_inner line 19
5. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelValue_add_left line 26
6. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelValue_smul_left line 34
7. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelValue_add_right line 42
8. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffelValue_smul_right line 50
9. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffel line 58
10. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffel_apply line 64
11. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffel_symm line 67
12. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.christoffel_metric line 76
13. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet line 84
14. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet_zero line 87
15. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet_contDiff line 90
16. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet_hasFDerivAt line 95
17. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet_fderiv_zero line 102
18. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.normalJacobian line 107
19. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.normalJacobian_zero line 110
20. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet_hasFDerivAt_normal line 113
21. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.normalJacobian_hasFDerivAt line 123
22. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.normalJacobian_apply_hasFDerivAt line 127
23. def OAI.TamingCompatibility.GeometricHilbert.NormalJets.pullbackMetric line 131
24. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.pullbackMetric_zero line 135
25. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.pullbackMetric_scalar_hasFDerivAt_zero line 140
26. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.coordinateJet_hasStrictFDerivAt_zero line 163
27. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.normalJacobian_contDiff line 168
28. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.pullbackMetric_contDiffAt line 171
29. lemma OAI.TamingCompatibility.GeometricHilbert.NormalJets.pullbackMetric_fderiv_zero line 189