OAI/Geometry/RCD/Transport/ReducedDistanceLimit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Distance continuity of reduced distortion, including zero length

At zero length the sharp Gaussian lower bound and the linear upper bound squeeze the hyperbolic ratio to its continuous value.

  1. theorem OAI.RegularPointCoordinates.sigma_nonpos_ne_top line 15
  2. theorem OAI.RegularPointCoordinates.sigma_nonpos_ne_zero line 24
  3. theorem OAI.RegularPointCoordinates.sigma_nonpos_length_tendsto line 40