OAI/Geometry/Relativity/CKS/CollarShiftJet.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CKSAngularGeometry.ShiftInput line 11
2. def OAI.CKSAngularGeometry.raisedMixedJet line 12
3. def OAI.CKSAngularGeometry.shiftRegion line 14
4. lemma OAI.CKSAngularGeometry.productThreeJet_zero_right line 16
5. lemma OAI.CKSAngularGeometry.raisedMixedJet_zero line 22
6. lemma OAI.CKSAngularGeometry.raisedMixedJet_smooth line 26
7. lemma OAI.CKSAngularGeometry.shiftRegion_open line 36
8. theorem OAI.CKSAngularGeometry.shift_uniform_lipschitz line 40
9. theorem OAI.CKSAngularGeometry.normalized_shift_bound line 56
10. lemma OAI.CKSAngularGeometry.actual_raisedMixedJet line 87