OAI/Geometry/Relativity/CKS/MixedMassCoefficient.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSMixedGeometry.MassInput line 14
  2. instance OAI.CKSMixedGeometry.massInputNormed line 17
  3. instance OAI.CKSMixedGeometry.massInputSpace line 22
  4. abbrev OAI.CKSMixedGeometry.MassParameter line 27
  5. def OAI.CKSMixedGeometry.lowerMatrixJet line 29
  6. def OAI.CKSMixedGeometry.mulMatrixJet line 30
  7. def OAI.CKSMixedGeometry.mulMatrixThreeJet line 31
  8. def OAI.CKSMixedGeometry.traceProductJet line 32
  9. def OAI.CKSMixedGeometry.coefficientMetric line 34
  10. def OAI.CKSMixedGeometry.coefficientShift line 36
  11. def OAI.CKSMixedGeometry.lieJet line 38
  12. def OAI.CKSMixedGeometry.coefficientLie line 41
  13. def OAI.CKSMixedGeometry.coefficientD line 43
  14. def OAI.CKSMixedGeometry.coefficientT line 46
  15. def OAI.CKSMixedGeometry.coefficientBB line 49
  16. def OAI.CKSMixedGeometry.coefficientV line 52
  17. def OAI.CKSMixedGeometry.cksMassJet line 56
  18. def OAI.CKSMixedGeometry.leadingMassJet line 58
  19. lemma OAI.CKSMixedGeometry.traceProductJet_sub line 63
  20. lemma OAI.CKSMixedGeometry.traceProductJet_smul line 66
  21. lemma OAI.CKSMixedGeometry.mulMatrixJet_zero line 69
  22. lemma OAI.CKSMixedGeometry.mulMatrixThreeJet_zero line 71
  23. lemma OAI.CKSMixedGeometry.coefficientMetric_zero line 73
  24. lemma OAI.CKSMixedGeometry.cksMassJet_zero line 76
  25. lemma OAI.CKSMixedGeometry.lowerMatrixJet_smooth line 83
  26. lemma OAI.CKSMixedGeometry.traceProductJet_smooth line 84
  27. lemma OAI.CKSMixedGeometry.mulMatrixJet_smooth line 88
  28. lemma OAI.CKSMixedGeometry.mulMatrixThreeJet_smooth line 92
  29. lemma OAI.CKSMixedGeometry.mulMatrixThreeJet_contDiff line 98
  30. lemma OAI.CKSMixedGeometry.mulMatrixJet_contDiff line 102
  31. lemma OAI.CKSMixedGeometry.mulMatrixJet_contDiffAt line 106
  32. lemma OAI.CKSMixedGeometry.coefficientMetric_smooth line 112
  33. lemma OAI.CKSMixedGeometry.coefficientShift_smooth line 117
  34. lemma OAI.CKSMixedGeometry.lieJet_smooth line 130
  35. lemma OAI.CKSMixedGeometry.coefficientLie_smooth line 134
  36. lemma OAI.CKSMixedGeometry.coefficientInverse_smooth line 141
  37. lemma OAI.CKSMixedGeometry.coefficientD_smooth line 150
  38. lemma OAI.CKSMixedGeometry.coefficientT_smooth line 170
  39. lemma OAI.CKSMixedGeometry.coefficientBB_smooth line 180
  40. lemma OAI.CKSMixedGeometry.coefficientV_smooth line 192
  41. lemma OAI.CKSMixedGeometry.cksMassJet_smooth line 199