OAI/Geometry/RCD/Heat/CompactHeatDualSaturation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Saturated optimal limits of the actual heat-kernel couplings

The kernel scaling, exact marginals, common action subsequence and dual potentials are all constructed. No optimality or dual-saturation input is used. The cost retains the original ambient metric.

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