OAI/Geometry/RCD/Transport/RenyiTreeChord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All-time scalar Rényi control and endpoint continuity

A fixed maximal midpoint tree has the exact scalar reduced-CD chord at every time. Weak upper semicontinuity and this lower bound give genuine continuity of its Rényi entropy at both endpoints.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.plan_following_renyi_tree_chord line 21