OAI/Geometry/CylinderCovering/Radial/Coordinates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RadialCoordinates.barycentricPoint_sum line 12
  2. theorem OAI.RadialCoordinates.barycentricPoint_mem_iff line 17
  3. theorem OAI.RadialCoordinates.barycentricPoint_reconstruct line 34
  4. theorem OAI.RadialCoordinates.barycentricPoint_distance_squared line 42
  5. theorem OAI.RadialCoordinates.canonicalPoint_distance_squared line 49
  6. theorem OAI.RadialCoordinates.canonicalPoint_distance line 57
  7. theorem OAI.RadialCoordinates.canonicalPoint_mem_of_simplex line 67
  8. theorem OAI.RadialCoordinates.exists_positive_radial_representation line 77
  9. theorem OAI.RadialCoordinates.radial_representation_sum_difference line 86
  10. theorem OAI.RadialCoordinates.interior_complementary_representations line 94
  11. theorem OAI.RadialCoordinates.velocity_quadratic_identity line 118
  12. theorem OAI.RadialCoordinates.cap_obstruction_identity line 124
  13. theorem OAI.RadialCoordinates.cap_obstruction_positive line 130
  14. theorem OAI.RadialCoordinates.capPolynomial_angular_expansion line 136
  15. theorem OAI.RadialCoordinates.speedSquared_expansion line 142
  16. theorem OAI.RadialCoordinates.integral_quartic line 147
  17. theorem OAI.RadialCoordinates.capPolynomial_integral line 159
  18. theorem OAI.RadialCoordinates.speedSquared_integral line 165
  19. theorem OAI.RadialCoordinates.barycentric_quadratic_coefficient_integral line 171
  20. theorem OAI.RadialCoordinates.frozen_intercept_identity line 181
  21. theorem OAI.RadialCoordinates.transverse_unit_norm line 188
  22. theorem OAI.RadialCoordinates.frozen_intercept_remainder line 193
  23. theorem OAI.RadialCoordinates.frozen_intercept_enclosure line 203