OAI/Geometry/RCD/Transport/OptimalMidpointSplice.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Splicing an optimal half-plan while preserving the other half

This interface retains the complete family of marginals on each half, including the shared midpoint needed for length-class localization.

  1. theorem OAI.RegularPointCoordinates.exists_optimal_midpoint_splice line 19
  2. theorem OAI.RegularPointCoordinates.exists_optimal_left_splice line 45