OAI/Geometry/RCD/Transport/RenyiChord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compressed finite-dimensional Rényi chord from the actual RCD inputs

The selected plan has all maximal dyadic midpoints, a uniform density bound, the scalar reduced-CD chord, and continuous endpoint entropy. The full position-dependent CD* estimate remains a separate step.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.exists_compressed_renyi_chord line 19