OAI/Geometry/RCD/Heat/AlmostMonotoneTimeLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convergence between dense time slices

A vanishing one-sided time error suffices for convergence at every continuity point of the bounded monotone envelope.

  1. theorem OAI.RegularPointCoordinates.almost_monotone_time_limit line 16