OAI/Geometry/RCD/Transport/OptimalSubplanSplice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Splicing an actual subplan through its fixed interior marginal

A normalized half-plan is lifted back to the original component mass. Both outside endpoint marginals and the entire untouched half are retained.

  1. theorem OAI.RegularPointCoordinates.exists_optimal_left_subplan_splice line 19