OAI/Geometry/Relativity/CKS/BoostTransport.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSLorentz.normalizeAmbient line 11
  2. def OAI.CKSLorentz.weightedPullback line 13
  3. def OAI.CKSLorentz.normalizedPullback line 16
  4. lemma OAI.CKSLorentz.boostField_tangent line 19
  5. lemma OAI.CKSLorentz.normalizeAmbient_smooth line 22
  6. lemma OAI.CKSLorentz.normalizeAmbient_sphere line 25
  7. lemma OAI.CKSLorentz.norm_derivative_sphere line 28
  8. lemma OAI.CKSLorentz.normalizeAmbient_fderiv_tangent line 37
  9. lemma OAI.CKSLorentz.flowPhi_smooth_at line 46
  10. lemma OAI.CKSLorentz.flowPhi_nonzero line 50
  11. lemma OAI.CKSLorentz.flowPhi_fderiv line 54
  12. lemma OAI.CKSLorentz.flowPhi_derivative line 66
  13. lemma OAI.CKSLorentz.flowPhi_transport line 73
  14. lemma OAI.CKSLorentz.weightedPullback_smooth_at line 94
  15. lemma OAI.CKSLorentz.weightedPullback_spatial_derivative line 102
  16. lemma OAI.CKSLorentz.weightedPullback_transport line 118
  17. lemma OAI.CKSLorentz.normalizedPullback_smooth line 137
  18. lemma OAI.CKSLorentz.normalizedPullback_spatial line 145
  19. lemma OAI.CKSLorentz.normalizedPullback_sphere line 150
  20. lemma OAI.CKSLorentz.normalizedPullback_fderiv_tangent line 154
  21. lemma OAI.CKSLorentz.normalizedPullback_transport line 167