§5.13, Theorem 1 — Minimum-distance duality for a convex set

Proved

VectorSpaceOpt.convex_minimum_norm_duality

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

convex-optimizationfunctional-analysisminimum-distancestrong-dualitysupport-functional

Let $X$ be a real normed space, $K \subseteq X$ nonempty and convex, and let $d=\operatorname{infDist}(x_1,K)>0$ . There exist a continuous linear functional $f$ and $c \in \mathbb R$ with $\|f\| \leq 1$ and $f(k) ≤ c$ on $K$ such that

f(x_1)-c=d,\qquad g(x_1)-b\le d\text{ for every feasible upper-bound pair }(g,b).

Thus $(f,c)$ attains the dual distance value. If $x_0 \in K$ realizes $d$ , then $-f$ is aligned with $x_0-x_1$ . The real upper-bound certificate is equivalent to the source's finite support-value formulation while avoiding an unfaithful boundedness assumption on $K$ ; it is the mission's capstone convex strong-duality result.

Preamble

import Mathlib

Formal statement

namespace VectorSpaceOpt

theorem convex_minimum_norm_duality
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (K : Set X) (hK : Convex ℝ K) (hKne : K.Nonempty) (x₁ : X)
    (hd : 0 < Metric.infDist x₁ K) :
    ∃ (f : X →L[ℝ] ℝ) (c : ℝ),
      ‖f‖ ≤ 1 ∧
      (∀ k ∈ K, f k ≤ c) ∧
      f x₁ - c = Metric.infDist x₁ K ∧
      (∀ (g : X →L[ℝ] ℝ) (b : ℝ), ‖g‖ ≤ 1 → (∀ k ∈ K, g k ≤ b) →
        g x₁ - b ≤ Metric.infDist x₁ K) ∧
      (∀ x₀ ∈ K, ‖x₀ - x₁‖ = Metric.infDist x₁ K →
        (-f) (x₀ - x₁) = ‖-f‖ * ‖x₀ - x₁‖) := by sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods, §5.13, Theorem 1, book pp. 136–137 (PDF physical pp. 156–157), https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf

Read-back

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

Let $X$ be any real normed vector space, let $K ⊆ X$ be convex and nonempty, and let $x_1 ∈ X$ satisfy $0 < \operatorname{infDist}(x_1,K)$ , where this is the metric infimum distance to $K$ . Then there exist a continuous real-linear functional $f : X → ℝ$ and a real number $c$ such that simultaneously: $‖f‖ ≤ 1$ ; $f(k) ≤ c$ for every $k ∈ K$ ; $f(x_1)-c=\operatorname{infDist}(x_1,K)$ ; for every continuous real-linear $g : X → ℝ$ and every $b ∈ ℝ$ , if $‖g‖ ≤ 1$ and $g(k) ≤ b$ for all $k ∈ K$ , then $g(x_1)-b ≤ \operatorname{infDist}(x_1,K)$ ; and every $x_0 ∈ K$ satisfying $‖x_0-x_1‖=\operatorname{infDist}(x_1,K)$ obeys $(-f)(x_0-x_1)=‖-f‖‖x_0-x_1‖$ . The set $K$ is not assumed closed and therefore need not contain a nearest point, in which case the final universal clause is vacuous; $f$ is required only to have norm at most one, and completeness and nontriviality of $X$ are not assumed.

Human review

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

View graph