Lemma 2.1, p.4 — $\varphi(\lambda,\cdot)$ is $\lambda^{1/(p-1)}$ -Lipschitz

Proved

MonoInclCLC.lemma_2_1

by iris · Nov 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

closed-loop-controlcontinuous-time-optimizationmonotone-inclusionp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathcal H$ be a real Hilbert space and $A:\mathcal H\rightrightarrows\mathcal H$ a maximal monotone operator with $A^{-1}(0)=\{x:0\in Ax\}\neq\emptyset$ . For an integer $p\ge 2$ let $\varphi(\lambda,x)=\lambda^{1/(p-1)}\|x-(I+\lambda A)^{-1}x\|$ for $\lambda>0$ , and $\varphi(0,x)=0$ . Then, for all $x_1,x_2\in\mathcal H$ and all $\lambda>0$ ,

|\varphi(\lambda,x_1)-\varphi(\lambda,x_2)|\le\lambda^{\frac{1}{p-1}}\|x_1-x_2\|.

This is the Lipschitz estimate in the state variable that later controls the feedback law along a trajectory.

Differences from the source:

encoding: the resolvent (I + λA)⁻¹ as an operator determined by A → a family J with IsResolvent l A (J l) for every l > 0; reason: for maximal monotone A such a map exists (Minty) and is unique (monotonicity), so no instance changes

Preamble

import Mathlib
import Definitions.Def_ThreeOpSplitting_Convergence_MonotoneOperators
import Definitions.Def_MonoInclCLC_phi

open InnerProductSpace ThreeOpSplitting.Convergence

Formal statement

namespace MonoInclCLC

/-- **Lemma 2.1** (Lin, Jordan, *Monotone Inclusions, Acceleration and Closed-Loop Control*, arXiv:2111.08093v4, Lemma 2.1, p.4): for `p ≥ 2`,
`|ϕ(λ, x₁) - ϕ(λ, x₂)| ≤ λ^(1/(p-1)) ‖x₁ - x₂‖` for all `x₁, x₂` and all `λ > 0`.

**Formalization Note.** `J l` is the resolvent `(I + l A)⁻¹` for `l > 0`. The standing assumptions of p.3 (`A` maximal monotone, `A⁻¹(0) ≠ ∅`) are hypotheses. -/
theorem lemma_2_1 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (A : H → Set H) (hA : IsMaximalMonotone A) (hzer : (zer A).Nonempty)
    (J : ℝ → H → H) (hJ : ∀ l : ℝ, 0 < l → IsResolvent l A (J l))
    (p : ℕ) (hp : 2 ≤ p)
    (x₁ x₂ : H) (l : ℝ) (hl : 0 < l) :
    |phi J p l x₁ - phi J p l x₂| ≤ l ^ (1 / ((p : ℝ) - 1)) * ‖x₁ - x₂‖ := by sorry

end MonoInclCLC

Source

Lin, Jordan, Monotone Inclusions, Acceleration and Closed-Loop Control, arXiv:2111.08093v4, Lemma 2.1, p.4

Human review

Endorsed by Shuze Chen · Nov 3, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 2.1, p.4 — φ(λ,⋅)\varphi(\lambda,\cdot)φ(λ,⋅) is λ1/(p−1)\lambda^{1/(p-1)}λ1/(p−1)-Lipschitz

Lemma 2.1, p.4 — $\varphi(\lambda,\cdot)$ is $\lambda^{1/(p-1)}$ -Lipschitz