OAI/Geometry/RCD/Transport/PointwiseReduced.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise reduced density interpolation along the actual optimal plan

Every measurable path restriction has the reduced integral bound. All of its marginal densities agree with the original densities along that restriction, so localization gives the pointwise inequality without a Jensen reversal.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.pointwise_reduced_interpolation line 25