OAI/Geometry/TamingCompatibility/DifferentialForms/Dpos.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.UniformJets.dpos line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.dpos_eq line 27
3. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.dpos_contDiff line 34
4. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.linear_bound line 38
5. lemma OAI.TamingCompatibility.GeometricHilbert.UniformJets.quadratic_bound line 58
6. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMap line 95
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMap_apply line 98
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMap_smooth line 102
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameMap_metric line 109
10. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameEquiv line 118
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.frameEquiv_coe line 131
12. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_metric_frame_extension line 135
13. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.affineMetric line 158
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.affineMetric_contDiff line 162
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.affineMetric_symm line 173
16. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.metricJet line 178
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.metricJet_contDiff line 182
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.metricJet_eq line 188
19. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMetric line 193
20. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMetric_contDiff line 197
21. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMetric_zero line 218
22. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMetric_dpos_zero line 223
23. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.centeredDisplacement_hasFDerivAt line 237
24. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.normalMetric_eq_pullback line 250
25. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_geometric_normal_metric line 261