OAI/Geometry/RCD/Transport/GlobalRenyiLeftComponent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Global-reference maximality of normalized left length components

A single bounded reference region contains all relevant midpoint measures. Localizing and then restoring the Hausdorff reference preserves the actual variational comparison, including possible singular competitors.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.global_renyi_left_component line 20