OAI/Geometry/Relativity/CKS/LogPhysicalCoefficients.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSMixedGeometry.radiusPower_neg_nat line 13
  2. lemma OAI.CKSMixedGeometry.radiusPower_inverse line 15
  3. lemma OAI.CKSMixedGeometry.radiusPower_two line 18
  4. lemma OAI.CKSMixedGeometry.radiusPower_three line 19
  5. lemma OAI.CKSMixedGeometry.radiusPower_six line 20
  6. lemma OAI.CKSMixedGeometry.radiusPower_minus_five line 21
  7. lemma OAI.CKSMixedGeometry.D_radiusPower_angular line 23
  8. lemma OAI.CKSMixedGeometry.normalizedLie_radius line 28
  9. def OAI.CKSMixedGeometry.logGamma line 48
  10. def OAI.CKSMixedGeometry.logGammaRadial line 51
  11. def OAI.CKSMixedGeometry.logTangentialK line 55
  12. def OAI.CKSMixedGeometry.logShift line 58
  13. def OAI.CKSMixedGeometry.logRadialMetric line 61
  14. def OAI.CKSMixedGeometry.logSchur line 64
  15. def OAI.CKSMixedGeometry.logScaledQ line 67
  16. lemma OAI.CKSMixedGeometry.logGamma_normalized line 71
  17. lemma OAI.CKSMixedGeometry.logGammaRadial_normalized line 80
  18. lemma OAI.CKSMixedGeometry.logShift_normalized line 91
  19. lemma OAI.CKSMixedGeometry.logTangentialK_normalized line 106
  20. lemma OAI.CKSMixedGeometry.traceProduct_add line 118
  21. lemma OAI.CKSMixedGeometry.traceProduct_smul line 120
  22. lemma OAI.CKSMixedGeometry.traceProduct_smul_left line 122
  23. lemma OAI.CKSMixedGeometry.log_trace_coefficient line 131
  24. lemma OAI.CKSMixedGeometry.log_schur_coefficient line 152