OAI/Geometry/Relativity/CKS/NonroundConstraints.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CKSFrame.TensorData line 10
  2. def OAI.CKSFrame.tensor line 17
  3. def OAI.CKSFrame.tangential line 22
  4. def OAI.CKSFrame.tau line 25
  5. def OAI.CKSFrame.covariantTensor line 28
  6. def OAI.CKSFrame.momentum line 32
  7. def OAI.CKSFrame.energy line 35
  8. def OAI.CKSFrame.shearNormSq line 38
  9. def OAI.CKSFrame.tauNormSq line 41
  10. def OAI.CKSFrame.etaNormSq line 43
  11. def OAI.CKSFrame.shearTau line 45
  12. def OAI.CKSFrame.etaAcceleration line 48
  13. def OAI.CKSFrame.etaDiv line 51
  14. def OAI.CKSFrame.tauDiv line 54
  15. def OAI.CKSFrame.normalLieEta line 58
  16. def OAI.CKSFrame.accelTensor line 61
  17. lemma OAI.CKSFrame.tensor_trace line 64
  18. lemma OAI.CKSFrame.energy_decomposition line 67
  19. lemma OAI.CKSFrame.normal_momentum_decomposition line 75
  20. lemma OAI.CKSFrame.tangential_momentum_decomposition line 82
  21. theorem OAI.CKSFrame.constraint_decomposition line 89