Two-sided sensitivity bounds from Lagrange multipliers

Proved

VectorSpaceOpt.lagrange_multiplier_sensitivity

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

lagrange-multiplierperturbationsensitivityvalue-function

Consider perturbed constraints $G(x)\le_P z_0$ and $G(x)\le_P z_1$ . Let $x_i\in\Omega$ be feasible for $z_i$ , and let dual-positive $z_i^*$ be complementary and make $x_i$ minimize the shifted Lagrangian $f(x)+z_i^*(G(x)-z_i)$ over $\Omega$ . Then

z_1^*(z_1-z_0)\le f(x_0)-f(x_1)\le z_0^*(z_1-z_0).

The hypotheses spell out the source phrase “solutions and corresponding multipliers” without hiding optimality or complementarity in a new structure. This theorem quantifies the multiplier interpretation as a marginal value of constraint relaxation and provides a reusable stability estimate for pairs of conic programs. It remains meaningful for arbitrary vector perturbations, with ordering confined to feasibility and multiplier positivity.

Preamble

import Definitions.Def_VectorSpaceOpt_coneLE
import Definitions.Def_VectorSpaceOpt_dualPositive

Formal statement

namespace VectorSpaceOpt

/-- Luenberger, Chapter 8, §8.5, Theorem 1. -/
theorem lagrange_multiplier_sensitivity
    {X Z : Type*}
    [NormedAddCommGroup Z] [NormedSpace ℝ Z]
    (P : ConvexCone ℝ Z) (Ω : Set X) (f : X → ℝ) (G : X → Z)
    (z₀ z₁ : Z) (x₀ x₁ : X)
    (zstar₀ zstar₁ : Z →L[ℝ] ℝ)
    (hx₀ : x₀ ∈ Ω) (hx₁ : x₁ ∈ Ω)
    (hfeas₀ : coneLE P (G x₀) z₀)
    (hfeas₁ : coneLE P (G x₁) z₁)
    (hzstar₀ : dualPositive P zstar₀)
    (hzstar₁ : dualPositive P zstar₁)
    (hcomp₀ : zstar₀ (G x₀ - z₀) = 0)
    (hcomp₁ : zstar₁ (G x₁ - z₁) = 0)
    (hmin₀ : ∀ x ∈ Ω,
      f x₀ + zstar₀ (G x₀ - z₀) ≤
        f x + zstar₀ (G x - z₀))
    (hmin₁ : ∀ x ∈ Ω,
      f x₁ + zstar₁ (G x₁ - z₁) ≤
        f x + zstar₁ (G x - z₁)) :
    zstar₁ (z₁ - z₀) ≤ f x₀ - f x₁ ∧
      f x₀ - f x₁ ≤ zstar₀ (z₁ - z₀) := 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.5, Theorem 1, printed p. 222; physical PDF p. 242.

Read-back

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

Let $X$ be an arbitrary type and $Z$ a real normed vector space. For a real convex cone $P$ in $Z$ , set $Ω⊆X$ , functions $f : X → ℝ$ and $G : X → Z$ , vectors $z₀,z₁∈Z$ , points $x₀,x₁∈X$ , and continuous real-linear functionals $z₀^*,z₁^*$ , assume $x₀,x₁∈Ω$ ; $z₀-G(x₀)∈P$ and $z₁-G(x₁)∈P$ ; each $zᵢ^*$ is nonnegative on every point of $P$ ; and $z₀^*(G(x₀)-z₀)=0$ and $z₁^*(G(x₁)-z₁)=0$ . Also assume that for every $x∈Ω$ , $f(x₀)+z₀^*(G(x₀)-z₀)≤f(x)+z₀^*(G(x)-z₀)$ and $f(x₁)+z₁^*(G(x₁)-z₁)≤f(x)+z₁^*(G(x)-z₁)$ . Then $z₁^*(z₁-z₀)≤f(x₀)-f(x₁)≤z₀^*(z₁-z₀)$ . The minimization hypotheses range over all of $Ω$ , not only feasible points, and no vector-space structure on $X$ , convexity, closedness, or existence assertion beyond the supplied $x₀,x₁$ is 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