OAI/Geometry/RCD/Transport/RenyiMidpointCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded density of the actual Rényi-maximizing midpoint

The sharp midpoint capacity controls every Rényi maximizer. The proof first removes singular mass and then uses strict improvement under a bounded replacement of a density superlevel set.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.renyi_midpoint_compressed line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_renyi_maximizing_midpoint line 92