Prove2Me

(2.3) — Fenchel–Young inequality f(x) + g(y) ≥ (x | y) for f ∈ Γ₀(H) and its dual g

Proved
MoreauProx.Decomposition.fenchel_young

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

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

Let HH be a real Hilbert space, let f∈Γ0(H)f \in \Gamma_0(H) (proper, convex, lower semicontinuous, with values in ]−∞,+∞]]-\infty,+\infty]), and let g=f∗g = f^{*} be its dual function, g(y)=sup⁡x∈H[(x∣y)−f(x)]g(y) = \sup_{x\in H}[(x\mid y) - f(x)]. Then for all x,y∈Hx, y \in H,

f(x)+g(y)  ≥  (x∣y).f(x) + g(y) \;\ge\; (x \mid y).

This is the inequality underlying the notion of conjugate points: xx and yy are called conjugate with respect to ff and gg exactly when equality holds.

Formalization Note The sum is taken in EReal. Because ff never takes the value −∞-\infty and is not identically +∞+\infty, neither f(x)f(x) nor g(y)g(y) is −∞-\infty, so the convention −∞+(+∞)=−∞-\infty + (+\infty) = -\infty never enters.

Preamble
import Mathlib
import Definitions.Def_MoreauProx_Decomposition_ConvexDuality
Formal statement
namespace MoreauProx.Decomposition

open scoped InnerProductSpace

/-- Moreau 1965, (2.3), p. 277: for `f ∈ Γ₀(H)` and its dual `g`,
`f(x) + g(y) ≥ (x | y)` for all `x, y`. -/
theorem fenchel_young {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] (f : H → EReal) (hf : GammaZero f) (x y : H) :
    ((⟪x, y⟫_ℝ : ℝ) : EReal) ≤ f x + conj f y := by sorry

end MoreauProx.Decomposition
Source
Moreau, Proximité et dualité dans un espace hilbertien, Bull. Soc. Math. France 93 (1965), p. 277, §2.c, (2.3)
Read-back

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

Let HH be a real Hilbert space, meaning a complete real inner product space. Let f:H→[−∞,+∞]f : H \to [-\infty, +\infty] belong to Γ0(H)\Gamma_0(H). That is:

  • ff never takes the value −∞-\infty;
  • ff is finite at some point;
  • the epigraph {(x,r)∈H×R:f(x)≤r}\{(x, r) \in H \times \mathbb R : f(x) \le r\} is convex;
  • ff is lower semicontinuous.

Let f∗(y)=sup⁡x∈H(⟨x,y⟩−f(x))f^*(y) = \sup_{x \in H} (\langle x, y\rangle - f(x)) be its conjugate, computed in the extended reals, where a point with f(x)=+∞f(x) = +\infty contributes −∞-\infty.

The theorem asserts that for all x,y∈Hx, y \in H,

⟨x,y⟩  ≤  f(x)+f∗(y),\langle x, y\rangle \;\le\; f(x) + f^*(y),

where the sum is taken in the extended reals, with the convention (+∞)+(−∞)=−∞(+\infty) + (-\infty) = -\infty.

Degenerate cases. If f(x)=+∞f(x) = +\infty, the inequality says ⟨x,y⟩≤+∞+f∗(y)\langle x,y\rangle \le +\infty + f^*(y). This is automatically true unless f∗(y)=−∞f^*(y) = -\infty, and that cannot happen here because ff is finite somewhere. When H={0}H = \{0\}, the statement reads 0≤f(0)+f∗(0)0 \le f(0) + f^*(0) with f(0)f(0) real.

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