OAI/Geometry/CylinderCovering/Angular/Aperture.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AngularAperture.transverse_nonneg line 9
2. lemma OAI.AngularAperture.transverse_half line 13
3. lemma OAI.AngularAperture.transverse_le line 17
4. lemma OAI.AngularAperture.transverse_lipschitz line 23
5. lemma OAI.AngularAperture.tau_sq_le line 45
6. lemma OAI.AngularAperture.level_strictMonoOn line 48
7. lemma OAI.AngularAperture.root_remainder line 70
8. lemma OAI.AngularAperture.roots_lipschitz line 105