Proposition 7.d — the primitive φ is Fréchet differentiable with gradient prox_g z

Proved

MoreauProx.Characterization.primitive_hasGradientAt

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

convex-analysisp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-map

Let $H$ be a real Hilbert space, $f \in \Gamma_0(H)$ and $g$ its dual function, and let $\varphi(z) = \tfrac12 \|\operatorname{prox}_g z\|^2 + f(\operatorname{prox}_f z)$ be the primitive of $\operatorname{prox}_g$ . At every point $z \in H$ , $\varphi$ is Fréchet differentiable and its gradient is

\nabla \varphi(z) = \operatorname{prox}_g z .

This justifies the name "primitive": $\operatorname{prox}_g$ is the gradient of the convex function $\varphi$ . It is the key input for the necessity half of Corollary 10.c.

Formalization Note The gradient is Mathlib's HasGradientAt, which is Fréchet differentiability with derivative $h \mapsto (\operatorname{prox}_g z \mid h)$ . The gradient is $\operatorname{prox}_g z$ , not $\operatorname{prox}_f z$ .

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_Prox
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem primitive_hasGradientAt {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f g : H → EReal) (hf : GammaZero f) (hg : g = conj f) (z : H) :
    HasGradientAt (primitive f g) (prox g z) z := by sorry

end MoreauProx.Characterization

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 286, Proposition 7.d

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$ never takes the value $-\infty$ , is finite somewhere, has a convex real epigraph, and is lower semicontinuous. Let $g=f^*$ , where $g(y)=\sup_x(\langle x,y\rangle-f(x))$ in $[-\infty,+\infty]$ .

Define the real-valued function

\Phi(z)=\tfrac12\|\operatorname{prox}_g(z)\|^2+\operatorname{re}\big(f(\operatorname{prox}_f(z))\big),

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

For every $z\in H$ , the statement asserts that $\Phi$ is Fréchet differentiable at $z$ with gradient $\operatorname{prox}_g(z)$ :

\Phi(z+h)=\Phi(z)+\langle\operatorname{prox}_g(z),h\rangle+o(\|h\|)\quad\text{as }h\to0.

Degenerate case. If $H=\{0\}$ , the claim is trivially true with gradient $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