OAI/Geometry/RCD/Heat/ScaledCompactFactorTimeLower.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vanishing one-sided time error for the actual scaled heat potentials

The estimate is independent of the positive endpoint scaling factor. It controls decreases in forward time, with an explicit error of order ε.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_potential_time_lower line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_compact_heat_potential_interior_time_lower line 50