OAI/Geometry/CylinderCovering/Convexity/NormalFrame.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderNormalFrame.positive_mass_eq_negative_mass line 10
  2. theorem OAI.CylinderNormalFrame.sum_abs_eq_twice_positive_mass line 23
  3. theorem OAI.CylinderNormalFrame.sum_sq_le_half_sq_sum_abs line 37
  4. theorem OAI.CylinderNormalFrame.sum_normal line 55
  5. theorem OAI.CylinderNormalFrame.inner_normal_zero line 59
  6. theorem OAI.CylinderNormalFrame.inner_normal_one line 64
  7. theorem OAI.CylinderNormalFrame.inner_normal_two line 69
  8. theorem OAI.CylinderNormalFrame.inner_normal_three line 74
  9. theorem OAI.CylinderNormalFrame.sum_sq_inner_normal line 79
  10. theorem OAI.CylinderNormalFrame.normal_unit line 90
  11. theorem OAI.CylinderNormalFrame.frameCost_lower_bound line 98
  12. theorem OAI.CylinderNormalFrame.edgeDirection_unit line 114
  13. theorem OAI.CylinderNormalFrame.frameCost_edgeDirection line 117
  14. theorem OAI.CylinderNormalFrame.barycentricCost_lower_bound line 126
  15. theorem OAI.CylinderNormalFrame.sum_normal_mul line 144
  16. theorem OAI.CylinderNormalFrame.isLeast_frameCost line 152
  17. theorem OAI.CylinderNormalFrame.barycentricEdge_sum line 159
  18. theorem OAI.CylinderNormalFrame.barycentricEdge_unit line 162
  19. theorem OAI.CylinderNormalFrame.barycentricCost_edge line 168
  20. theorem OAI.CylinderNormalFrame.isLeast_barycentricCost line 173