OAI/Geometry/RCD/Transport/RenyiMeasureReplacement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strict Rényi improvement for a measure replacement

This converts the scalar replacement estimate to the actual measure obtained by replacing a portion of a transport plan.

  1. theorem OAI.RegularPointCoordinates.exists_measure_renyi_increase line 18