OAI/Geometry/CylinderCovering/Convexity/ThresholdInverse.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.ThresholdInverse.inverse_norm_bound line 12
2. theorem OAI.CylinderCovering.ThresholdInverse.inverse_remainder_bound line 23
3. theorem OAI.CylinderCovering.ThresholdInverse.inverse_unique line 33
4. theorem OAI.CylinderCovering.ThresholdInverse.inverse_equations_estimate line 41
5. theorem OAI.CylinderCovering.ThresholdInverse.existsUnique_inverse_on_complete line 54
6. theorem OAI.CylinderCovering.ThresholdInverse.norm_vertical_difference line 87
7. theorem OAI.CylinderCovering.ThresholdInverse.inverse_height_strict line 96