OAI/Geometry/CylinderCovering/Convexity/GeneralCapArea.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.GeneralCapArea.continuous_profile line 11
2. lemma OAI.CylinderCovering.GeneralCapArea.continuous_idealSpeed line 12
3. lemma OAI.CylinderCovering.GeneralCapArea.continuous_idealDensity line 13
4. lemma OAI.CylinderCovering.GeneralCapArea.coefficient_polynomial line 17
5. lemma OAI.CylinderCovering.GeneralCapArea.coefficient_integral line 23
6. lemma OAI.CylinderCovering.GeneralCapArea.idealDensity_integral line 37
7. lemma OAI.CylinderCovering.GeneralCapArea.perturbed_product_remainder line 50
8. lemma OAI.CylinderCovering.GeneralCapArea.profile_bounds line 93
9. lemma OAI.CylinderCovering.GeneralCapArea.square_difference line 103
10. theorem OAI.CylinderCovering.GeneralCapArea.capDensity_error line 112
11. lemma OAI.CylinderCovering.GeneralCapArea.integral_error line 180
12. theorem OAI.CylinderCovering.GeneralCapArea.partition_area_error line 194
13. lemma OAI.CylinderCovering.GeneralCapArea.partition_monotone line 222
14. theorem OAI.CylinderCovering.GeneralCapArea.general_cap_area_expansion line 234
15. theorem OAI.CylinderCovering.GeneralCapArea.strict_half_of_area_error line 265
16. theorem OAI.CylinderCovering.GeneralCapArea.exists_uniform_smallness line 273