OAI/Geometry/RCD/Transport/DimensionalH1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The dimensional optimal potential for bounded compact Sobolev densities

The proved square-root probability recovery and a common-support potential subsequence pass the exact finite-dimensional bound to the actual density.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.quantitative_H1_dimensional_subgradient line 19