OAI/Geometry/Relativity/CKS/PhysicalFrameContractions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSAngularGeometry.orthonormal_frame_gram line 12
2. lemma OAI.CKSAngularGeometry.orthonormal_frame_completeness line 19
3. lemma OAI.CKSAngularGeometry.frame_tensor_matrix line 24
4. lemma OAI.CKSAngularGeometry.frame_trace_exact line 36
5. lemma OAI.CKSAngularGeometry.symmetric_square_trace line 43
6. lemma OAI.CKSAngularGeometry.frame_tensor_norm_exact line 54
7. theorem OAI.CKSAngularGeometry.actualFrameEnergy_coordinate line 75