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

Proved

MoreauProx.Characterization.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 and $f \in \Gamma_0(H)$ . For every $z \in H$ the function

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

has a strict minimum: there is $x \in H$ such that $\Phi(x) < \Phi(u)$ for every $u \ne x$ .

This is what makes the proximal point $\operatorname{prox}_f z$ well defined for every $f \in \Gamma_0(H)$ and every $z$ : the strict minimum gives both existence and uniqueness of the minimizer.

Formalization Note Values are computed in EReal; the strict inequality is required against every other point, which is stronger than the existence of a minimizer.

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_GammaZero
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

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 →
      ((‖x - z‖ ^ 2 / 2 : ℝ) : EReal) + f x < ((‖u - z‖ ^ 2 / 2 : ℝ) : EReal) + f u := by sorry

end MoreauProx.Characterization

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: a complete real inner product space. Let $f:H\to[-\infty,+\infty]$ belong to $\Gamma_0(H)$ , meaning that $f$ never takes the value $-\infty$ , is finite at some point, has a convex real epigraph $\{(x,t)\in H\times\mathbb R: f(x)\le t\}$ , and is lower semicontinuous. Let $z\in H$ .

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

\tfrac12\|x-z\|^2+f(x)\ <\ \tfrac12\|u-z\|^2+f(u)\quad\text{for every }u\in H\text{ with }u\neq x,

with the strict inequality taken in $[-\infty,+\infty]$ .

So $x$ is the unique strict minimizer of $u\mapsto\frac12\|u-z\|^2+f(u)$ . When $H$ has more than one point, the strict inequality against any $u$ forces the left side to be below $+\infty$ , so $f(x)$ is finite.

Degenerate case. If $H=\{0\}$ , there is no $u\neq x$ . The statement then holds trivially with $x=0$ and says nothing about $f$ .

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