OAI/Geometry/Relativity/CKS/CollarThinInputs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CKSAngularGeometry.CollarCoefficientFields.freezeRadial line 12
2. lemma OAI.CKSAngularGeometry.fieldRaw_freeze line 15
3. lemma OAI.CKSAngularGeometry.freezeRadial_regular line 28
4. def OAI.CKSAngularGeometry.CollarCoefficientFields.ThinBoundedAt line 37
5. lemma OAI.CKSAngularGeometry.freezeRadial_bounded line 46
6. lemma OAI.CKSAngularGeometry.fieldRaw_thin_norm line 58
7. theorem OAI.CKSAngularGeometry.bounded_thin_field_map_DEC line 64