OAI/Geometry/Relativity/CKS/MassJetRealization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.traceProduct line 11
2. lemma OAI.CKSAngularGeometry.traceProduct_diff line 13
3. lemma OAI.CKSAngularGeometry.actual_traceProductJet line 19
4. lemma OAI.CKSAngularGeometry.inverse_diff_at line 33
5. lemma OAI.CKSAngularGeometry.actual_inverseJets line 48
6. def OAI.CKSAngularGeometry.massNumeratorField line 54
7. def OAI.CKSAngularGeometry.normalizedMassField line 59
8. lemma OAI.CKSAngularGeometry.massNumeratorField_diff line 62
9. lemma OAI.CKSAngularGeometry.actual_massNumeratorJet line 68
10. lemma OAI.CKSAngularGeometry.actual_normalizedMassJet line 76
11. theorem OAI.CKSAngularGeometry.physical_mass_normalized line 94