OAI/Geometry/RCD/Transport/DimensionalPotential.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An actual compact optimal potential with the dimensional subgradient bound

This is the bounded square-root-core specialization of EKS Theorem 3.17, equation (3.24). The potential and the transport plan are constructed from the original RCD structure; no dimensional evolution inequality is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.sqrt_core_dimensional_potential line 22