OAI/Geometry/RCD/Transport/FiniteContinuousChord.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite length-partition bounds at all times

The weighted scalar sum is continuous. Upper semicontinuity of the actual Rényi entropy extends its dyadic lower bound to the whole interval.

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