OAI/Geometry/RCD/Transport/RadialTimeCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A compressed marginal at a prescribed radial time

Actual CD replacements minimize excess mass at the chosen time. Only the source capacity enters the resulting bound; bounded endpoint support is used for compactness, independently of the sharper distortion supports.

  1. theorem OAI.RegularPointCoordinates.FullCD.improve_time_saturation line 20
  2. theorem OAI.RegularPointCoordinates.FullCD.time_excess_minimizer_zero line 121
  3. theorem OAI.RegularPointCoordinates.FullCD.exists_compressed_time line 190