OAI/Geometry/CylinderCovering/Simplex/LayerCake.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.SimplexLayerCake.integral_shadow_profile line 11
  2. theorem OAI.CylinderCovering.SimplexLayerCake.integral_eq_area_mul_length_div line 21
  3. theorem OAI.CylinderCovering.SimplexLayerCake.prod_real_eq_integral_fiber line 41
  4. theorem OAI.CylinderCovering.SimplexLayerCake.integrable_fiber_measure line 52
  5. theorem OAI.CylinderCovering.SimplexLayerCake.prod_real_eq_area_mul_length_div line 63
  6. theorem OAI.CylinderCovering.SimplexLayerCake.compact_fiber line 77
  7. theorem OAI.CylinderCovering.SimplexLayerCake.convex_fiber line 86
  8. theorem OAI.CylinderCovering.SimplexLayerCake.le_fiber_measure_iff_exists_segment line 91
  9. theorem OAI.CylinderCovering.SimplexLayerCake.fiber_superlevel_eq_projected_overlap line 113
  10. theorem OAI.CylinderCovering.SimplexLayerCake.fiber_measure_le_of_chord_bound line 130
  11. theorem OAI.CylinderCovering.SimplexLayerCake.compact_convex_prod_volume_of_overlap_profile line 144