OAI/Geometry/Relativity/CKS/CollarLapseRealization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSAngularGeometry.lapseVField line 13
  2. def OAI.CKSAngularGeometry.lapseRadField line 15
  3. def OAI.CKSAngularGeometry.lapseDField line 16
  4. def OAI.CKSAngularGeometry.lapseAField line 17
  5. def OAI.CKSAngularGeometry.lapseNormalizedField line 19
  6. lemma OAI.CKSAngularGeometry.lapseVField_diff line 22
  7. lemma OAI.CKSAngularGeometry.lapseRadField_diff line 27
  8. lemma OAI.CKSAngularGeometry.lapseDField_diff line 31
  9. lemma OAI.CKSAngularGeometry.lapseAField_diff line 33
  10. lemma OAI.CKSAngularGeometry.actual_lapseVField line 43
  11. lemma OAI.CKSAngularGeometry.actual_lapseRadField line 54
  12. lemma OAI.CKSAngularGeometry.actual_lapseDField line 61
  13. lemma OAI.CKSAngularGeometry.actual_lapseAField line 67
  14. lemma OAI.CKSAngularGeometry.lapseAField_identity line 88
  15. theorem OAI.CKSAngularGeometry.actual_normalized_lapse_coefficient line 94