OAI/Geometry/RCD/Harmonic/RadialContractionFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Quantitative radial density at small times

The proved signed Gaussian lower bound for the CD coefficient suffices: the derivative of its inverse volume factor is n + kappa D²/3.

  1. def OAI.RegularPointCoordinates.radialContractionFloor line 16
  2. def OAI.RegularPointCoordinates.radialContractionDensity line 19
  3. theorem OAI.RegularPointCoordinates.radialContractionFloor_pos line 22
  4. theorem OAI.RegularPointCoordinates.radialContractionFloor_ne_top line 27
  5. theorem OAI.RegularPointCoordinates.radialContractionFloor_le_tau line 30
  6. theorem OAI.RegularPointCoordinates.radialContractionDensity_zero line 48
  7. theorem OAI.RegularPointCoordinates.radialContractionDensity_pos line 52
  8. theorem OAI.RegularPointCoordinates.radialContractionFloor_inv_pow line 56
  9. theorem OAI.RegularPointCoordinates.radialContractionDensity_hasDerivAt_zero line 70
  10. theorem OAI.RegularPointCoordinates.radialContractionDensity_secant_tendsto line 85