OAI/Geometry/RCD/Transport/RenyiMidpointInequality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compressed midpoint with the original finite-CD lower value

The entropy-maximizing midpoint dominates the original CD midpoint. The distortion integral still uses that original CD witness; no equality of the two endpoint couplings is asserted.

  1. theorem OAI.RegularPointCoordinates.RenyiMaximizingPlan.renyiIntegral_le line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_finite_renyi_midpoint line 42