OAI/Geometry/Relativity/CKS/CKSMassCoefficient.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularGeometry.MassInput line 12
  2. def OAI.CKSAngularGeometry.lowerMatrixJet line 15
  3. def OAI.CKSAngularGeometry.traceProductJet line 17
  4. def OAI.CKSAngularGeometry.coefficientMetric line 20
  5. def OAI.CKSAngularGeometry.coefficientShift line 23
  6. def OAI.CKSAngularGeometry.coefficientLie line 26
  7. def OAI.CKSAngularGeometry.coefficientD line 29
  8. def OAI.CKSAngularGeometry.coefficientT line 33
  9. def OAI.CKSAngularGeometry.coefficientBB line 37
  10. def OAI.CKSAngularGeometry.coefficientV line 41
  11. def OAI.CKSAngularGeometry.cksMassJet line 45
  12. def OAI.CKSAngularGeometry.leadingMassJet line 48
  13. lemma OAI.CKSAngularGeometry.traceProductJet_sub line 53
  14. lemma OAI.CKSAngularGeometry.traceProductJet_smul line 57
  15. lemma OAI.CKSAngularGeometry.coefficientMetric_zero line 61
  16. lemma OAI.CKSAngularGeometry.cksMassJet_zero line 64
  17. lemma OAI.CKSAngularGeometry.lowerMatrixJet_smooth line 72
  18. lemma OAI.CKSAngularGeometry.traceProductJet_smooth line 73
  19. lemma OAI.CKSAngularGeometry.coefficientMetric_smooth line 78
  20. lemma OAI.CKSAngularGeometry.coefficientShift_smooth line 82
  21. lemma OAI.CKSAngularGeometry.coefficientLie_smooth line 88
  22. lemma OAI.CKSAngularGeometry.coefficientInverse_smooth line 103
  23. lemma OAI.CKSAngularGeometry.coefficientD_smooth line 113
  24. lemma OAI.CKSAngularGeometry.coefficientT_smooth line 127
  25. lemma OAI.CKSAngularGeometry.coefficientBB_smooth line 138
  26. lemma OAI.CKSAngularGeometry.coefficientV_smooth line 151
  27. lemma OAI.CKSAngularGeometry.cksMassJet_smooth line 160