OAI/Geometry/RCD/Heat/CompactHeatBackwardSource.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform quadratic lower sources for the actual backward factor

On the first half of the interpolation, the backward heat time stays away from zero relative to the noise scale. Only the original endpoint density and its boundedness are used.

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