PointedGeodesicInterpolation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Images of short source geodesics approach Euclidean affine segments

This estimate applies to every geodesic in a bounded endpoint region; no choice of optimal plan or pointwise regularity of the approximation map is required.

theorem OAI.RegularPointCoordinates.pointed_geodesic_interpolation line 17