(5.1) — conjugate pairs form a monotone relation: (x − x′ | y − y′) ≥ 0

Proved

MoreauProx.Characterization.conjugate_points_monotone

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

convex-analysismonotone-operatorsp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $H$ be a real Hilbert space, $f \in \Gamma_0(H)$ and $g$ its dual function. If $x, y$ and $x', y'$ are two pairs of points conjugate with respect to $f$ and $g$ , that is,

f(x) + g(y) = (x \mid y), \qquad f(x') + g(y') = (x' \mid y'),

then

(x - x' \mid y - y') \ge 0.

The relation " $y \in \partial f(x)$ " is therefore monotone in the sense of Minty. Combined with Moreau's decomposition, this inequality yields the nonexpansiveness of $\operatorname{prox}_f$ (Proposition 5.b).

Formalization Note $f$ and $g$ are EReal-valued, and the conjugacy equalities are equalities in EReal.

Preamble

import Mathlib
import Definitions.Def_MoreauProx_Characterization_GammaZero
open scoped InnerProductSpace

Formal statement

namespace MoreauProx.Characterization

theorem conjugate_points_monotone {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (f g : H → EReal) (hf : GammaZero f) (hg : g = conj f) (x y x' y' : H)
    (hxy : f x + g y = ((⟪x, y⟫_ℝ : ℝ) : EReal))
    (hxy' : f x' + g y' = ((⟪x', y'⟫_ℝ : ℝ) : EReal)) :
    0 ≤ ⟪x - x', y - y'⟫_ℝ := by sorry

end MoreauProx.Characterization

Source

Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 281, §5.a, (5.1)

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 $f^*(y)=\sup_{x}(\langle x,y\rangle-f(x))$ in $[-\infty,+\infty]$ .

Suppose $x,y,x',y'\in H$ satisfy

f(x)+g(y)=\langle x,y\rangle\quad\text{and}\quad f(x')+g(y')=\langle x',y'\rangle,

with the sums taken in $[-\infty,+\infty]$ and equal to these real numbers. Then the statement asserts

\langle x-x',\,y-y'\rangle\ \ge\ 0.

Degenerate cases.

For $x=x'$ or $y=y'$ the conclusion is $0\ge0$ .
If no pair satisfies the hypotheses, the statement is vacuous.
If $H=\{0\}$ , the conclusion is $0\ge0$ .

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