OAI/Geometry/TamingCompatibility/Charts/FirstJetGauge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.End line 15
2. def OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.adjointCLM line 17
3. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.adjointCLM_apply line 20
4. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.fderiv_adjoint line 22
5. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.weighted_principal_jet_skew line 30
6. def OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.squareFirst line 61
7. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.squareFirst_skew line 65
8. def OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.halfJet line 73
9. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.halfJet_skew line 76
10. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.halfJet_direction line 82
11. def OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.transformedFirst line 87
12. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.transformedFirst_contDiff line 92
13. lemma OAI.TamingCompatibility.GeometricHilbert.FirstJetGauge.transformedFirst_zero line 101
14. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.pulled_covector line 126
15. lemma OAI.TamingCompatibility.GeometricHilbert.NormalMetricCalculus.pulled_principal line 135