OAI/Geometry/RCD/Transport/FullReducedMidpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Full CD controls the exact reduced coefficient at a midpoint

The result covers zero distance and curvature, and the infinite coefficient at a conjugate point. It is the only full-to-reduced distortion comparison required by the midpoint construction.

  1. theorem OAI.RegularPointCoordinates.reduced_midpoint_le_tau line 17