Proposition 9.b — φ is less convex than 𝒬 ⟺ its dual is more convex than 𝒬 ⟺ φ is a prox primitive

Proved

MoreauProx.Characterization.prox_primitive_tfae

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

conjugate-dualityconvex-analysisp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-map

Let $H$ be a real Hilbert space, $\mathcal{Q}(z) = \tfrac12\|z\|^2$ , and $\varphi : H \to [-\infty, +\infty]$ . The following three properties are equivalent:

$\varphi \in \Gamma_0(H)$ and $\varphi$ is less convex than $\mathcal{Q}$ ;
$\varphi \in \Gamma_0(H)$ and the dual function of $\varphi$ is more convex than $\mathcal{Q}$ ;
$\varphi$ is the primitive of a prox map: there is $g \in \Gamma_0(H)$ such that, with $f$ the dual function of $g$ ,

\varphi(z) = \tfrac12 \|\operatorname{prox}_g z\|^2 + f(\operatorname{prox}_f z) \quad \text{for all } z \in H.

The proposition describes the primitives of prox maps intrinsically, without reference to $g$ . Together with Proposition 10.b it reduces the characterization of prox maps (Corollary 10.c) to a statement about subgradients.

Formalization Note The equivalence is stated as List.TFAE. Property 3 does not itself assume $\varphi \in \Gamma_0(H)$ , as in the paper; "less/more convex than $\mathcal{Q}$ " uses an auxiliary convex function with values in $]-\infty, +\infty]$ (Définition 9.b).

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_ConvexityVsQ
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem prox_primitive_tfae {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (φ : H → EReal) :
    List.TFAE
      [GammaZero φ ∧ LessConvexThanQ φ,
       GammaZero φ ∧ MoreConvexThanQ (conj φ),
       IsProxPrimitive φ] := by sorry

end MoreauProx.Characterization

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 288, Définition 9.b; p. 289, Proposition 9.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, with no hypotheses. The statement asserts that the following three conditions are equivalent.

$\varphi\in\Gamma_0(H)$ , and there is a $\gamma$ with the following properties: $\gamma$ never takes the value $-\infty$ , has a convex real epigraph, and satisfies $\varphi(z)+\gamma(z)=\frac12\|z\|^2$ for all $z$ . Under the $[-\infty,+\infty]$ addition rules, this forces $\varphi$ and $\gamma$ to be finite everywhere, so the condition means that $\frac12\|\cdot\|^2-\varphi$ is a real convex function.
$\varphi\in\Gamma_0(H)$ , and there is a $\gamma$ that never takes the value $-\infty$ , has a convex real epigraph (the value $+\infty$ is allowed), and satisfies

\varphi^*(y)=\tfrac12\|y\|^2+\gamma(y)\quad\text{for all }y,\qquad\text{where }\varphi^*(y)=\sup_x\big(\langle x,y\rangle-\varphi(x)\big).

There is a $g\in\Gamma_0(H)$ such that, for every $z$ ,

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

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$ .

Membership in $\Gamma_0(H)$ means: never $-\infty$ , finite somewhere, convex real epigraph, and lower semicontinuous.

Degenerate cases.

Condition 3 does not explicitly require $\varphi\in\Gamma_0(H)$ ; the equivalence asserts that it follows.
If $H=\{0\}$ , condition 1 holds exactly when $\varphi(0)$ is real. The equivalence then claims the same for conditions 2 and 3.

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