OAI/Geometry/RCD/Transport/RenyiSubplanMaximality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Maximality passes to separated transport components

Replacing a subplan preserves optimality. If both the original component and its replacement are disjoint from the untouched midpoint mass, exact Rényi additivity transfers maximality to that component.

  1. theorem OAI.RegularPointCoordinates.RenyiMaximizingPlan.subplan_comparison line 20