Proposition 7.b — the primitive φ of prox_g lies in Γ₀(H) and its dual is g + ½‖·‖²

Proved

MoreauProx.Characterization.primitive_gammaZero_conj

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, $f \in \Gamma_0(H)$ and $g$ its dual function. Let $\varphi$ be the primitive of $\operatorname{prox}_g$ ,

\varphi(z) = \tfrac12 \|\operatorname{prox}_g z\|^2 + f(\operatorname{prox}_f z).

Then $\varphi \in \Gamma_0(H)$ , and the dual function of $\varphi$ is

\theta(y) = g(y) + \tfrac12 \|y\|^2 .

Since $\varphi(z) = \inf_u \big[\tfrac12\|u - z\|^2 + f(u)\big]$ (Remark 7.c), this identifies $\varphi$ as the inf-convolution of $f$ with $\tfrac12\|\cdot\|^2$ and computes its dual; it is used for Propositions 9.b and 10.b.

Formalization Note $\varphi$ is real-valued and is viewed as an EReal-valued function to apply the definitions of $\Gamma_0(H)$ and of the dual function; the identity of duals is an equality of EReal-valued functions on $H$ (where $g$ may take the value $+\infty$ ).

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_Prox
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem primitive_gammaZero_conj {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f g : H → EReal) (hf : GammaZero f) (hg : g = conj f) :
    GammaZero (fun z => ((primitive f g z : ℝ) : EReal)) ∧
      conj (fun z => ((primitive f g z : ℝ) : EReal)) =
        fun y => g y + ((‖y‖ ^ 2 / 2 : ℝ) : EReal) := by sorry

end MoreauProx.Characterization

Source

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

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

Here:

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

Viewing $\Phi$ as a function into $[-\infty,+\infty]$ , the statement asserts two things:

$\Phi\in\Gamma_0(H)$ .
Its conjugate is

\Phi^*(y)=g(y)+\tfrac12\|y\|^2\quad\text{for every }y\in H,

with the sum in $[-\infty,+\infty]$ , so $\Phi^*(y)=+\infty$ wherever $g(y)=+\infty$ .

Degenerate case. If $H=\{0\}$ , then $\Phi(0)=f(0)$ and $g(0)=-f(0)$ , and the claims reduce to identities about the real number $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