OAI/Geometry/Relativity/CKS/PhysicalFrameTensor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CKSFrame.extractTensor line 12
  2. lemma OAI.CKSFrame.extractTensor_complete line 19
  3. def OAI.CKSAngularGeometry.frameTensor line 38
  4. def OAI.CKSAngularGeometry.frameTensorData line 41
  5. def OAI.CKSAngularGeometry.frameTensorDerivativeData line 44
  6. lemma OAI.CKSAngularGeometry.frameTensor_hermitian line 48
  7. lemma OAI.CKSAngularGeometry.frameTensorData_exact line 54
  8. lemma OAI.CKSAngularGeometry.frameTensorDerivativeData_exact line 59
  9. def OAI.CKSAngularGeometry.actualFrameTensorCovariant line 71
  10. def OAI.CKSAngularGeometry.actualFrameMomentum line 77
  11. def OAI.CKSAngularGeometry.actualFrameEnergy line 82
  12. lemma OAI.CKSAngularGeometry.actualFrame_covariant_representation line 87
  13. lemma OAI.CKSAngularGeometry.actualFrame_momentum_representation line 97
  14. lemma OAI.CKSAngularGeometry.actualFrame_energy_representation line 106