OAI/Geometry/RCD/Transport/RenyiMidpointShort.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Distance-sensitive compression of the actual Rényi midpoint

The capacity uses the bound on all optimal transport distances, rather than the containing support ball. It therefore scales under subdivision and yields a uniform compression budget for the dyadic construction.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.renyi_midpoint_compressed_short line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_renyi_maximizing_midpoint_short line 92