Prove2Me

Lemma A.4 — if lim inf⁡f≠lim sup⁡f\liminf f\neq\limsup f, some α\alpha in between is exceeded along β\beta-separated times

Proved
SDEConvexOpt.lemma_A_4

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-optimizationgradient-flowmartingalesp2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-differential-equations

Let f:R+→Rf:\mathbb R_+\to\mathbb R with lim inf⁡t→∞f(t)≠lim sup⁡t→∞f(t)\liminf_{t\to\infty}f(t)\neq\limsup_{t\to\infty}f(t). Then there is a real constant α\alpha with

lim inf⁡t→∞f(t)<α<lim sup⁡t→∞f(t)\liminf_{t\to\infty}f(t)<\alpha<\limsup_{t\to\infty}f(t)

such that for every β>0\beta>0 there is a sequence (tk)k∈N(t_k)_{k\in\mathbb N} with

f(tk)>α,tk+1>tk+β,∀k∈N.f(t_k)>\alpha,\qquad t_{k+1}>t_k+\beta,\qquad\forall k\in\mathbb N .

The lemma provides the separated times in the contradiction argument for lim⁡∥∇f(X(t))∥=0\lim\|\nabla f(X(t))\|=0.

Differences from the source:

  • encoding: lim inf⁡\liminf, lim sup⁡\limsup of a real function → computed in EReal; reason: they may be ±∞\pm\infty for an unbounded ff; a real-valued liminf would give junk values
  • encoding: (tk)k∈N⊂R(t_k)_{k\in\mathbb N}\subset\mathbb R → tk∈R≥0t_k\in\mathbb R_{\ge0}; reason: ff is only defined on R+\mathbb R_+, so f(tk)f(t_k) requires tk≥0t_k\ge0
Preamble
import Mathlib

open MeasureTheory ProbabilityTheory Filter
open scoped NNReal ENNReal Topology InnerProductSpace
Formal statement
namespace SDEConvexOpt

/-- Lemma A.4 of Maulen S., Fadili, Attouch, arXiv:2207.02750v1, p.32: let `f : ℝ₊ → ℝ` with
`lim inf_{t→∞} f(t) ≠ lim sup_{t→∞} f(t)`. Then there exists a constant `α`, satisfying
`lim inf_{t→∞} f(t) < α < lim sup_{t→∞} f(t)`, such that for every `β > 0` there is a sequence
`(t_k)_{k∈ℕ}` with `f(t_k) > α` and `t_{k+1} > t_k + β` for all `k ∈ ℕ`.

**Formalization Note** `ℝ₊` is `ℝ≥0`. The `lim inf` and `lim sup` are taken in `EReal` (they may
be `±∞` for unbounded `f`), and `α` is real. The sequence takes values in `ℝ≥0`, the domain of
`f`. -/
theorem lemma_A_4 (f : ℝ≥0 → ℝ)
    (hf : liminf (fun t => (f t : EReal)) atTop ≠ limsup (fun t => (f t : EReal)) atTop) :
    ∃ α : ℝ, liminf (fun t => (f t : EReal)) atTop < (α : EReal) ∧
      (α : EReal) < limsup (fun t => (f t : EReal)) atTop ∧
      ∀ β : ℝ, 0 < β → ∃ tk : ℕ → ℝ≥0, ∀ k : ℕ, α < f (tk k) ∧ (tk k : ℝ) + β < tk (k + 1) := by sorry

end SDEConvexOpt
Source
Maulen S., Fadili, Attouch, An SDE perspective on stochastic convex optimization, arXiv:2207.02750v1, Lemma A.4, p.32
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph