OAI/Geometry/Relativity/CKS/BondiCharge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSLorentz.aspectPullback line 13
2. lemma OAI.CKSLorentz.nullDirection_smooth line 16
3. lemma OAI.CKSLorentz.aspectPullback_smooth line 21
4. lemma OAI.CKSLorentz.rawCharge_integrable line 30
5. lemma OAI.CKSLorentz.rawCharge_test line 35
6. lemma OAI.CKSLorentz.transformedCharge_test line 40
7. theorem OAI.CKSLorentz.rawCharge_lorentz line 72
8. theorem OAI.CKSLorentz.bondiCharge_lorentz line 80