OAI/Geometry/Relativity/CKS/ADMAverage.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CKSADM.surfaceMeasure_real line 12
2. lemma OAI.CKSADM.canonicalF_mean line 16
3. lemma OAI.CKSADM.canonicalF_continuous_sphere line 31
4. def OAI.CKSADM.tailSphereMass line 37
5. lemma OAI.CKSADM.tailSphereMass_continuous line 40
6. lemma OAI.CKSADM.tailSphereMass_mean line 44
7. lemma OAI.CKSADM.tailSphereMass_bound line 52
8. lemma OAI.CKSADM.denominator_lower line 69
9. lemma OAI.CKSADM.rational_mass_error line 76
10. def OAI.CKSADM.reducedEnergy line 97
11. lemma OAI.CKSADM.reducedEnergy_error line 101
12. theorem OAI.CKSADM.reducedEnergy_limit line 132