OAI/Geometry/Relativity/CKS/CKSPhysicalCoefficients.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularGeometry.inverse_smul line 12
  2. def OAI.CKSAngularGeometry.cksGamma line 15
  3. def OAI.CKSAngularGeometry.cksGammaRadial line 18
  4. def OAI.CKSAngularGeometry.cksTangentialK line 21
  5. def OAI.CKSAngularGeometry.cksShift line 24
  6. def OAI.CKSAngularGeometry.cksRadialMetric line 27
  7. def OAI.CKSAngularGeometry.cksSchur line 30
  8. def OAI.CKSAngularGeometry.cksScaledQ line 33
  9. lemma OAI.CKSAngularGeometry.cksGamma_normalized line 36
  10. lemma OAI.CKSAngularGeometry.cksGammaRadial_normalized line 42
  11. lemma OAI.CKSAngularGeometry.cksShift_normalized line 50
  12. lemma OAI.CKSAngularGeometry.traceProduct_add line 64
  13. lemma OAI.CKSAngularGeometry.traceProduct_smul line 66
  14. lemma OAI.CKSAngularGeometry.cksTangentialK_normalized line 70
  15. theorem OAI.CKSAngularGeometry.physical_trace_coefficient line 78
  16. theorem OAI.CKSAngularGeometry.physical_schur_coefficient line 106