OAI/Geometry/Relativity/CKS/CollarRawMomentum.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CKSAngularGeometry.RawMetricData line 13
  2. abbrev OAI.CKSAngularGeometry.RawTensorData line 15
  3. instance OAI.CKSAngularGeometry.rawMetricNormedGroup line 16
  4. instance OAI.CKSAngularGeometry.rawTensorNormedGroup line 17
  5. instance OAI.CKSAngularGeometry.rawMetricNormedSpace line 18
  6. instance OAI.CKSAngularGeometry.rawTensorNormedSpace line 19
  7. abbrev OAI.CKSAngularGeometry.RawCollarData line 20
  8. instance OAI.CKSAngularGeometry.rawCollarNormedGroup line 21
  9. instance OAI.CKSAngularGeometry.rawCollarNormedSpace line 22
  10. abbrev OAI.CKSAngularGeometry.RawCollarInput line 24
  11. abbrev OAI.CKSAngularGeometry.rz line 25
  12. abbrev OAI.CKSAngularGeometry.re line 26
  13. abbrev OAI.CKSAngularGeometry.rθ line 27
  14. abbrev OAI.CKSAngularGeometry.rpad line 28
  15. abbrev OAI.CKSAngularGeometry.rwgt line 29
  16. abbrev OAI.CKSAngularGeometry.rmat line 30
  17. abbrev OAI.CKSAngularGeometry.rdmat line 31
  18. abbrev OAI.CKSAngularGeometry.rshift line 32
  19. abbrev OAI.CKSAngularGeometry.rdshift line 33
  20. abbrev OAI.CKSAngularGeometry.rscalar line 34
  21. abbrev OAI.CKSAngularGeometry.reta line 35
  22. abbrev OAI.CKSAngularGeometry.rtau line 36
  23. abbrev OAI.CKSAngularGeometry.retar line 37
  24. def OAI.CKSAngularGeometry.rawQ line 39
  25. def OAI.CKSAngularGeometry.rawDQ line 40
  26. def OAI.CKSAngularGeometry.rawS line 41
  27. def OAI.CKSAngularGeometry.rawDS line 42
  28. def OAI.CKSAngularGeometry.rawQr line 43
  29. def OAI.CKSAngularGeometry.rawExpansionInput line 44
  30. def OAI.CKSAngularGeometry.rawC line 46
  31. def OAI.CKSAngularGeometry.matrixTraceJet line 49
  32. def OAI.CKSAngularGeometry.traceFreeJet line 51
  33. def OAI.CKSAngularGeometry.rawD line 53
  34. def OAI.CKSAngularGeometry.rawT line 54
  35. def OAI.CKSAngularGeometry.rawF line 55
  36. def OAI.CKSAngularGeometry.rawL line 57
  37. def OAI.CKSAngularGeometry.rawTr line 58
  38. def OAI.CKSAngularGeometry.rawLapseInput line 59
  39. def OAI.CKSAngularGeometry.rawA line 60
  40. def OAI.CKSAngularGeometry.rawLambda line 61
  41. def OAI.CKSAngularGeometry.rawX line 62
  42. def OAI.CKSAngularGeometry.scalarMatrixToJet line 65
  43. def OAI.CKSAngularGeometry.rawMomentumInput line 67
  44. def OAI.CKSAngularGeometry.rawRegular line 72
  45. lemma OAI.CKSAngularGeometry.rawQ_smooth line 74
  46. lemma OAI.CKSAngularGeometry.rawExpansionInput_smooth line 75
  47. lemma OAI.CKSAngularGeometry.rawC_smooth line 78
  48. lemma OAI.CKSAngularGeometry.matrixTraceJet_smooth line 82
  49. lemma OAI.CKSAngularGeometry.traceFreeJet_smooth line 91
  50. lemma OAI.CKSAngularGeometry.rawD_smooth line 99
  51. lemma OAI.CKSAngularGeometry.rawT_smooth line 102
  52. lemma OAI.CKSAngularGeometry.rawF_smooth line 103
  53. lemma OAI.CKSAngularGeometry.rawLapseInput_smooth line 106
  54. lemma OAI.CKSAngularGeometry.rawA_smooth line 110
  55. lemma OAI.CKSAngularGeometry.rawMomentumInput_smooth line 113