OAI/Geometry/CylinderCovering/Convexity/OrthonormalHeightComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.OrthonormalHeight.k_pos line 9
2. lemma OAI.CylinderCovering.OrthonormalHeight.k_ne line 10
3. lemma OAI.CylinderCovering.OrthonormalHeight.k_sq line 11
4. lemma OAI.CylinderCovering.OrthonormalHeight.upperHeight_scale line 16
5. lemma OAI.CylinderCovering.OrthonormalHeight.lowerHeight_scale line 21
6. lemma OAI.CylinderCovering.OrthonormalHeight.cap_dictionary line 26
7. theorem OAI.CylinderCovering.OrthonormalHeight.error_bound line 41
8. theorem OAI.CylinderCovering.OrthonormalHeight.cubic_coverage line 61
9. theorem OAI.CylinderCovering.OrthonormalHeight.orthonormal_height_comparison line 96