OAI/Geometry/RCD/Harmonic/ResidualCollapse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Collapse of the residual factor from sharp dimensional packing

This is a consequence of an actual product approximation. It does not assume that the source is already close to Euclidean space, nor that the residual metric factor is geodesic.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.residual_factor_small line 18