Finite systems of linear inequalities #
Gale's theorem of the alternative for a finite system of weak linear inequalities and Motzkin's transposition theorem for a mixed system of strict and weak ones, the characterisation of the consequences of a consistent system, and Farkas' Lemma.
Farkas' Lemma is the bipolar identity K°° = K for the cone K generated by the coefficient
vectors, which is closed because it is finitely generated (Minkowski–Weyl). Gale's theorem follows
from it by homogenisation: the system ⟨aᵢ, x⟩ ≤ αᵢ is inconsistent exactly when (0, -1) lies in
the cone of F × ℝ generated by the (aᵢ, αᵢ) together with (0, 1), since a point of the polar
with a negative last coordinate rescales to a solution. Motzkin's theorem is then derived from the
alternative for a system of convex inequalities with affine side constraints.
Main results #
farkas,farkas_of_pairing— Farkas' Lemma. The two differ only in which side of the pairing carries the coefficient vectors:farkas_of_pairingputs them first, the orientation instance search can use atepiPairing, andfarkasis the flipped form the rest of the file reads in.alternative_linear_system— Gale's theorem;exists_multipliers_of_infeasibleis its existence half alone.alternative_linear_system_strict— Motzkin's transposition theorem.le_consequence_iff— the consequences of a consistent system.mem_pointedCone_hull_range_iff,isClosed_coe_pointedCone_hull_range— the two facts about the cone generated by a finite family that Farkas' Lemma runs on.eq_zero_of_forall_pairing_eq_zero,eq_zero_and_nonpos_of_forall_nonneg— a compatible pairing separates its second variable, so an affine function of the pairing that is non-negative everywhere is a non-negative constant. This is the step that turns the multiplier alternative for a convex system into the multiplier condition of Motzkin's theorem, and it needsIsCompatiblePairing B.flip, not merelyIsCompatiblePairing B.
References #
- R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §22.
Conical combinations of a finite family #
Membership in the pointed-cone hull of a finite family, unfolded to a non-negative combination.
The cone generated by a finite family is closed: it is finitely generated, hence polyhedral (Weyl's half of Minkowski–Weyl), hence an intersection of finitely many closed half-spaces.
Farkas' Lemma #
Farkas' Lemma in the form the pairing calls for: an inequality ⟨a₀, x⟩ ≤ 0 is a
consequence of the homogeneous system ⟨aᵢ, x⟩ ≤ 0 exactly when a₀ is a non-negative combination
of the aᵢ. This is Rockafellar's remark that Farkas' Lemma is K°° = K for the cone K
generated by the aᵢ. The coefficient vectors sit in the first space of the pairing, the
orientation in which epiPairing's instances are found.
The alternative for a weak system #
Farkas' Lemma, in the orientation the rest of the development uses: the solution variable
lives in E and the coefficient vectors in F.
The substantial half of Gale's theorem: an inconsistent finite system of weak linear
inequalities carries non-negative multipliers that annihilate the coefficient vectors while making
the right-hand sides negative. This is Farkas' Lemma applied in F × ℝ to the vectors (aᵢ, αᵢ)
together with the extra generator (0, 1).
Gale's theorem of the alternative. For a₁, …, a_m and α₁, …, α_m, one and only one of
the following holds: the system ⟨aᵢ, x⟩ ≤ αᵢ has a solution, or
there are non-negative λ₁, …, λ_m with ∑ λᵢaᵢ = 0 and ∑ λᵢαᵢ < 0. "One and only one" is
recorded as an Iff with a negation on the right: the forward direction is the elementary
exclusivity, the backward direction exists_multipliers_of_infeasible.
The alternative for a mixed system #
The affine function x ↦ ⟨x, y⟩ - c of a pairing, bundled as an AffineMap. The alternative
for a convex system keeps its affine constraints as E →ᵃ[ℝ] ℝ, and this is the bundling that
presents a linear inequality to it. affineFn is the same function read in EReal.
Equations
- Tdaf.ConvexAnalysis.affineMapOfPairing B y c = AffineMap.mk' (fun (x : E) => (B x) y - c) (B.flip y) 0 ⋯
Instances For
The value of a weighted mixed system at x, as one affine function of the pairing: the
coefficient vector is ∑ λᵢaᵢ + ∑ μⱼbⱼ and the constant is ∑ λᵢαᵢ + ∑ μⱼβⱼ.
A pairing whose flip is compatible separates its second variable: only 0 pairs to 0
against every x. This is Hahn–Banach on F plus the surjectivity that IsCompatiblePairing
asserts.
An affine function of the pairing that is non-negative on all of E is a non-negative
constant: its linear part vanishes. This is the step that turns the multiplier alternative for a
convex system into the multiplier condition of Motzkin's theorem.
Motzkin's transposition theorem. If the weak subsystem ⟨bⱼ, x⟩ ≤ βⱼ is consistent, then
one and only one of the following holds: the mixed system
⟨aᵢ, x⟩ < αᵢ, ⟨bⱼ, x⟩ ≤ βⱼ has a solution, or there are non-negative multipliers with at least
one of the λᵢ non-zero, ∑ λᵢaᵢ + ∑ μⱼbⱼ = 0 and ∑ λᵢαᵢ + ∑ μⱼβⱼ ≤ 0.
The consequences of a consistent system. For a system ⟨aᵢ, x⟩ ≤ αᵢ with a solution, the
inequality
⟨a₀, x⟩ ≤ α₀ is a consequence of the system exactly when a₀ is a non-negative combination
∑ λᵢaᵢ whose right-hand side ∑ λᵢαᵢ does not exceed α₀. The inequality fails to be a
consequence exactly when the mixed system ⟨-a₀, x⟩ < -α₀, ⟨aᵢ, x⟩ ≤ αᵢ is solvable, so
Motzkin's theorem applies and its multiplier on the strict inequality can be divided out.