Strong alternatives for strict convex inequality systems

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

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).