OAI/Geometry/RCD/Transport/AsymmetricMidpointCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An actual compressed midpoint with unequal endpoint bounds

Minimizing excess mass and replacing its saturated region turns the CD support estimate into a density bound. Separate endpoint bounds allow one marginal to concentrate while retaining the contribution of the other.

  1. theorem OAI.RegularPointCoordinates.FullCD.improve_localized_saturation_asymmetric line 20
  2. theorem OAI.RegularPointCoordinates.FullCD.localized_excess_minimizer_zero_asymmetric line 121
  3. theorem OAI.RegularPointCoordinates.FullCD.exists_compressed_midpoint_asymmetric line 190