Proposition 3.a — the proximal objective ½‖u − z‖² + f(u) has a strict minimum

Proved

MoreauProx.Decomposition.prox_strict_minimum

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 $z \in H$ . Then the function

\Phi(u) = \tfrac12 \|u - z\|^2 + f(u), \qquad u \in H,

with values in $]-\infty,+\infty]$ , has a strict minimum: there is a point $x \in H$ such that $\Phi(x) < \Phi(u)$ for every $u \ne x$ .

The minimizer is therefore unique; Moreau denotes it $\mathrm{prox}_f z$ , the proximal point of $z$ relative to $f$ (3.b). For $f$ the indicator function of a nonempty closed convex set $C$ , it is the nearest-point projection onto $C$ .

Formalization Note "Strict minimum" is stated literally, as strict inequality at every other point, which gives both existence and uniqueness of the minimizer. The sum is computed in EReal.

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Decomposition_ConvexDuality

Formal statement

namespace MoreauProx.Decomposition

open scoped InnerProductSpace

/-- Moreau 1965, Proposition 3.a, p. 278: for `f ∈ Γ₀(H)` and every `z ∈ H`, the function
`Φ(u) = ½‖u − z‖² + f(u)` has a strict minimum: a point `x` with `Φ(x) < Φ(u)` for all `u ≠ x`. -/
theorem prox_strict_minimum {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] (f : H → EReal) (hf : GammaZero f) (z : H) :
    ∃ x : H, ∀ u : H, u ≠ x → proxObjective f z x < proxObjective f z u := by sorry

end MoreauProx.Decomposition

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 278, Proposition 3.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 : H \to [-\infty,+\infty]$ belong to $\Gamma_0(H)$ , meaning:

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

Let $z \in H$ be arbitrary. Define, in the extended reals,

\Phi(u) = \tfrac12\|u-z\|^2 + f(u).

The theorem asserts that there exists $x \in H$ such that

\Phi(x) < \Phi(u) \qquad \text{for every } u \in H \text{ with } u \neq x.

So $x$ is a strict global minimiser of $\Phi$ . Uniqueness of such an $x$ follows from the strict inequality, but it is not stated separately.

Degenerate cases. If $H = \{0\}$ , there is no $u \neq x$ , so the statement holds trivially with $x = 0$ . If $H$ has a nonzero element, the strict inequality against some $u$ forces $\Phi(x) < +\infty$ , and therefore $f(x)$ is finite.

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