OAI/Geometry/Relativity/CKS/BoostFlow.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSLorentz.flowEnergy line 10
  2. def OAI.CKSLorentz.flowCoeff line 11
  3. def OAI.CKSLorentz.flowD line 12
  4. def OAI.CKSLorentz.flowS line 13
  5. def OAI.CKSLorentz.flowPhi line 14
  6. def OAI.CKSLorentz.boostField line 16
  7. def OAI.CKSLorentz.flowDLinear line 18
  8. def OAI.CKSLorentz.flowSLinear line 19
  9. lemma OAI.CKSLorentz.flowEnergy_pos line 22
  10. lemma OAI.CKSLorentz.flowEnergy_sq line 23
  11. lemma OAI.CKSLorentz.flowEnergy_add_pos line 24
  12. lemma OAI.CKSLorentz.flowEnergy_gt line 25
  13. lemma OAI.CKSLorentz.flowEnergy_smooth line 30
  14. lemma OAI.CKSLorentz.flowCoeff_smooth line 32
  15. lemma OAI.CKSLorentz.flowD_smooth line 35
  16. lemma OAI.CKSLorentz.flowS_smooth line 38
  17. lemma OAI.CKSLorentz.flowD_eq line 42
  18. lemma OAI.CKSLorentz.flowS_eq line 44
  19. lemma OAI.CKSLorentz.flowD_pos line 50
  20. lemma OAI.CKSLorentz.flowS_norm line 53
  21. lemma OAI.CKSLorentz.flowPhi_norm line 58
  22. lemma OAI.CKSLorentz.flowEnergy_derivative line 62
  23. lemma OAI.CKSLorentz.flowCoeff_derivative line 70
  24. lemma OAI.CKSLorentz.flowD_derivative line 82
  25. lemma OAI.CKSLorentz.flowS_derivative line 86
  26. lemma OAI.CKSLorentz.flowD_fderivative line 90
  27. lemma OAI.CKSLorentz.flowS_fderivative line 93
  28. lemma OAI.CKSLorentz.flowD_transport line 98
  29. lemma OAI.CKSLorentz.flowS_transport line 106