OAI/Geometry/RCD/Heat/CompactHeatUniformDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounded compression for the actual heat interpolation

The bound holds at every point, time and noise index. It is constructed from the original endpoint densities, not supplied as an additional input.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationDensity_uniform_bound line 25