OAI/Geometry/TamingCompatibility/DifferentialForms/ScalarJet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TamingCompatibility.ScalarPair.Jet line 13
2. def OAI.TamingCompatibility.ScalarPair.jetComponent line 15
3. def OAI.TamingCompatibility.ScalarPair.jet line 20
4. lemma OAI.TamingCompatibility.ScalarPair.make_jet_bound line 24
5. def OAI.TamingCompatibility.ScalarPair.jetDistribution line 55
6. lemma OAI.TamingCompatibility.ScalarPair.jetDistribution_jet line 58
7. lemma OAI.TamingCompatibility.ScalarPair.jet_derivative line 62
8. def OAI.TamingCompatibility.GeometricHilbert.scalarToJet line 79
9. lemma OAI.TamingCompatibility.GeometricHilbert.scalarToJet_bound line 82
10. def OAI.TamingCompatibility.GeometricHilbert.energyToScalarJet line 101
11. lemma OAI.TamingCompatibility.GeometricHilbert.energyToScalarJet_smooth line 104
12. lemma OAI.TamingCompatibility.GeometricHilbert.energy_scalar_derivative line 108