OAI/Geometry/Relativity/CKS/CollarLapseCoefficient.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularGeometry.LapseCoefficientInput line 11
  2. abbrev OAI.CKSAngularGeometry.lz line 12
  3. abbrev OAI.CKSAngularGeometry.lT line 13
  4. abbrev OAI.CKSAngularGeometry.lF line 14
  5. abbrev OAI.CKSAngularGeometry.lD line 15
  6. def OAI.CKSAngularGeometry.lapseV line 17
  7. def OAI.CKSAngularGeometry.lapseRad line 19
  8. def OAI.CKSAngularGeometry.lapseD line 20
  9. def OAI.CKSAngularGeometry.lapseA line 22
  10. def OAI.CKSAngularGeometry.lapseCoefficientRegion line 25
  11. lemma OAI.CKSAngularGeometry.lapseV_smooth line 27
  12. lemma OAI.CKSAngularGeometry.lapseRad_smooth line 34
  13. lemma OAI.CKSAngularGeometry.lapseD_smooth line 36
  14. lemma OAI.CKSAngularGeometry.lapseA_smooth line 37
  15. lemma OAI.CKSAngularGeometry.lapseCoefficientRegion_open line 50
  16. lemma OAI.CKSAngularGeometry.lapseCoefficientRegion_zero line 53
  17. lemma OAI.CKSAngularGeometry.lapseA_identity line 56
  18. lemma OAI.CKSAngularGeometry.lapseCoefficient_uniform line 74