(2.2) — Fenchel–Young inequality with its equality case

Proved

RockafellarMaxMono.Maximality.fenchel_young_eq_iff

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

convex-analysisconvex-conjugatep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $V$ be a real Banach space with dual $V^*$ , and let $f$ be a lower semicontinuous proper convex function on $V$ with conjugate $f^*$ . Then for every $x \in V$ and $x^* \in V^*$ ,

f(x) + f^*(x^*) \ \ge\ \langle x, x^* \rangle ,

with equality if and only if $x^* \in \partial f(x)$ .

This is display (2.2) of the paper. Applied with $V = E^*$ and $f^*$ in place of $f$ it also gives display (2.4), which relates $f^{**}$ , $f^*$ and $\partial f^*$ ; both are used to pass between subgradients and equality in the Fenchel–Young inequality.

Formalization Note The paper writes $f(x) + f^*(x^*) - \langle x, x^*\rangle \ge 0$ ; we state the equivalent form with the pairing on the other side, so that no extended-real subtraction appears. The space is an arbitrary real Banach space $V$ (the paper's $E$ ), so that the statement applies to $E^*$ as well.

Preamble

import Mathlib
import Definitions.Def_RockafellarMaxMono_Shared_ProperConvex
import Definitions.Def_RockafellarMaxMono_Shared_Subdiff
import Definitions.Def_RockafellarMaxMono_Shared_Conj

Formal statement

namespace RockafellarMaxMono.Maximality

theorem fenchel_young_eq_iff {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [CompleteSpace V] (f : V → EReal) (hf : Shared.ProperConvex f) (hlsc : LowerSemicontinuous f) :
    ∀ (x : V) (x' : StrongDual ℝ V),
      ((x' x : ℝ) : EReal) ≤ f x + Shared.conj f x' ∧
        (f x + Shared.conj f x' = ((x' x : ℝ) : EReal) ↔ x' ∈ Shared.subdiff f x) := by sorry

end RockafellarMaxMono.Maximality

Source

Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), p. 210, (2.2)

Read-back

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

Setting. $V$ is a real Banach space (a complete normed space) and $V^*$ is its continuous dual. The function $f : V \to \overline{\mathbb{R}}$ takes values in the extended reals $\overline{\mathbb{R}} = [-\infty, +\infty]$ . There are two hypotheses on $f$ :

$f$ satisfies the predicate Shared.ProperConvex, an imported definition not shown in this declaration's text. The name suggests "proper convex function", but its exact conditions cannot be unfolded here.
$f$ is lower semicontinuous on $V$ with the norm topology.

Two more imported operations appear, also not shown here:

$f^*(x^*)$ stands for Shared.conj f at $x^* \in V^*$ . The name suggests the Fenchel conjugate $\sup_x \,(x^*(x) - f(x))$ .
$\partial f(x) \subseteq V^*$ stands for Shared.subdiff f at $x$ . The name suggests the subdifferential.

Claim. For every $x \in V$ and every $x^* \in V^*$ , both of the following hold:

x^*(x) \;\le\; f(x) + f^*(x^*) \quad \text{in } \overline{\mathbb{R}},

f(x) + f^*(x^*) = x^*(x) \iff x^* \in \partial f(x).

Here $x^*(x)$ is a real number, viewed as an extended real.

Degenerate cases. The sum is extended-real addition, with the convention $(-\infty) + (+\infty) = (+\infty) + (-\infty) = -\infty$ . So if $f(x)$ and $f^*(x^*)$ were infinite with opposite signs, the sum would be $-\infty$ , and the inequality would require $x^*(x) \le -\infty$ . That is false. Whether properness excludes this case depends on the unseen definitions. If $f(x) = +\infty$ and $f^*(x^*) > -\infty$ , the inequality holds trivially. In that case the equation is false, so the claim says $x^* \notin \partial f(x)$ . If $V = \{0\}$ , then $x^* = 0$ and $x^*(x) = 0$ , and the claim reduces to $0 \le f(0) + f^*(0)$ , with equality exactly when $0 \in \partial f(0)$ .

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