OAI/Geometry/RCD/Transport/LengthRootMaximality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Maximality of an entire length component

The initial speed identity ensures that any optimal replacement stays in the same length class. Its interior mass is disjoint from the untouched class, so exact Rényi additivity transfers maximality to the component.

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