OAI/Geometry/RCD/Transport/RenyiPlanVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Power-entropy transport reweighting

The finite-dimensional power and its matching primitive have the same initial variation after changing the initial marginal to the reference measure. The error is controlled by the actual test-plan square estimate.

  1. theorem OAI.RegularPointCoordinates.memLp_renyi_negative_power line 20
  2. theorem OAI.RegularPointCoordinates.memLp_renyiDualPower line 29
  3. theorem OAI.RegularPointCoordinates.planInitialSecant_renyi_reweight_error line 50
  4. theorem OAI.RegularPointCoordinates.planInitialSecant_renyi_reweight_tendsto line 106