A function that is monotone near every point of $[0,T]$ is monotone on $[0,T]$

Proved

HryniewiczCriterion.monotoneOn_Icc_of_forall_local

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysis

Let $E:\mathbb{R}\to\mathbb{R}$ and $T\in\mathbb{R}$ . Suppose every $t_0\in[0,T]$ has a $\delta>0$ such that $E(s)\le E(t)$ whenever $s\le t$ both lie in $[0,T]\cap(t_0-\delta,t_0+\delta)$ . Then $E$ is monotone on $[0,T]$ . No continuity of $E$ is assumed (it is applied to integer-valued functions). Proof idea: the balls $(t_0-\delta,t_0+\delta)$ cover the compact $[0,T]$ ; with a Lebesgue number $r$ , any two points of $[0,T]$ at distance $<r$ lie in one ball, and $[s,t]$ is crossed in steps of length $r/2$ .

Preamble

import Mathlib.Data.Real.Basic

Formal statement

theorem HryniewiczCriterion.monotoneOn_Icc_of_forall_local {E : ℝ → ℝ} {T : ℝ}
    (h : ∀ t0 ∈ Set.Icc 0 T, ∃ δ > 0, ∀ s t, s ∈ Set.Icc 0 T → t ∈ Set.Icc 0 T →
      |s - t0| < δ → |t - t0| < δ → s ≤ t → E s ≤ E t) :
    MonotoneOn E (Set.Icc 0 T) := by sorry

Source

Elementary (Lebesgue number lemma); used for the local-to-global monotonicity of the eigen-angle defect in the proof of HryniewiczCriterion.positive_unitary_path_eigenAngleSum_le.

View graph

A function that is monotone near every point of [0,T][0,T][0,T] is monotone on [0,T][0,T][0,T]

A function that is monotone near every point of $[0,T]$ is monotone on $[0,T]$