OAI/Geometry/RCD/Heat/CompactHeatSecondVariationLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrated second variation on the original heat-law subsequence

The two limiting derivatives are constructed from actual interpolation means. All strict interior intervals share these same limits.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.integrated_second_variation_limit line 26