OAI/Geometry/RCD/Transport/ConcentratedMidpointLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A radial limiting plan whose midpoint retains bounded density

Only midpoint compression is imposed before the endpoint concentrates. Compactness of the actual bounded geodesic plans retains the initial law, the Dirac final law, and the same midpoint density bound.

  1. theorem OAI.RegularPointCoordinates.exists_concentrated_midpoint_limit line 22