OAI/Geometry/Relativity/CKS/CKSTensorJet.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSMixedGeometry.TensorInput line 13
  2. abbrev OAI.CKSMixedGeometry.TensorParameter line 14
  3. instance OAI.CKSMixedGeometry.tensorInputNormed line 15
  4. instance OAI.CKSMixedGeometry.tensorInputSpace line 18
  5. instance OAI.CKSMixedGeometry.tensorParameterNormed line 21
  6. instance OAI.CKSMixedGeometry.tensorParameterSpace line 22
  7. def OAI.CKSMixedGeometry.tensorBase line 24
  8. def OAI.CKSMixedGeometry.tensorQ line 25
  9. def OAI.CKSMixedGeometry.tensorK line 26
  10. def OAI.CKSMixedGeometry.tensorH line 28
  11. def OAI.CKSMixedGeometry.tensorDen line 30
  12. def OAI.CKSMixedGeometry.tensorLapseSq line 32
  13. def OAI.CKSMixedGeometry.tensorLapse line 34
  14. def OAI.CKSMixedGeometry.tensorCross line 37
  15. def OAI.CKSMixedGeometry.tensorNormalQuad line 38
  16. def OAI.CKSMixedGeometry.tensorLCoeff line 41
  17. def OAI.CKSMixedGeometry.tensorEtaCoeff line 44
  18. def OAI.CKSMixedGeometry.tensorTauCoeff line 46
  19. def OAI.CKSMixedGeometry.tensorCoefficients line 51
  20. def OAI.CKSMixedGeometry.tensorRegion line 54
  21. lemma OAI.CKSMixedGeometry.tensorBase_smooth line 57
  22. lemma OAI.CKSMixedGeometry.tensorQ_smooth line 58
  23. lemma OAI.CKSMixedGeometry.tensorK_smooth line 60
  24. lemma OAI.CKSMixedGeometry.tensorH_smooth line 62
  25. lemma OAI.CKSMixedGeometry.tensorDen_smooth line 70
  26. lemma OAI.CKSMixedGeometry.tensorLapseSq_smooth line 77
  27. lemma OAI.CKSMixedGeometry.tensorLapse_smooth line 83
  28. lemma OAI.CKSMixedGeometry.tensorCross_smooth line 97
  29. lemma OAI.CKSMixedGeometry.tensorNormalQuad_smooth line 104
  30. lemma OAI.CKSMixedGeometry.tensorLCoeff_smooth line 114
  31. lemma OAI.CKSMixedGeometry.tensorEtaCoeff_smooth line 124
  32. lemma OAI.CKSMixedGeometry.tensorTauCoeff_smooth line 136
  33. lemma OAI.CKSMixedGeometry.tensorCoefficients_smooth line 144