OAI/Geometry/RCD/Transport/LengthComponentCompression.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compression at the length of a component, independent of total diameter

Normalization cancels from the inherited density budget. This estimate is uniform for fixed length windows when bounded endpoint approximations grow.

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