OAI/Geometry/RCD/Heat/ScaledHeatLimitTimeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing viscosity in the time increment estimate

This uses the prescribed global limit and subsequence. The constant in the limiting bound depends only on the local cylinder, not on the test.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_limit_pairing_time_bound line 22