OAI/Geometry/IsometricImmersion/Darboux/DarbouxJet.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.jetConnection line 16
  2. def OAI.SmoothLocal.Geometry.jetMixed line 19
  3. def OAI.SmoothLocal.Geometry.jetYY line 22
  4. def OAI.SmoothLocal.Geometry.jetEnergy line 25
  5. def OAI.SmoothLocal.Geometry.jetNumerator line 29
  6. def OAI.SmoothLocal.Geometry.solvedDarboux line 32
  7. def OAI.SmoothLocal.Geometry.jetDriftVector line 35
  8. def OAI.SmoothLocal.Geometry.christoffelAlongD line 37
  9. theorem OAI.SmoothLocal.Geometry.DarbouxJetCalculus.coordPartial_const line 42
  10. theorem OAI.SmoothLocal.Geometry.DarbouxJetCalculus.coordPartial_eval line 46
  11. theorem OAI.SmoothLocal.Geometry.DarbouxJetCalculus.coordPartial_sq line 50
  12. theorem OAI.SmoothLocal.Geometry.jetConnection_differentiableAt line 59
  13. theorem OAI.SmoothLocal.Geometry.coordPartial_jetConnection line 68
  14. theorem OAI.SmoothLocal.Geometry.jetMixed_differentiableAt line 84
  15. theorem OAI.SmoothLocal.Geometry.jetYY_differentiableAt line 90
  16. theorem OAI.SmoothLocal.Geometry.coordPartial_jetMixed line 96
  17. theorem OAI.SmoothLocal.Geometry.coordPartial_jetYY line 103
  18. theorem OAI.SmoothLocal.Geometry.jetEnergy_differentiableAt line 110
  19. theorem OAI.SmoothLocal.Geometry.coordPartial_jetEnergy line 123
  20. theorem OAI.SmoothLocal.Geometry.jetNumerator_differentiableAt line 141
  21. theorem OAI.SmoothLocal.Geometry.coordPartial_jetNumerator line 154
  22. theorem OAI.SmoothLocal.Geometry.solvedDarboux_firstJet_expanded line 175
  23. theorem OAI.SmoothLocal.Geometry.christoffelAlongD_eq line 199
  24. theorem OAI.SmoothLocal.Geometry.solvedDarboux_firstJet line 210
  25. theorem OAI.SmoothLocal.Geometry.solvedDarboux_deriv_b line 221
  26. theorem OAI.SmoothLocal.Geometry.solvedDarboux_deriv_c line 236
  27. theorem OAI.SmoothLocal.Geometry.jetEnergy_at_height line 253
  28. theorem OAI.SmoothLocal.Geometry.jetMixed_at_height line 259
  29. theorem OAI.SmoothLocal.Geometry.jetYY_at_height line 263