OAI/Geometry/Relativity/CKS/CollarExpansionInputNorm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.packExpansion line 11
2. lemma OAI.CKSAngularGeometry.actualExpansionInput_pack line 15
3. lemma OAI.CKSAngularGeometry.packExpansion_reference line 19
4. lemma OAI.CKSAngularGeometry.packExpansion_sub line 22
5. lemma OAI.CKSAngularGeometry.packExpansion_norm line 26
6. theorem OAI.CKSAngularGeometry.actualExpansionInput_norm line 52
7. def OAI.CKSAngularGeometry.normalizedShift line 62
8. lemma OAI.CKSAngularGeometry.normalizedShift_realized line 65