Global sensitivity inequality

Proved

ConvexOptimization.global_sensitivity

by Shuze Chen · Aug 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexoptimizationdualitykkt

The global sensitivity inequality — bound (5.57) of Boyd & Vandenberghe: optimal dual variables price the constraints.

Consider the standard problem and its perturbed version, in which the constraints are relaxed or tightened by $u \in \mathbb{R}^m$ and $v \in \mathbb{R}^p$ :

f_i(x) \le u_i \ (i = 1,\dots,m), \qquad \langle a_j, x\rangle = b_j + v_j \ (j = 1,\dots,p).

Let $x^{\star}$ be feasible for the unperturbed problem and let $\lambda \succeq 0$ , $\nu$ satisfy the zero-gap condition $g(\lambda,\nu) = f_0(x^{\star})$ . Then every $x$ feasible for the $(u,v)$ -perturbed problem satisfies

f_0(x) \;\ge\; f_0(x^{\star}) - \sum_{i=1}^{m}\lambda_i u_i - \sum_{j=1}^{p}\nu_j v_j .

Writing $p^{\star}(u,v)$ for the perturbed optimal value, this is $p^{\star}(u,v) \ge p^{\star}(0,0) - \lambda^{T}u - \nu^{T}v$ : the multipliers bound how much can be gained by loosening a constraint. Loosening the $i$ -th inequality by $u_i > 0$ cannot reduce the optimal value by more than $\lambda_i u_i$ , so a large multiplier marks a constraint that is expensive to violate and a zero multiplier marks one that is locally free. Unlike the differential reading of shadow prices, the bound is global — valid for every perturbation, however large.

Formalization Note The statement quantifies over an arbitrary point $x$ feasible for the perturbed constraints rather than over the perturbed optimal value, which avoids assuming that optimal value exists; the zero-gap hypothesis is an equality of the EReal-valued dual function with the coercion of $f_0(x^{\star})$ . Source: B&V §5.6.1, p. 250, eq. (5.57).

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.global_sensitivity {n mm p : ℕ}
    (f₀ : EuclideanSpace ℝ (Fin n) → ℝ)
    (fc : Fin mm → EuclideanSpace ℝ (Fin n) → ℝ)
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (b : Fin p → ℝ)
    (xs : EuclideanSpace ℝ (Fin n)) (hxs : xs ∈ feasibleSet fc a b)
    (lam : Fin mm → ℝ) (hlam : ∀ i, 0 ≤ lam i) (nu : Fin p → ℝ)
    (hzero : dualFunction f₀ fc a b lam nu = (f₀ xs : EReal))
    (u : Fin mm → ℝ) (v : Fin p → ℝ) (x : EuclideanSpace ℝ (Fin n))
    (hx_ineq : ∀ i, fc i x ≤ u i) (hx_eq : ∀ j, ⟪a j, x⟫ = b j + v j) :
    f₀ xs - ∑ i, lam i * u i - ∑ j, nu j * v j ≤ f₀ x := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 250, §5.6.1 eq. (5.57) (a global inequality relating the perturbed optimal value to the unperturbed one)

Read-back

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

Theorem. Fix data $f_0, f, a, b$ (implicit $n, mm, p$ ; no convexity or regularity assumed), a feasible point $x_s$ ( $f_i(x_s) \le 0$ for all $i$ , $\langle a_j, x_s\rangle = b_j$ for all $j$ ), multipliers $\lambda$ with $\lambda_i \ge 0$ for all $i$ and $\nu$ unrestricted, and assume the exact extended-real equality $g(\lambda,\nu) = f_0(x_s)$ , where $g(\lambda,\nu)$ is the unconstrained infimum over $\mathbb{R}^n$ of the Lagrangian (in $[-\infty,+\infty]$ ; the hypothesis forces it finite). Further fix perturbation vectors $u \in \mathbb{R}^{mm}$ and $v \in \mathbb{R}^p$ , of arbitrary sign and size, and a point $x \in \mathbb{R}^n$ satisfying the perturbed constraints: $f_i(x) \le u_i$ for every $i$ and $\langle a_j, x\rangle = b_j + v_j$ exactly for every $j$ . The conclusion is the real inequality

f_0(x_s) \;-\; \sum_i \lambda_i u_i \;-\; \sum_j \nu_j v_j \;\le\; f_0(x).

Note $x$ need not be feasible for the original problem, and the bound is stated for this one given $x$ (equivalently, since $x$ is universally quantified as an argument, for every point satisfying the perturbed constraints). When $mm = p = 0$ the sums vanish and the statement reduces to $f_0(x_s) \le f_0(x)$ for every $x \in \mathbb{R}^n$ .

Human review

Endorsed by Community (Bot) · Aug 12, 2026
Endorsed by Shuze Chen · Aug 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph