OAI/Geometry/Relativity/CKS/AngularGeometry.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularGeometry.Mat line 11
  2. abbrev OAI.CKSAngularGeometry.Jet line 12
  3. abbrev OAI.CKSAngularGeometry.ScalarJet line 13
  4. abbrev OAI.CKSAngularGeometry.CombinedJet line 14
  5. def OAI.CKSAngularGeometry.determinant line 16
  6. def OAI.CKSAngularGeometry.inverse line 18
  7. lemma OAI.CKSAngularGeometry.determinant_eq line 21
  8. lemma OAI.CKSAngularGeometry.inverse_eq line 24
  9. def OAI.CKSAngularGeometry.christoffel line 29
  10. def OAI.CKSAngularGeometry.inverseDerivative line 32
  11. def OAI.CKSAngularGeometry.christoffelDerivative line 35
  12. def OAI.CKSAngularGeometry.ricci line 39
  13. def OAI.CKSAngularGeometry.scalarCurvature line 44
  14. def OAI.CKSAngularGeometry.laplace line 46
  15. def OAI.CKSAngularGeometry.lapseLaplacian line 49
  16. def OAI.CKSAngularGeometry.operators line 54
  17. def OAI.CKSAngularGeometry.regular line 57
  18. lemma OAI.CKSAngularGeometry.determinant_smooth line 59
  19. lemma OAI.CKSAngularGeometry.inverse_component_smooth line 63
  20. lemma OAI.CKSAngularGeometry.christoffel_smooth line 71
  21. lemma OAI.CKSAngularGeometry.inverseDerivative_smooth line 79
  22. lemma OAI.CKSAngularGeometry.christoffelDerivative_smooth line 90
  23. lemma OAI.CKSAngularGeometry.ricci_smooth line 99
  24. lemma OAI.CKSAngularGeometry.operators_smooth line 114
  25. lemma OAI.CKSAngularGeometry.regular_open line 146
  26. theorem OAI.CKSAngularGeometry.operators_uniform_lipschitz line 151