OAI/Geometry/TamingCompatibility/DifferentialForms/JetOperator.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.TamingCompatibility.JetOperator.Jet line 19
  2. def OAI.TamingCompatibility.JetOperator.value line 21
  3. def OAI.TamingCompatibility.JetOperator.projZero line 24
  4. def OAI.TamingCompatibility.JetOperator.projOne line 25
  5. def OAI.TamingCompatibility.JetOperator.projTwo line 27
  6. def OAI.TamingCompatibility.JetOperator.firstOrder line 33
  7. def OAI.TamingCompatibility.JetOperator.derivativeComponent line 36
  8. def OAI.TamingCompatibility.JetOperator.derivativeJet line 41
  9. lemma OAI.TamingCompatibility.JetOperator.derivative_component line 46
  10. lemma OAI.TamingCompatibility.JetOperator.directional_reconstruct line 62
  11. lemma OAI.TamingCompatibility.JetOperator.derivativeJet_spec line 73
  12. def OAI.TamingCompatibility.JetOperator.exteriorJet line 82
  13. lemma OAI.TamingCompatibility.JetOperator.exteriorJet_spec line 87
  14. lemma OAI.TamingCompatibility.JetOperator.value_norm line 96
  15. lemma OAI.TamingCompatibility.JetOperator.exteriorJet_bound line 125
  16. lemma OAI.TamingCompatibility.JetOperator.derivativeComponent_smooth line 146
  17. lemma OAI.TamingCompatibility.JetOperator.derivativeJet_smooth line 159
  18. lemma OAI.TamingCompatibility.JetOperator.exteriorJet_smooth line 167
  19. lemma OAI.TamingCompatibility.JetOperator.exteriorJet_bounded line 174