OAI/Geometry/Relativity/CKS/CollarRawNull.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSAngularGeometry.RawNullInput line 12
2. abbrev OAI.CKSAngularGeometry.nr line 13
3. def OAI.CKSAngularGeometry.rawNullMap line 15
4. def OAI.CKSAngularGeometry.rawNullOriginal line 17
5. def OAI.CKSAngularGeometry.rawNullDomain line 18
6. lemma OAI.CKSAngularGeometry.rawNullDomain_open line 19
7. lemma OAI.CKSAngularGeometry.rawNullMap_regular line 21
8. lemma OAI.CKSAngularGeometry.rawNullMap_smooth line 25
9. lemma OAI.CKSAngularGeometry.rawNullResidual_smooth line 32
10. lemma OAI.CKSAngularGeometry.rawNullPadding_smooth line 36
11. lemma OAI.CKSAngularGeometry.rawNullOriginal_diff line 44
12. theorem OAI.CKSAngularGeometry.raw_null_uniform line 53