OAI/Geometry/RCD/Transport/RenyiTreeCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform compression on the fixed maximal midpoint tree

Dyadic marginals are fixed before compactness. Their common density bound extends to every time by weak continuity and closedness of domination.

  1. theorem OAI.RegularPointCoordinates.isClosed_probability_domination line 18
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.plan_following_renyi_tree_compression line 26