Fenchel–Moreau biconjugation

Proved

ConvexOptimization.fenchel_biconjugate_eq_self

by Shuze Chen · Aug 11, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexanalysisconvexoptimizationlog-concavity

The Fenchel–Moreau theorem: a convex function equals its own biconjugate.

Let $f : \mathbb{R}^n \to \mathbb{R}$ be convex on all of $\mathbb{R}^n$ (and finite-valued), with conjugate $f^{*}(y) = \sup_x(\langle x,y\rangle - f(x))$ and biconjugate $f^{**}(x) = \sup_y(\langle x,y\rangle - f^{*}(y))$ . Then

f^{**}(x) \;=\; f(x) \qquad \text{for every } x \in \mathbb{R}^n .

Since $f^{**}$ is by construction the supremum of all affine functions lying below $f$ , the theorem says a convex function is exactly the upper envelope of its affine minorants — the analytic counterpart of the statement that a closed convex set is the intersection of the halfspaces containing it, and thus a direct descendant of the separating hyperplane theorem.

Conjugation is therefore an involution on this class of functions, which is what makes dual descriptions lossless: for a convex problem, dualizing twice returns the original problem, and the duality gap of a nonconvex problem measures precisely the distance from $f$ to $f^{**}$ .

Formalization Note Finiteness of $f$ is built into its type EuclideanSpace ℝ (Fin n) → ℝ, and convexity is ConvexOn ℝ Set.univ f; a finite-valued convex function on all of $\mathbb{R}^n$ is automatically continuous, so no closedness hypothesis is needed. The conclusion equates an EReal value with the coercion of a real number, which also asserts finiteness of $f^{**}(x)$ . Source: B&V §3.3.2, p. 94.

Preamble

import Mathlib
import Definitions.Def_fenchelConjugate
import Definitions.Def_fenchelBiconjugate

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.fenchel_biconjugate_eq_self {n : ℕ}
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : ConvexOn ℝ Set.univ f)
    (x : EuclideanSpace ℝ (Fin n)) :
    fenchelBiconjugate f x = (f x : EReal) := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 94, §3.3.2 (the biconjugate; f** = f for closed convex f)

Read-back

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

Theorem statement. Let $f : \mathbb{R}^n \to \mathbb{R}$ be a total, everywhere-finite function that is convex on the whole space (ConvexOn over the universal set: $f(ax+by) \le a f(x) + b f(y)$ for all $x, y$ and all $a, b \ge 0$ with $a + b = 1$ ; no continuity, closedness, or lower-semicontinuity hypothesis appears). Then for every $x \in \mathbb{R}^n$ , the extended-real number $f^{**}(x) = \sup_{y}\big(\langle x, y\rangle - f^*(y)\big)$ equals the real number $f(x)$ (as an element of $[-\infty,+\infty]$ ). Here $f^*(y) = \sup_{x'}(\langle x', y\rangle - f(x')) \in \mathbb{R}\cup\{+\infty\}$ , and the outer subtraction is extended-real, with the convention that finite $-\ (+\infty) = -\infty$ ; so terms with $f^*(y) = +\infty$ contribute $-\infty$ to the supremum. The equality in particular asserts that this supremum is finite (neither $+\infty$ nor $-\infty$ ) and has exactly the value $f(x)$ . The case $n = 0$ (one-point space, $f$ a single real value, the inner product always $0$ ) is included.

Human review

Endorsed by Community (Bot) · Aug 11, 2026
Endorsed by Shuze Chen · Aug 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph