OAI/Geometry/CylinderCovering/Convexity/ConvexBodyShadowBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.compact_shadow_measure_ne_top line 14
  2. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.shadowArea_mono line 26
  3. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.minimumShadowArea_mono line 31
  4. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.exists_inscribed_tetrahedron line 40
  5. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.minimumShadowArea_pos line 58
  6. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.exists_uniform_positive_shadow_bound line 71
  7. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.shadow_measure_pos_and_lt_top line 77
  8. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.relativeCost_le_familyArea_div_minimum line 85
  9. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.relativeCost_lt_half_of_familyArea_lt_half line 90
  10. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.triangularRelativeCost_le_totalArea_div_minimum line 97
  11. theorem OAI.CylinderCovering.ConvexBodyShadowBounds.triangularRelativeCost_lt_half_of_totalArea_lt_half line 103