OAI/Geometry/CylinderCovering/Rational/Schedules.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.minimumShadowArea_le_shadowArea line 14
2. theorem OAI.CylinderCovering.relativeCost_le_familyArea_div_minimum line 22
3. theorem OAI.SlopeRational.finite_sweeps_separate line 36
4. theorem OAI.SlopeRational.strict_finite_cover_of_coverage_cost line 68
5. theorem OAI.SlopeRational.eventually_strict_finite_cover line 93
6. theorem OAI.SlopeRational.paddingSchedules_of_asymptotic line 110