Fenchel duality with attained dual functional

Proved

VectorSpaceOpt.fenchel_duality

by wenxinzhang · Aug 25, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-analysisdualityfenchel-dualityfunctional-analysis

Let $f$ be convex on nonempty $C$ and $g$ concave on nonempty $D$ in a real normed space. Assume the intrinsic interiors of $C$ and $D$ meet, and that either the restricted epigraph of $f$ or restricted hypograph of $g$ has nonempty ordinary interior. If the finite number $\mu$ is the infimum of $f-g$ on $C\cap D$ , then some $\ell_0\in C^*\cap D^*$ satisfies

\mu=g_D^*(\ell_0)-f_C^*(\ell_0)=\max_{\ell\in C^*\cap D^*}\bigl(g_D^*(\ell)-f_C^*(\ell)\bigr).

If $x_0$ attains the primal infimum, it also attains both conjugate extrema at $\ell_0$ . This is the mission goal and retains both qualification conditions and dual attainment.

Preamble

import Definitions.Def_VectorSpaceOpt_restrictedConvexConjugate
import Definitions.Def_VectorSpaceOpt_restrictedConcaveConjugate

open Set

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 7, §7.12, Theorem 1 (Fenchel Duality). -/
theorem fenchel_duality
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (C D : Set X) (f g : X → ℝ) (μ : ℝ)
    (hC : C.Nonempty) (hD : D.Nonempty)
    (hf : ConvexOn ℝ C f) (hg : ConcaveOn ℝ D g)
    (hri : (intrinsicInterior ℝ C ∩ intrinsicInterior ℝ D).Nonempty)
    (hsolid :
      (interior {p : X × ℝ | p.1 ∈ C ∧ f p.1 ≤ p.2}).Nonempty ∨
      (interior {p : X × ℝ | p.1 ∈ D ∧ p.2 ≤ g p.1}).Nonempty)
    (hμ : IsGLB ((fun x : X ↦ f x - g x) '' (C ∩ D)) μ) :
    ∃ ℓ₀ : X →L[ℝ] ℝ,
      BddAbove ((fun x : X ↦ ℓ₀ x - f x) '' C) ∧
      BddBelow ((fun x : X ↦ ℓ₀ x - g x) '' D) ∧
      μ = restrictedConcaveConjugate D g ℓ₀ -
        restrictedConvexConjugate C f ℓ₀ ∧
      (∀ ℓ : X →L[ℝ] ℝ,
        BddAbove ((fun x : X ↦ ℓ x - f x) '' C) →
        BddBelow ((fun x : X ↦ ℓ x - g x) '' D) →
        restrictedConcaveConjugate D g ℓ -
          restrictedConvexConjugate C f ℓ ≤ μ) ∧
      (∀ x₀ ∈ C ∩ D, f x₀ - g x₀ = μ →
        restrictedConvexConjugate C f ℓ₀ = ℓ₀ x₀ - f x₀ ∧
        restrictedConcaveConjugate D g ℓ₀ = ℓ₀ x₀ - g x₀) := by sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, public scan https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf, Chapter 7, §7.12, Theorem 1 (Fenchel Duality), printed pp. 201–202; physical PDF pp. 221–222.

Read-back

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

For every real normed vector space $X$ , nonempty sets $C,D⊆X$ , functions $f,g : X → ℝ$ , and real number $μ$ , assume $f$ is convex on $C$ , $g$ is concave on $D$ , the intersection of the real intrinsic interiors of $C$ and $D$ is nonempty, and at least one of the following two subsets of $X×ℝ$ has nonempty topological interior: the restricted epigraph $\{(x,r):x∈C, f(x)≤r\}$ or the restricted hypograph $\{(x,r):x∈D, r≤g(x)\}$ . Also assume that $μ$ is the greatest lower bound of $\{f(x)-g(x):x∈C∩D\}$ , meaning it is a lower bound and every other lower bound is at most $μ$ ; attainment is not assumed. Then there exists a continuous real-linear functional $ℓ₀$ such that $\{ℓ₀(x)-f(x):x∈C\}$ is bounded above, $\{ℓ₀(x)-g(x):x∈D\}$ is bounded below, and $μ=\inf_{x∈D}(ℓ₀(x)-g(x))-\sup_{x∈C}(ℓ₀(x)-f(x))$ . For every continuous real-linear $ℓ$ satisfying the same respective boundedness conditions, $\inf_{x∈D}(ℓ(x)-g(x))-\sup_{x∈C}(ℓ(x)-f(x))≤μ$ . Finally, for every $x₀∈C∩D$ that does attain $f(x₀)-g(x₀)=μ$ , both extrema for $ℓ₀$ are attained there: $\sup_{x∈C}(ℓ₀(x)-f(x))=ℓ₀(x₀)-f(x₀)$ and $\inf_{x∈D}(ℓ₀(x)-g(x))=ℓ₀(x₀)-g(x₀)$ . All these conjugate extrema are real $sSup$ or $sInf$ values; nonemptiness of $C,D$ and the displayed boundedness hypotheses put the extrema used in the conclusion in their ordinary finite-real cases.

Human review

Endorsed by Shuze Chen · Aug 25, 2026
Endorsed by wenxinzhang · Aug 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph