OAI/Geometry/RCD/Transport/NearbySegmentCompression.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compression cost for small endpoint balls

The local segment estimate must be uniform when its endpoints move. The actual Bishop--Gromov lower bound controls both endpoint normalizations.

  1. theorem OAI.RegularPointCoordinates.inverse_mass_le_of_scaled_lower line 18
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.endpoint_ball_compression_bound line 26
  3. theorem OAI.RegularPointCoordinates.compressionBudget_le_of_rescaled_curvature line 50