OAI/Geometry/RCD/Transport/RadialMidpointRigidity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integral rigidity of a radial midpoint coupling

The quadratic triangle defect is nonnegative. The two marginal moments and the optimal half-cost force its integral to vanish, so every path of the replacement plan is still radial almost everywhere.

  1. theorem OAI.RegularPointCoordinates.radial_midpoint_rigidity_of_moments line 21