Global Lagrange duality under strict feasibility

Proved

VectorSpaceOpt.lagrange_duality

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

convex-programminglagrange-dualityslater-conditionstrong-duality

Let $f$ be convex and $G$ cone-convex on nonempty $\Omega$ in real normed spaces. Let $P$ be a convex cone with nonempty interior, and assume a Slater point $x_s\in\Omega$ satisfies $-G(x_s)\in\operatorname{int}P$ . If the finite number $\mu$ is the infimum of $f$ over $G(x)\le_P0$ , then some dual-positive $z_0^*$ attains

\mu=\phi(z_0^*)=\max_{z^*\text{ dual-positive}}\phi(z^*).

If $x_0$ attains the primal value, then $z_0^*(G(x_0))=0$ and $x_0$ minimizes $L(\cdot,z_0^*)$ on $\Omega$ . The root adds neither closedness nor pointedness of $P$ and retains dual attainment and complementarity. Its conclusion remains useful even when existence of a primal optimizer is not known.

Preamble

import Definitions.Def_VectorSpaceOpt_coneLE
import Definitions.Def_VectorSpaceOpt_dualPositive
import Definitions.Def_VectorSpaceOpt_coneConvexOn
import Definitions.Def_VectorSpaceOpt_lagrangian
import Definitions.Def_VectorSpaceOpt_lagrangeDualValue

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 8, §8.6, Theorem 1 (Lagrange Duality). -/
theorem lagrange_duality
    {X Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (Ω : Set X) (f : X → ℝ) (G : X → Z) (μ : ℝ)
    (hΩ : Ω.Nonempty) (hf : ConvexOn ℝ Ω f)
    (hG : ConeConvexOn P Ω G)
    (hPint : (interior (P : Set Z)).Nonempty)
    (hslater : ∃ x ∈ Ω, -G x ∈ interior (P : Set Z))
    (hμ : IsGLB
      (f '' {x : X | x ∈ Ω ∧ coneLE P (G x) 0}) μ) :
    ∃ zstar₀ : Z →L[ℝ] ℝ,
      dualPositive P zstar₀ ∧
      lagrangeDualValue Ω f G zstar₀ = (μ : EReal) ∧
      (∀ zstar : Z →L[ℝ] ℝ, dualPositive P zstar →
        lagrangeDualValue Ω f G zstar ≤
          lagrangeDualValue Ω f G zstar₀) ∧
      (∀ x₀ ∈ Ω, coneLE P (G x₀) 0 → f x₀ = μ →
        zstar₀ (G x₀) = 0 ∧
        ∀ x ∈ Ω,
          lagrangian f G zstar₀ x₀ ≤ lagrangian f G zstar₀ 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 8, §8.6, Theorem 1 (Lagrange Duality), printed pp. 224–225; physical PDF pp. 244–245. Equivalent multiplier conclusion also appears in §8.3, Theorem 1, printed pp. 217–218.

Read-back

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

For real normed vector spaces $X,Z$ , a real convex cone $P$ in $Z$ , a set $Ω⊆X$ , functions $f : X → ℝ$ and $G : X → Z$ , and $μ∈ℝ$ , assume: $Ω$ is nonempty; $f$ is convex on $Ω$ ; $Ω$ is convex and for every $x₀,x₁∈Ω$ and $a,b≥0$ with $a+b=1$ , $(aG(x₀)+bG(x₁))-G(ax₀+bx₁)∈P$ ; the topological interior of $P$ is nonempty; some $x∈Ω$ satisfies $-G(x)∈\operatorname{interior}(P)$ ; and $μ$ is the greatest lower bound of the objective-value set $\{f(x):x∈Ω, -G(x)∈P\}$ . Then there exists a continuous real-linear functional $z₀^*$ nonnegative on every $p∈P$ such that its extended-real dual value $q(z₀^*)=\inf_{x∈Ω}(f(x)+z₀^*(G(x)))$ equals the finite embedded value $μ$ , and for every other continuous real-linear $z^*$ nonnegative on $P$ , $q(z^*)≤q(z₀^*)$ in $\mathrm{EReal}$ . Moreover, for every $x₀∈Ω$ with $-G(x₀)∈P$ and $f(x₀)=μ$ , one has $z₀^*(G(x₀))=0$ and $f(x₀)+z₀^*(G(x₀))≤f(x)+z₀^*(G(x))$ for every $x∈Ω$ . The greatest-lower-bound hypothesis and final clause do not assert that such an $x₀$ exists. Since $Ω$ is nonempty, each dual infimum is over at least one finite value and may be finite or $-∞$ , but not $+∞$ ; the asserted equality makes the value at $z₀^*$ finite.

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