OAI/Geometry/Relativity/CKS/SchwarzschildCKSDecay.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSSchwarzschild.compactDenominator line 11
2. def OAI.CKSSchwarzschild.compactCoefficient line 14
3. def OAI.CKSSchwarzschild.compactRemainder line 17
4. lemma OAI.CKSSchwarzschild.compactDenominator_pos line 20
5. lemma OAI.CKSSchwarzschild.compactCoefficient_smooth line 27
6. lemma OAI.CKSSchwarzschild.compactRemainder_smooth line 31
7. lemma OAI.CKSSchwarzschild.tail_inverse_small line 38
8. lemma OAI.CKSSchwarzschild.radialCoefficient_id line 42
9. lemma OAI.CKSSchwarzschild.radial_decay line 67