§2.b — the dual of f ∈ Γ₀(H) lies in Γ₀(H), and its dual is f

Proved

MoreauProx.Decomposition.conj_gammaZero_and_conj_conj

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

conjugate-dualityconvex-analysisfenchel-moreaup2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $H$ be a real Hilbert space and $f \in \Gamma_0(H)$ . Let $g = f^{*}$ be the dual function of $f$ , $g(y) = \sup_{x\in H}[(x\mid y) - f(x)]$ . Then

$g \in \Gamma_0(H)$ ;
$f$ is the dual function of $g$ : for every $x \in H$ ,

f(x) = \sup_{y \in H}\,\big[(x \mid y) - g(y)\big].

Together these say that $f \mapsto f^{*}$ is an involution of $\Gamma_0(H)$ (the Fenchel–Moreau theorem). It is what makes the relation " $f$ and $g$ are dual to each other" symmetric, and what makes $\mathrm{prox}_g$ meaningful in Moreau's decomposition theorem.

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Decomposition_ConvexDuality

Formal statement

namespace MoreauProx.Decomposition

open scoped InnerProductSpace

/-- Moreau 1965, §2.b, p. 276: the dual of `f ∈ Γ₀(H)` belongs to `Γ₀(H)`, and `f` is the
dual of its dual. -/
theorem conj_gammaZero_and_conj_conj {H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → EReal) (hf : GammaZero f) :
    GammaZero (conj f) ∧ conj (conj f) = f := by sorry

end MoreauProx.Decomposition

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), pp. 276–277, §2.b (after (2.2))

Read-back

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

Let $H$ be a real Hilbert space. Let $f : H \to [-\infty,+\infty]$ belong to $\Gamma_0(H)$ , meaning:

$f$ never equals $-\infty$ ;
$f$ is finite at some point;
the epigraph $\{(x,r) \in H\times\mathbb R : f(x)\le r\}$ is convex;
$f$ is lower semicontinuous.

Let $f^*(y) = \sup_{x\in H}(\langle x,y\rangle - f(x))$ be the conjugate, computed in the extended reals, where terms with $f(x) = +\infty$ equal $-\infty$ .

The theorem asserts two things together:

$f^* \in \Gamma_0(H)$ . So $f^*$ never equals $-\infty$ , is finite at some point, has a convex epigraph in $H \times \mathbb R$ , and is lower semicontinuous.
The biconjugate equals $f$ at every point:

f^{**}(x) \;=\; \sup_{y\in H}\big(\langle x,y\rangle - f^*(y)\big) \;=\; f(x) \qquad \text{for all } x \in H.

This includes the points where $f(x) = +\infty$ .

Degenerate case. When $H = \{0\}$ , $f(0) = c$ is real. The statement then says that $f^*(0) = -c$ is real and $f^{**}(0) = c$ .

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