Proposition 4.a — Moreau's decomposition: z = x + y with x, y conjugate iff x = prox_f z, y = prox_g z

Proved

MoreauProx.Characterization.moreau_decomposition

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, let $f \in \Gamma_0(H)$ , and let $g$ be the dual function of $f$ . For all $x, y, z \in H$ the following are equivalent:

$z = x + y$ and $f(x) + g(y) = (x \mid y)$ ;
$x = \operatorname{prox}_f z$ and $y = \operatorname{prox}_g z$ , i.e. $x$ minimizes $u \mapsto \tfrac12\|u - z\|^2 + f(u)$ and $y$ minimizes $u \mapsto \tfrac12\|u - z\|^2 + g(u)$ .

In short, every $z \in H$ splits uniquely as $z = \operatorname{prox}_f z + \operatorname{prox}_g z$ , and the two parts are conjugate points for the pair $(f, g)$ . This is the key proposition of the paper: the results of Sections 5–10 are derived from it.

Formalization Note The paper assumes $f, g \in \Gamma_0(H)$ dual to each other; we assume $f \in \Gamma_0(H)$ and $g = f^*$ , which the paper's hypothesis implies, so the statement is at least as strong. " $x = \operatorname{prox}_f z$ " is stated as " $x$ minimizes the proximal objective", which is equivalent because the minimizer is unique (Proposition 3.a).

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_Prox
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem moreau_decomposition {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f g : H → EReal) (hf : GammaZero f) (hg : g = conj f) (x y z : H) :
    (z = x + y ∧ f x + g y = ((⟪x, y⟫_ℝ : ℝ) : EReal)) ↔ (IsProx f z x ∧ IsProx g z y) := by sorry

end MoreauProx.Characterization

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 280, Proposition 4.a

Read-back

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

Let $H$ be a real Hilbert space. Let $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. Let $g$ be its conjugate,

g(y)=\sup_{x\in H}\big(\langle x,y\rangle-f(x)\big),

computed in $[-\infty,+\infty]$ with $a-(+\infty)=-\infty$ .

For all $x,y,z\in H$ , the statement asserts that the following are equivalent:

$z=x+y$ and $f(x)+g(y)=\langle x,y\rangle$ , where the sum is taken in $[-\infty,+\infty]$ and equals the real number $\langle x,y\rangle$ ;
$x$ minimizes $u\mapsto\frac12\|u-z\|^2+f(u)$ over $H$ , and $y$ minimizes $u\mapsto\frac12\|u-z\|^2+g(u)$ over $H$ . Each minimization means " $\le$ the value at every $u$ ", in $[-\infty,+\infty]$ .

The statement does not assume $g\in\Gamma_0(H)$ ; $g$ is simply the conjugate of $f$ . The right side refers to the minimizer property itself, not to the chosen $\operatorname{prox}$ value.

Degenerate case. If $H=\{0\}$ , then $x=y=z=0$ and $g(0)=-f(0)$ . Both sides then reduce to statements that hold for any real $f(0)$ .

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