Proposition 5.b — prox_f is nonexpansive, hence continuous

Proved

MoreauProx.Characterization.prox_nonexpansive

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-analysisnonexpansive-mapsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-map

Let $H$ be a real Hilbert space and $f \in \Gamma_0(H)$ . For all $z, z' \in H$ ,

\|\operatorname{prox}_f z - \operatorname{prox}_f z'\| \le \|z - z'\|,

so the map $\operatorname{prox}_f$ is continuous from $H$ (norm topology) to $H$ (norm topology).

Nonexpansiveness of proximal maps is the basis of their use in numerical methods, and it is one of the two properties (with the subgradient selection) that characterize prox maps in Corollary 10.c.

Formalization Note $\operatorname{prox}_f$ is the choice-based function of the definitions file; under $f \in \Gamma_0(H)$ it returns the unique minimizer of $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ . Both clauses of the paper's statement, the inequality and the continuity, are stated.

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_Prox
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem prox_nonexpansive {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f : H → EReal) (hf : GammaZero f) :
    (∀ z z' : H, ‖prox f z - prox f z'‖ ≤ ‖z - z'‖) ∧ Continuous (prox f) := by sorry

end MoreauProx.Characterization

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 282, Proposition 5.b, (5.2)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $H$ be a real Hilbert space and $f\in\Gamma_0(H)$ : $f:H\to[-\infty,+\infty]$ never takes the value $-\infty$ , is finite somewhere, has a convex real epigraph, and is lower semicontinuous.

$\operatorname{prox}_f(z)$ is defined as a chosen minimizer of $u\mapsto\frac12\|u-z\|^2+f(u)$ . If there are several, one is chosen by the axiom of choice. If there is none, the value is $0$ .

The statement asserts two things:

\|\operatorname{prox}_f(z)-\operatorname{prox}_f(z')\|\le\|z-z'\|\quad\text{for all }z,z'\in H,

and the map $\operatorname{prox}_f:H\to H$ is continuous.

Degenerate case. If $H=\{0\}$ , both claims are trivially true.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph