OAI/Geometry/RCD/Transport/OptimalExactSplice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact path laws of an optimal midpoint splice

The gluing construction retains each entire half-path law. This lets geometric length bounds pass to a replacement, beyond its one-time marginals.

  1. theorem OAI.RegularPointCoordinates.joinMatched_subpath_left line 20
  2. theorem OAI.RegularPointCoordinates.joinMatched_subpath_right line 26
  3. theorem OAI.RegularPointCoordinates.exists_optimal_midpoint_splice_exact line 31