OAI/Geometry/RCD/Transport/QuadraticGeodesicGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Metric operations supplied by exact quadratic geodesics

Exact quadratic distance identities determine unique geodesics and radial similarities, including their composition and reversal laws.

  1. structure OAI.RegularPointCoordinates.QuadraticGeodesicGeometry line 17
  2. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.unique line 28
  3. def OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial line 34
  4. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial_zero line 36
  5. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial_one line 37
  6. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.dist_radial line 39
  7. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial_lipschitz line 47
  8. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial_antilipschitz line 53
  9. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial_self line 61
  10. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.radial_comp line 66
  11. theorem OAI.RegularPointCoordinates.QuadraticGeodesicGeometry.reverse_path line 81