OAI/Geometry/Relativity/CKS/CollarAngularWeighted.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.commonAngularMomentum line 12
2. def OAI.CKSAngularGeometry.rawAngularMatrix line 15
3. def OAI.CKSAngularGeometry.rawAngularResidual line 17
4. def OAI.CKSAngularGeometry.rawPositiveDomain line 20
5. lemma OAI.CKSAngularGeometry.rawAngularMatrix_smooth line 22
6. lemma OAI.CKSAngularGeometry.rawPositiveDomain_open line 27
7. lemma OAI.CKSAngularGeometry.rawAngularResidual_smooth line 33
8. lemma OAI.CKSAngularGeometry.commonAngularMomentum_factor line 44
9. lemma OAI.CKSAngularGeometry.rawPositiveFamily_regular line 51
10. theorem OAI.CKSAngularGeometry.bounded_raw_common_angular line 64