OAI/Geometry/CylinderCovering/Convexity/RelativeCostComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.CostComparison.shadowArea_nonneg line 11
2. lemma OAI.CylinderCovering.CostComparison.minimumShadowArea_le_shadowArea line 14
3. theorem OAI.CylinderCovering.CostComparison.relativeCost_le_familyArea_div_minimum line 22
4. theorem OAI.CylinderCovering.CostComparison.relativeCost_lt_half_of_familyArea_lt_half line 32
5. theorem OAI.CylinderCovering.CostComparison.triangularRelativeCost_le_totalArea_div_minimum line 40
6. theorem OAI.CylinderCovering.CostComparison.triangularRelativeCost_lt_half_of_totalArea_lt_half line 50