OAI/Geometry/RCD/Heat/CompactHeatMeanTimeBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform time bounds for compact Sobolev tests of the interpolation

The mass-one identity and the actual logarithmic velocity gradient bound control the derivative uniformly in the noise index on each interior time window. This supplies time compactness without a presumed limit curve.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationMean_uniform_lipschitz line 27