OAI/Geometry/Relativity/CKS/MixedMassRealization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSMixedGeometry.traceProduct line 13
2. lemma OAI.CKSMixedGeometry.traceProduct_diff line 15
3. lemma OAI.CKSMixedGeometry.actual_traceProductJet line 21
4. lemma OAI.CKSMixedGeometry.inverse_diff_at line 35
5. lemma OAI.CKSMixedGeometry.actual_inverseJets line 50
6. def OAI.CKSMixedGeometry.massNumeratorField line 56
7. def OAI.CKSMixedGeometry.normalizedMassField line 61
8. lemma OAI.CKSMixedGeometry.massNumeratorField_diff line 64
9. lemma OAI.CKSMixedGeometry.actual_massNumeratorJet line 70
10. lemma OAI.CKSMixedGeometry.actual_normalizedMassJet line 78