OAI/Geometry/RCD/Heat/PairedHeatActionLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common subsequence for the forward and backward heat factors

Both factors retain their actual endpoint laws and noise parameters. Every interior time has local uniform convergence on this one sequence.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.paired_heat_action_limits line 20