OAI/Geometry/TamingCompatibility/DifferentialForms/RawJetEstimate.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.coordinateTwoJet line 25
2. lemma OAI.TamingCompatibility.GeometricHilbert.coordinateTwoJet_bound line 29
3. lemma OAI.TamingCompatibility.GeometricHilbert.raw_two_jet_estimate line 34
4. def OAI.TamingCompatibility.GeometricChart.deltaComplexA line 78
5. def OAI.TamingCompatibility.GeometricChart.deltaComplexB line 80
6. lemma OAI.TamingCompatibility.GeometricChart.deltaComplexA_smooth line 84
7. lemma OAI.TamingCompatibility.GeometricChart.deltaComplexB_smooth line 87
8. lemma OAI.TamingCompatibility.GeometricChart.delta_local_representation line 91
9. lemma OAI.TamingCompatibility.GeometricChart.ddstar_local_jet line 108
10. lemma OAI.TamingCompatibility.JetOperator.schwartz_direction_basis line 143
11. def OAI.TamingCompatibility.JetOperator.directionOne line 151
12. def OAI.TamingCompatibility.JetOperator.directionTwo line 153
13. lemma OAI.TamingCompatibility.JetOperator.directionOne_value line 156
14. lemma OAI.TamingCompatibility.JetOperator.directionTwo_value line 163
15. def OAI.TamingCompatibility.JetOperator.linearTransport line 172
16. lemma OAI.TamingCompatibility.JetOperator.linearTransport_value line 177
17. lemma OAI.TamingCompatibility.JetOperator.value_recover_linear line 194
18. lemma OAI.TamingCompatibility.JetOperator.linear_output_scaled_bound line 202