Proposition 10.b — φ ∈ Γ₀(H) with ∂φ contracting distances ⟺ the three properties of 9.b

Proved

MoreauProx.Characterization.prox_primitive_iff_subgrad_contracts

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 $\varphi : H \to [-\infty, +\infty]$ . Consider the property

(IV) $\varphi \in \Gamma_0(H)$ and the (a priori multivalued) map $z \mapsto \partial\varphi(z)$ contracts distances:

x \in \partial\varphi(z),\ x' \in \partial\varphi(z') \ \Longrightarrow\ \|x - x'\| \le \|z - z'\|.

Then (IV) is equivalent to each of the three properties of Proposition 9.b:

$\varphi \in \Gamma_0(H)$ and $\varphi$ is less convex than $\mathcal{Q}(z) = \tfrac12\|z\|^2$ ;
$\varphi \in \Gamma_0(H)$ and the dual function of $\varphi$ is more convex than $\mathcal{Q}$ ;
$\varphi$ is the primitive of $\operatorname{prox}_g$ for some $g \in \Gamma_0(H)$ .

This is the step from the convexity comparisons of Section 9 to a metric condition on subgradients, on which the characterization of prox maps (Corollary 10.c) rests.

Formalization Note The contraction condition is the paper's definition for multivalued maps (§10.a); it places no condition at points where $\partial\varphi(z)$ is empty. Subgradients are in the affine-minorant form, which agrees with the paper's definition on $\Gamma_0(H)$ .

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_ConvexityVsQ
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem prox_primitive_iff_subgrad_contracts {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (φ : H → EReal) :
    ((GammaZero φ ∧ ContractsDistances (subgrad φ)) ↔ (GammaZero φ ∧ LessConvexThanQ φ)) ∧
    ((GammaZero φ ∧ ContractsDistances (subgrad φ)) ↔
      (GammaZero φ ∧ MoreConvexThanQ (conj φ))) ∧
    ((GammaZero φ ∧ ContractsDistances (subgrad φ)) ↔ IsProxPrimitive φ) := by sorry

end MoreauProx.Characterization

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 291, §10.a and Proposition 10.b

Read-back

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

Let $H$ be a real Hilbert space and let $\varphi:H\to[-\infty,+\infty]$ be arbitrary.

Let condition (A) be: $\varphi\in\Gamma_0(H)$ , and the subdifferential $\partial\varphi$ contracts distances. That is,

\|y-y'\|\le\|z-z'\|\quad\text{whenever }y\in\partial\varphi(z),\ y'\in\partial\varphi(z').

Here $\partial\varphi(z)$ is the set of $y$ such that $\varphi(z)$ is finite and $\varphi(z)+\langle u-z,y\rangle\le\varphi(u)$ for all $u$ . Membership in $\Gamma_0(H)$ means: never $-\infty$ , finite somewhere, convex real epigraph, and lower semicontinuous.

The statement asserts three equivalences, each with (A) on the left:

(A) holds if and only if $\varphi\in\Gamma_0(H)$ and $\varphi+\gamma=\frac12\|\cdot\|^2$ for some $\gamma$ that never takes the value $-\infty$ and has a convex real epigraph. This forces $\varphi$ and $\gamma$ to be real-valued everywhere.
(A) holds if and only if $\varphi\in\Gamma_0(H)$ and $\varphi^*=\frac12\|\cdot\|^2+\gamma$ for some $\gamma$ that never takes the value $-\infty$ and has a convex real epigraph (the value $+\infty$ is allowed). Here $\varphi^*(y)=\sup_x(\langle x,y\rangle-\varphi(x))$ .
(A) holds if and only if there is a $g\in\Gamma_0(H)$ with

\varphi(z)=\tfrac12\|\operatorname{prox}_g z\|^2+\operatorname{re}\big(g^*(\operatorname{prox}_{g^*}z)\big)\quad\text{for all }z.

Here $\operatorname{prox}_h(z)$ is a chosen minimizer of $u\mapsto\frac12\|u-z\|^2+h(u)$ (or $0$ if none exists), and $\operatorname{re}(\pm\infty)=0$ .

Degenerate cases.

The distance-contracting condition holds trivially wherever $\partial\varphi$ is empty.
With $z=z'$ , it forces each $\partial\varphi(z)$ to have at most one element.
If $H=\{0\}$ , then $\partial\varphi(0)$ is $\{0\}$ when $\varphi(0)$ is real, and (A) holds exactly when $\varphi(0)$ is real.

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