OAI/Geometry/RCD/Transport/QuadraticGeodesicUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness forced by the quadratic distance identities

The identity is tested at a point on a competing geodesic. Its right hand side then vanishes, so no nonbranching assumption is needed.

  1. theorem OAI.RegularPointCoordinates.quadratic_geodesic_unique line 16
  2. theorem OAI.RegularPointCoordinates.quadratic_radial_distance line 38