Strong alternatives for strict convex inequality systems

Proved

ConvexOptimization.strong_alternatives_strict_convex

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

convex-optimizations-proceduresemidefinite-programming

Strong alternatives for a system of strict convex inequalities.

Let $f_1,\dots,f_m : \mathbb{R}^n \to \mathbb{R}$ be convex, let $a_1,\dots,a_p \in \mathbb{R}^n$ be linearly independent, let $b \in \mathbb{R}^p$ , and assume the affine system $\langle a_j, x\rangle = b_j$ has a solution. Write $g(\lambda,\nu) = \inf_x\bigl[\sum_i \lambda_i f_i(x) + \sum_j \nu_j(\langle a_j,x\rangle - b_j)\bigr]$ for the dual function of the feasibility problem, i.e. of the problem with zero objective. Then

\bigl(\exists x:\ f_i(x) < 0 \ \forall i,\ \langle a_j,x\rangle = b_j \ \forall j\bigr) \qquad\Longleftrightarrow\qquad \neg\bigl(\exists \lambda \succeq 0,\ \lambda \ne 0,\ \nu:\ g(\lambda,\nu) \ge 0\bigr).

The two systems are strong alternatives: exactly one of them is feasible, with no gap between them. The second is the certificate of infeasibility — a nonnegative, nonzero combination of the constraints that is bounded below by zero, i.e. a proof that no strictly feasible point exists.

Theorems of the alternative are the infeasibility counterpart of duality: rather than certifying optimality, they certify that a system has no solution. Farkas' lemma is the linear case, and the LMI alternatives used later in this mission are the semidefinite specializations of this result.

Formalization Note The dual function is the mission's dualFunction applied with objective 0, so the statement reuses the Lagrange-duality interface of Mission II; the constraint qualification is stated as solvability of the equality system together with linear independence of the a j. Source: B&V §5.8.2, pp. 260–261, systems (5.79)/(5.80).

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_lagrangeDuality

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.strong_alternatives_strict_convex {n mm p : ℕ}
    (fc : Fin mm → EuclideanSpace ℝ (Fin n) → ℝ)
    (hfc : ∀ i, ConvexOn ℝ Set.univ (fc i))
    (a : Fin p → EuclideanSpace ℝ (Fin n)) (ha : LinearIndependent ℝ a)
    (b : Fin p → ℝ) (hCQ : ∃ x, ∀ j, ⟪a j, x⟫ = b j) :
    (∃ x, (∀ i, fc i x < 0) ∧ ∀ j, ⟪a j, x⟫ = b j) ↔
      ¬∃ (lam : Fin mm → ℝ) (nu : Fin p → ℝ), (∀ i, 0 ≤ lam i) ∧ lam ≠ 0 ∧
        0 ≤ dualFunction 0 fc a b lam nu := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 260-261, §5.8.2 eq. (5.79)/(5.80) (strong alternatives for strict convex inequalities)

Read-back

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

Theorem. Fix natural numbers $n$ , $mm$ , $p$ (any of which may be $0$ ). Assume: a family of functions $f_i : \mathbb{R}^n \to \mathbb{R}$ for $i \in \{1,\dots,mm\}$ (real-valued, total on all of $\mathbb{R}^n$ , modeled as Euclidean space), each convex on the whole space; vectors $a_1,\dots,a_p \in \mathbb{R}^n$ that are linearly independent (this forces $p \le n$ and that all $a_j$ are distinct and nonzero; for $p = 0$ it is vacuous); scalars $b_1,\dots,b_p \in \mathbb{R}$ ; and the hypothesis that there exists some $x$ with $\langle a_j, x\rangle = b_j$ for every $j$ . The theorem asserts the following equivalence:

\Big(\exists x \in \mathbb{R}^n:\ f_i(x) < 0 \text{ (strictly) for every } i, \text{ and } \langle a_j, x\rangle = b_j \text{ for every } j\Big) \iff \neg\Big(\exists\, \lambda \in \mathbb{R}^{mm},\, \nu \in \mathbb{R}^{p}:\ \lambda_i \ge 0\ \forall i,\ \lambda \ne 0,\ \text{and}\ 0 \le g(\lambda,\nu)\Big),

where $g(\lambda,\nu)$ unfolds (via the bundle's ConvexOptimization_dualFunction with objective $f_0 \equiv 0$ ) to the extended-real infimum over all of $\mathbb{R}^n$ (unconstrained):

g(\lambda,\nu) = \inf_{x \in \mathbb{R}^n}\Big(\textstyle\sum_i \lambda_i f_i(x) + \sum_j \nu_j\,(\langle a_j, x\rangle - b_j)\Big) \in \overline{\mathbb{R}},

taken in $\overline{\mathbb{R}} = [-\infty,+\infty]$ ; it can be $-\infty$ , but never $+\infty$ since $\mathbb{R}^n$ is nonempty (including $n=0$ ), and the condition $0 \le g(\lambda,\nu)$ is an inequality of extended reals. Here $\lambda \ne 0$ means $\lambda$ is not the identically-zero vector, and $\nu$ is unrestricted in sign. Edge cases: if $mm = 0$ , the strict inequalities on the left are vacuous (so the left side holds by the stated feasibility hypothesis), while on the right the only $\lambda \in \mathbb{R}^0$ is the zero function, so $\lambda \ne 0$ is unsatisfiable and the right side is vacuously true — the biconditional then holds degenerately. If $p = 0$ , all equality-constraint clauses are vacuous and the feasibility hypothesis is automatic.

Human review

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

View graph