OAI/Geometry/Relativity/CKS/SourcePhysicalTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.CKSMixedGeometry.SourceTensorFields line 14
2. structure OAI.CKSMixedGeometry.SourceTensorFields.RegularAt line 19
3. structure OAI.CKSMixedGeometry.SourceTensorFields.ComponentBounds line 24
4. def OAI.CKSMixedGeometry.SourceTensorFields.logFields line 29
5. def OAI.CKSMixedGeometry.sourceRadialK line 34
6. def OAI.CKSMixedGeometry.sourceOriginalL line 36
7. def OAI.CKSMixedGeometry.sourceOriginalEta line 41
8. def OAI.CKSMixedGeometry.sourceOriginalTau line 44
9. lemma OAI.CKSMixedGeometry.source_tensor_log_regular line 48
10. lemma OAI.CKSMixedGeometry.sourceOriginalL_pullback line 54
11. lemma OAI.CKSMixedGeometry.sourceOriginalEta_pullback line 64
12. lemma OAI.CKSMixedGeometry.sourceOriginalTau_pullback line 74
13. lemma OAI.CKSMixedGeometry.sourceRadialK_regular line 83
14. lemma OAI.CKSMixedGeometry.sourceOriginalL_regular line 88
15. lemma OAI.CKSMixedGeometry.sourceOriginalEta_regular line 104
16. lemma OAI.CKSMixedGeometry.sourceOriginalTau_regular line 118