OAI/Geometry/CylinderCovering/Convexity/GeneralCapCoverage.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.GeneralCap.quartic_bounds line 7
2. theorem OAI.CylinderCovering.GeneralCap.first_crossing line 13
3. theorem OAI.CylinderCovering.GeneralCap.weighted_errors line 28
4. theorem OAI.CylinderCovering.GeneralCap.rough_angle line 44
5. theorem OAI.CylinderCovering.GeneralCap.rough_square line 64
6. theorem OAI.CylinderCovering.GeneralCap.cross_term_bound line 77
7. theorem OAI.CylinderCovering.GeneralCap.radial_identity line 102
8. theorem OAI.CylinderCovering.GeneralCap.radial_lower_est line 114
9. theorem OAI.CylinderCovering.GeneralCap.radial_failure line 121
10. theorem OAI.CylinderCovering.GeneralCap.radial_exclusion line 152
11. theorem OAI.CylinderCovering.GeneralCap.node_bounds line 227
12. theorem OAI.CylinderCovering.GeneralCap.angular_selection line 240
13. theorem OAI.CylinderCovering.GeneralCap.coordinate_coverage line 283
14. theorem OAI.CylinderCovering.GeneralCap.half_lt_cap line 331
15. theorem OAI.CylinderCovering.GeneralCap.exists_positive_threshold line 347