OAI/Geometry/TamingCompatibility/Functional/NormalMap.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap line 26
2. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDifferential line 29
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap_zero line 33
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDifferential_zero line 36
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap_contDiff line 39
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDifferential_contDiff line 42
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMap_fderiv line 45
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalDifferential_eventually_invertible line 51
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalInverse_contDiffAt line 60
10. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledA line 70
11. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledB line 77
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledA_contDiffAt line 82
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledB_contDiffAt line 99
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.pulledA_weighted_principal line 109
15. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ActualData line 149
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_actual_normal_jets line 157