OAI/Geometry/Relativity/CKS/LogPhysicalTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSMixedGeometry.normalizeTensorLogFields line 12
  2. def OAI.CKSMixedGeometry.logRadialK line 17
  3. def OAI.CKSMixedGeometry.logOriginalL line 19
  4. def OAI.CKSMixedGeometry.logOriginalEta line 24
  5. def OAI.CKSMixedGeometry.logOriginalTau line 27
  6. lemma OAI.CKSMixedGeometry.logTensorK_normalized line 31
  7. lemma OAI.CKSMixedGeometry.logLapseSq_normalized line 41
  8. lemma OAI.CKSMixedGeometry.logLapse_normalized line 55
  9. lemma OAI.CKSMixedGeometry.radiusPower_minus_three line 77
  10. lemma OAI.CKSMixedGeometry.logOriginalEta_normalized line 80
  11. lemma OAI.CKSMixedGeometry.logOriginalTau_normalized line 108
  12. lemma OAI.CKSMixedGeometry.logBB_normalized line 131
  13. lemma OAI.CKSMixedGeometry.logShift_coefficient line 148
  14. lemma OAI.CKSMixedGeometry.logCross_normalized line 158
  15. lemma OAI.CKSMixedGeometry.logQuad_normalized line 169
  16. lemma OAI.CKSMixedGeometry.logOriginalL_normalized line 185