OAI/Geometry/RCD/Heat/CompactHeatInterpolationLaws.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual interpolation laws are uniformly tight

A single finite measure dominates every noise index and every interior time. It is built from the established uniform density and Gaussian tail.

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationLaw line 28
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationLaw_integral line 32
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.interpolationLaw_finite_dominator line 45