OAI/Geometry/RCD/Heat/CompactHeatContinuousLawLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One continuous limit curve for the actual compact heat laws

All interior times share the same noise subsequence. The probability curve is constructed from the actual heat densities and retains the same uniform density bound; every ambient L1 function can be tested at every time.

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