Fenchel–Moreau theorem

DefinitionFenchel conjugate#✓fully proved

Let \(E\) be a real vector space with a topology and let \(f : E \to [-\infty, \infty]\). The Fenchel conjugate of \(f\) at a continuous linear functional \(L : E \to \mathbb{R}\) is the extended real number \(f^*(L) = \sup_{y \in E} \big(L(y) - f(y)\big)\).

noncomputable def fenchelConj (f : E → EReal) (L : E →L[ℝ] ℝ) : EReal :=
  ⨆ y : E, (((L y : ℝ)) : EReal) - f y

Used by 6

Used byThe biconjugate lies below the function · Fenchel biconjugate · Fenchel–Moreau theorem · Legendre transform · Supremum formula for the Legendre transform · The double Legendre transform lies below the function

DefinitionFenchel biconjugate#✓fully proved

Let \(E\) be a real vector space with a topology and let \(f : E \to [-\infty, \infty]\). The biconjugate of \(f\) at \(x \in E\) is the extended real number \(f^{**}(x) = \sup_L \big(L(x) - f^*(L)\big)\), where \(L\) ranges over the continuous linear functionals \(E \to \mathbb{R}\) and \(f^*\) is the Fenchel conjugate of \(f\).

noncomputable def fenchelBiconj (f : E → EReal) (x : E) : EReal :=
  ⨆ L : E →L[ℝ] ℝ, (((L x : ℝ)) : EReal) - fenchelConj f L

Uses 1 · Used by 3

Statement usesFenchel conjugate

Used byThe biconjugate lies below the function · Fenchel–Moreau theorem · The double Legendre transform lies below the function

TheoremLower semicontinuous functions have closed epigraphs#✓fully proved

Let \(E\) be a topological space and let \(f : E \to [-\infty, \infty]\) be lower semicontinuous. Then the set \(\{(x, r) \in E \times \mathbb{R} : f(x) \le r\}\) is closed in \(E \times \mathbb{R}\).

theorem isClosed_epi_real (f : E → EReal) (hf_lsc : LowerSemicontinuous f) :
    IsClosed {p : E × ℝ | f p.1 ≤ (p.2 : EReal)}

Used by 1

Used byFenchel–Moreau theorem

TheoremThe biconjugate lies below the function#✓fully proved

Let \(E\) be a real vector space with a topology and let \(f : E \to [-\infty, \infty]\) never take the value \(-\infty\). Then \(f^{**}(x) \le f(x)\) for every \(x \in E\), where \(f^{**}\) is the Fenchel biconjugate of \(f\).

This is the easy direction of the Fenchel–Moreau theorem.

theorem biconj_le (f : E → EReal) (hf_not_bot : ∀ x, f x ≠ ⊥) (x : E) :
    fenchelBiconj f x ≤ f x

Uses 2 · Used by 2

Statement usesFenchel biconjugate

Proof usesFenchel conjugate

Used byFenchel–Moreau theorem · The double Legendre transform lies below the function

TheoremFenchel–Moreau theorem#✓fully proved

Let \(E\) be a locally convex real topological vector space, not necessarily Hausdorff. Let \(f : E \to [-\infty, \infty]\) be lower semicontinuous, never equal to \(-\infty\), not identically \(+\infty\), and convex in the sense that the set \(\{(x, r) \in E \times \mathbb{R} : f(x) \le r\}\) is convex. Then for every \(x \in E\), \(f(x) = \sup_L \big(L(x) - \sup_{y \in E} (L(y) - f(y))\big)\), where \(L\) ranges over the continuous linear functionals \(E \to \mathbb{R}\); that is, \(f\) equals its Fenchel biconjugate.

theorem fenchel_moreau
    {f : E → EReal}
    (hf_convex : Convex ℝ {p : E × ℝ | f p.1 ≤ (p.2 : EReal)})
    (hf_lsc : LowerSemicontinuous f)
    (hf_not_top : ∃ x, f x ≠ ⊤)
    (hf_not_bot : ∀ x, f x ≠ ⊥) :
    ∀ x : E,
      f x = ⨆ (L : E →L[ℝ] ℝ),
        (((L x : ℝ) : EReal) - (⨆ y : E, ((L y : ℝ) : EReal) - f y))

Sources

• Werner Fenchel, Convex Cones, Sets, and Functions: From Notes by D. W. Blackett of Lectures at Princeton University, 1951, Princeton University Department of Mathematics, 1953, Open Library OL1430688W; and Jean-Jacques Moreau, "Fonctions convexes duales et points proximaux," C. R. Acad. Sci. Paris 255 (1962), 2897–2899, zbMATH 0118.10502.

Uses 4

Proof usesThe biconjugate lies below the function · Fenchel biconjugate · Fenchel conjugate · Lower semicontinuous functions have closed epigraphs

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.