AlmostMonotoneAllTimes.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform convergence at every time from a vanishing one-sided error

Good times bracket any prescribed interior time. The common Lipschitz bound of the limit and the vanishing monotonicity error squeeze every spatial value with the same error.

theorem OAI.RegularPointCoordinates.almost_monotone_uniform_all_times line 17