OAI/Geometry/Relativity/CKS/PhysicalFrameCurvature.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.frameConnectionField line 11
2. def OAI.CKSAngularGeometry.connectionFieldDerivative line 15
3. lemma OAI.CKSAngularGeometry.connectionFieldDerivative_exact line 24
4. def OAI.CKSAngularGeometry.ActualAdaptedAt line 31
5. lemma OAI.CKSAngularGeometry.frame_connection_actual line 37
6. def OAI.CKSAngularGeometry.actualFrameCurvature line 50
7. def OAI.CKSAngularGeometry.actualFrameScalar line 58
8. lemma OAI.CKSAngularGeometry.physical_curvature_representation line 61
9. theorem OAI.CKSAngularGeometry.physical_scalar_decomposition line 83