OAI/Geometry/RCD/Transport/RenyiScalarMidpoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The scalar reduced-CD bound at each selected midpoint

The original FullCD witness and the selected midpoint may have different couplings. The uniform length bound removes the coupling dependence in this scalar estimate. No equality of the two plans is assumed.

  1. theorem OAI.RegularPointCoordinates.RenyiMaximizingPlan.renyiIntegral_le_of_integrable line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.renyiNode_scalar_midpoint line 36