PointedGeodesicWithin.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Images of geodesics contained in the measured approximation domain

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_within line 17