OAI/Geometry/Relativity/CKS/CollarRadialFields.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CKSAngularSlice.paddingDensity_rpow line 14
  2. def OAI.CKSAngularSlice.radialLift line 20
  3. lemma OAI.CKSAngularSlice.radialLift_diff line 22
  4. lemma OAI.CKSAngularSlice.radialLift_D line 25
  5. def OAI.CKSAngularSlice.collarQ line 35
  6. def OAI.CKSAngularSlice.collarShift line 38
  7. def OAI.CKSAngularSlice.collarT line 41
  8. def OAI.CKSAngularSlice.collarLb line 44
  9. def OAI.CKSAngularSlice.collarL line 47
  10. def OAI.CKSAngularSlice.collarF line 50
  11. def OAI.CKSAngularSlice.collarEtaDivR line 53
  12. lemma OAI.CKSAngularSlice.collarQ_slice line 56
  13. lemma OAI.CKSAngularSlice.collarShift_slice line 62
  14. lemma OAI.CKSAngularSlice.collarT_slice line 69
  15. lemma OAI.CKSAngularSlice.collarLb_slice line 75
  16. lemma OAI.CKSAngularSlice.collarF_slice line 81
  17. lemma OAI.CKSAngularSlice.collarEta_slice line 86
  18. lemma OAI.CKSAngularSlice.collarQ_radial line 93
  19. lemma OAI.CKSAngularSlice.collarT_radial line 113
  20. lemma OAI.CKSAngularSlice.collarF_radial line 126
  21. lemma OAI.CKSAngularSlice.collarEta_radial line 149
  22. def OAI.CKSMixedGeometry.sourceTensor line 173