OAI/Geometry/Relativity/CKS/SchwarzschildCharges.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSSchwarzschild.sphere_coordinate_integral line 13
2. lemma OAI.CKSSchwarzschild.constant_bondi_charge line 22
3. lemma OAI.CKSSchwarzschild.bondi_charge line 32
4. lemma OAI.CKSSchwarzschild.source_minimum_area line 35
5. lemma OAI.CKSSchwarzschild.numerical_equality line 39