Fenchel–Young inequality

Proved

ConvexOptimization.fenchel_young

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

convexanalysisconvexoptimizationlog-concavity

Fenchel's inequality (also called the Fenchel–Young inequality).

For $f : \mathbb{R}^n \to \mathbb{R}$ let $f^{*}(y) = \sup_x(\langle x,y\rangle - f(x))$ be its Fenchel conjugate, with values in $(-\infty,+\infty]$ . Then for all $x, y \in \mathbb{R}^n$ ,

\langle x, y\rangle \;\le\; f(x) + f^{*}(y).

The inequality holds for every function $f$ — no convexity, continuity or measurability is needed — since it is nothing but the definition of the supremum applied at the point $x$ . Equality holds exactly when $y$ is a subgradient of $f$ at $x$ , which is how the inequality is used to characterize the solutions of dual pairs of problems.

Specialized to $f(x) = |x|^{p}/p$ on $\mathbb{R}$ , whose conjugate is $|y|^{q}/q$ with $1/p + 1/q = 1$ , it becomes Young's inequality $xy \le x^{p}/p + y^{q}/q$ , and hence — after integration — Hölder's inequality.

Formalization Note The inequality is stated in EReal, adding the real value $f(x)$ (coerced) to the EReal-valued conjugate, so the case $f^{*}(y) = +\infty$ needs no separate treatment. Source: B&V §3.3.1, p. 94.

Preamble

import Mathlib
import Definitions.Def_fenchelConjugate

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.fenchel_young {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (x y : EuclideanSpace ℝ (Fin n)) :
    ((⟪x, y⟫ : ℝ) : EReal) ≤ (f x : EReal) + fenchelConjugate f y := 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 (Fenchel's inequality; stated unnumbered in the text)

Read-back

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

Theorem statement. For every $n$ , every total function $f : \mathbb{R}^n \to \mathbb{R}$ — no convexity, continuity, or any other hypothesis — and every pair of points $x, y \in \mathbb{R}^n$ , the inequality $\langle x, y\rangle \le f(x) + f^*(y)$ holds in the extended reals, where $f^*(y)$ is the file's fenchelConjugate: $\sup_{x' \in \mathbb{R}^n}\big(\langle x', y\rangle - f(x')\big)$ taken in $[-\infty,+\infty]$ , a value in $\mathbb{R} \cup \{+\infty\}$ . The left side is the finite real $\langle x, y\rangle$ coerced into the extended reals; the right side is extended-real addition of the finite $f(x)$ and $f^*(y)$ , which equals $+\infty$ whenever $f^*(y) = +\infty$ (making the inequality automatic in that case). The particular choice $x' = x$ inside the supremum already gives the term $\langle x, y\rangle - f(x)$ , so the statement's content is exactly this one-term lower bound on the supremum.

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