OAI/Geometry/CylinderCovering/Barycentric/Coverage.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.BarycentricRadial.abs_mul_le_abs_left line 8
2. theorem OAI.CylinderCovering.BarycentricRadial.quadratic_bounds line 13
3. theorem OAI.CylinderCovering.BarycentricRadial.joint_excess_bound line 18
4. theorem OAI.CylinderCovering.BarycentricRadial.capped_alternative line 115
5. theorem OAI.RadialCoordinates.nonnegative_complementary_representations line 140
6. theorem OAI.RadialCoordinates.cap_eq_angular_polynomial line 165
7. theorem OAI.RadialCoordinates.barycentric_simplex_covered line 171