OAI/Geometry/RCD/Coordinates/CoordinateHeatInput.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The heat bounds actually used by the coordinate construction

Jiang--Li--Zhang (2016), Theorem 1.2, implies these bounds. The lower estimate is needed only when squared distance is a fixed multiple of time, and only for times at most one. The full two-sided Gaussian estimate gives these local comparisons.

  1. structure OAI.RegularPointCoordinates.HasCoordinateHeatBounds line 20
  2. instance OAI.RegularPointCoordinates.(instance at line 28) line 28
  3. theorem OAI.RegularPointCoordinates.HasGaussianHeatBounds.toCoordinate line 34
  4. theorem OAI.RegularPointCoordinates.HasCoordinateHeatBounds.upper_five line 63