Rockafellar, §22: Linear Inequalities

Finite systems of weak and strict linear inequalities, the theorems of the alternative that decide their solvability, and Farkas' Lemma.

Four of §22's nine numbered results are formalized over Rn n = ℝⁿ: Theorems 22.1–22.3 and Corollary 22.3.1 (Farkas' Lemma). The other five — Lemmas 22.4 and 22.5, Corollary 22.4.1, and Theorems 22.6 and 22.7 (Tucker's complementarity theorem) — rest on the elementary vectors of a subspace, a development that is combinatorial matroid theory rather than convex analysis and is deliberately not formalized here; it is this project's one scope deferral. Theorems 22.6 and 22.7 rest further on Tucker representations of a subspace, which the book describes only procedurally — solve the defining system for the last N - n coordinates in terms of the first n, for some permutation — so stating them at all needs a choice of n independent coordinate positions and the resulting change of basis. Corollary 31.4.2 is the one other result of the book resting on them.

The book writes ⟨aᵢ, x⟩ with the coefficient vector first, while the backbone writes B x (a i), because in general the solution vector and the coefficient vectors live in different spaces. On ℝⁿ the pairing is symmetric, and pairing_comm is the only translation any statement here needs.

Rockafellar's Σ ζ*ⱼIⱼ > 0 (p. 202) is a set containment, ⊆ (0, +∞): it says that ζ*₁ζ₁ + ⋯ + ζ*_NζN > 0 for every choice of ζⱼ ∈ Iⱼ. The convention is stated once in the book, in a parenthesis far ahead of the theorem that uses it; posIntervalCombo records it.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §22.

Theorem 22.1: the alternative for a system of weak inequalities

theorem Rockafellar.theorem_22_1 {m n : ℕ} (a : Fin m → TdafSurface.Rn n) (α : Fin m → ℝ) : (∃ (x : TdafSurface.Rn n), ∀ (i : Fin m), ((TdafSurface.pairing n) (a i)) x ≤ α i) ↔ ¬∃ (l : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ l i) ∧ ∑ i : Fin m, l i • a i = 0 ∧ ∑ i : Fin m, l i * α i < 0

Theorem 22.1 (Gale's theorem of the alternative). For aᵢ ∈ ℝⁿ and αᵢ ∈ ℝ, one and only one of the following holds: (a) ⟨aᵢ, x⟩ ≤ αᵢ for i = 1, …, m has a solution x ∈ ℝⁿ; (b) there are reals λᵢ ≥ 0 with ∑ λᵢaᵢ = 0 and ∑ λᵢαᵢ < 0. "One and only one" is the Iff with the negation on the right: forwards is the exclusivity, backwards the existence.

Theorem 22.2: the alternative for a mixed system

theorem Rockafellar.theorem_22_2 {n p q : ℕ} (a : Fin p → TdafSurface.Rn n) (α : Fin p → ℝ) (b : Fin q → TdafSurface.Rn n) (β : Fin q → ℝ) (hcons : ∃ (x : TdafSurface.Rn n), ∀ (j : Fin q), ((TdafSurface.pairing n) (b j)) x ≤ β j) : (∃ (x : TdafSurface.Rn n), (∀ (i : Fin p), ((TdafSurface.pairing n) (a i)) x < α i) ∧ ∀ (j : Fin q), ((TdafSurface.pairing n) (b j)) x ≤ β j) ↔ ¬∃ (l : Fin p → ℝ) (μ : Fin q → ℝ), (∀ (i : Fin p), 0 ≤ l i) ∧ (∀ (j : Fin q), 0 ≤ μ j) ∧ (∃ (i : Fin p), l i ≠ 0) ∧ ∑ i : Fin p, l i • a i + ∑ j : Fin q, μ j • b j = 0 ∧ ∑ i : Fin p, l i * α i + ∑ j : Fin q, μ j * β j ≤ 0

Theorem 22.2 (Motzkin's transposition theorem). Assume ⟨bⱼ, x⟩ ≤ βⱼ is consistent. Then one and only one of the following holds: (a) some x has ⟨aᵢ, x⟩ < αᵢ for every i and ⟨bⱼ, x⟩ ≤ βⱼ for every j; (b) there are reals λᵢ, μⱼ ≥ 0 with some λᵢ non-zero, ∑ λᵢaᵢ + ∑ μⱼbⱼ = 0 and ∑ λᵢαᵢ + ∑ μⱼβⱼ ≤ 0. The book cuts one index range 1, …, m at k; here the strict and weak constraints are separate families.

theorem Rockafellar.not_consistent_iff {n q : ℕ} (b : Fin q → TdafSurface.Rn n) (β : Fin q → ℝ) : (¬∃ (x : TdafSurface.Rn n), ∀ (j : Fin q), ((TdafSurface.pairing n) (b j)) x ≤ β j) ↔ ∃ (μ : Fin q → ℝ), (∀ (j : Fin q), 0 ≤ μ j) ∧ ∑ j : Fin q, μ j • b j = 0 ∧ ∑ j : Fin q, μ j * β j < 0

§22 (p. 200). The hypothesis of Theorem 22.2 is itself decided by Theorem 22.1: the weak subsystem is inconsistent exactly when it carries non-negative multipliers annihilating the bⱼ with ∑ μⱼβⱼ < 0.

Theorem 22.3: consequences of a system

def Rockafellar.IsConsequence {m n : ℕ} (a : Fin m → TdafSurface.Rn n) (α : Fin m → ℝ) (a₀ : TdafSurface.Rn n) (α₀ : ℝ) : Prop

Consequence of a system (p. 200): ⟨a₀, x⟩ ≤ α₀ is a consequence of the system ⟨aᵢ, x⟩ ≤ αᵢ, i = 1, …, m, if every solution of the system satisfies it.

Equations

• Rockafellar.IsConsequence a α a₀ α₀ = ∀ (x : TdafSurface.Rn n), (∀ (i : Fin m), ((TdafSurface.pairing n) (a i)) x ≤ α i) → ((TdafSurface.pairing n) a₀) x ≤ α₀

theorem Rockafellar.isConsequence_iff {m n : ℕ} {a : Fin m → TdafSurface.Rn n} {α : Fin m → ℝ} {a₀ : TdafSurface.Rn n} {α₀ : ℝ} : IsConsequence a α a₀ α₀ ↔ ∀ (x : TdafSurface.Rn n), (∀ (i : Fin m), ((TdafSurface.pairing n) x) (a i) ≤ α i) → ((TdafSurface.pairing n) x) a₀ ≤ α₀

IsConsequence in the backbone's orientation of the pairing.

theorem Rockafellar.theorem_22_3 {m n : ℕ} (a : Fin m → TdafSurface.Rn n) (α : Fin m → ℝ) (a₀ : TdafSurface.Rn n) (α₀ : ℝ) (hcons : ∃ (x : TdafSurface.Rn n), ∀ (i : Fin m), ((TdafSurface.pairing n) (a i)) x ≤ α i) : IsConsequence a α a₀ α₀ ↔ ∃ (l : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ l i) ∧ ∑ i : Fin m, l i • a i = a₀ ∧ ∑ i : Fin m, l i * α i ≤ α₀

Theorem 22.3. For a consistent system ⟨aᵢ, x⟩ ≤ αᵢ, an inequality ⟨a₀, x⟩ ≤ α₀ is a consequence of it iff ∑ λᵢaᵢ = a₀ and ∑ λᵢαᵢ ≤ α₀ for some reals λᵢ ≥ 0.

theorem Rockafellar.corollary_22_3_1 {m n : ℕ} (a : Fin m → TdafSurface.Rn n) (a₀ : TdafSurface.Rn n) : IsConsequence a (fun (x : Fin m) => 0) a₀ 0 ↔ ∃ (l : Fin m → ℝ), (∀ (i : Fin m), 0 ≤ l i) ∧ ∑ i : Fin m, l i • a i = a₀

Corollary 22.3.1 (Farkas' Lemma). ⟨a₀, x⟩ ≤ 0 is a consequence of ⟨aᵢ, x⟩ ≤ 0, i = 1, …, m, iff ∑ λᵢaᵢ = a₀ for some reals λᵢ ≥ 0.

theorem Rockafellar.solutions_eq_polarCone {m n : ℕ} (a : Fin m → TdafSurface.Rn n) : {x : TdafSurface.Rn n | ∀ (i : Fin m), ((TdafSurface.pairing n) (a i)) x ≤ 0} = Tdaf.ConvexAnalysis.polarCone (TdafSurface.pairing n) ↑(PointedCone.hull ℝ (Set.range a))

The solution set of a homogeneous system is a polar cone (p. 200): the solutions of ⟨aᵢ, x⟩ ≤ 0 are exactly K°, for K the convex cone generated by a₁, …, a_m.

theorem Rockafellar.corollary_22_3_1_polar {m n : ℕ} (a : Fin m → TdafSurface.Rn n) : Tdaf.ConvexAnalysis.polarCone (TdafSurface.pairing n) (Tdaf.ConvexAnalysis.polarCone (TdafSurface.pairing n) ↑(PointedCone.hull ℝ (Set.range a))) = ↑(PointedCone.hull ℝ (Set.range a))

Farkas' Lemma says K°° = K (p. 200) for K the convex cone generated by finitely many vectors: K is closed because it is finitely generated (Theorem 19.1), so Theorem 14.1 gives K°° = cl K = K.

The matrix form

def Rockafellar.IsRowsOf {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (a : Fin m → TdafSurface.Rn n) : Prop

The matrix form (p. 201): A is the m × n matrix whose rows are a₁, …, a_m, so that the system of alternative (a) of Theorem 22.1 reads Ax ≤ a, componentwise.

Equations

• Rockafellar.IsRowsOf A a = ∀ (x : TdafSurface.Rn n) (i : Fin m), (A x).ofLp i = ((TdafSurface.pairing n) (a i)) x

theorem Rockafellar.adjoint_eq_sum_smul {m n : ℕ} {A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m} {a : Fin m → TdafSurface.Rn n} (h : IsRowsOf A a) (w : TdafSurface.Rn m) : (LinearMap.adjoint A) w = ∑ i : Fin m, w.ofLp i • a i

Rockafellar's transpose A* is the adjoint, and on the rows it is w ↦ ∑ wᵢaᵢ; so the vector condition ∑ λᵢaᵢ = 0 of Theorem 22.1(b) reads A*w = 0.

theorem Rockafellar.theorem_22_1_matrix {m n : ℕ} {A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m} {a : Fin m → TdafSurface.Rn n} (h : IsRowsOf A a) (α : TdafSurface.Rn m) : (∃ (x : TdafSurface.Rn n), ∀ (i : Fin m), (A x).ofLp i ≤ α.ofLp i) ↔ ¬∃ (w : TdafSurface.Rn m), (∀ (i : Fin m), 0 ≤ w.ofLp i) ∧ (LinearMap.adjoint A) w = 0 ∧ ((TdafSurface.pairing m) w) α < 0

Theorem 22.1 in matrix form (p. 201). With A the matrix whose rows are the aᵢ, alternative (a) is Ax ≤ a and alternative (b) is w ≥ 0, A*w = 0, ⟨w, a⟩ < 0: whatever the coefficients, exactly one of the two systems has a solution.

The interval form

def Rockafellar.IsRealInterval (I : Set ℝ) : Prop

Real interval (p. 202): "by a real interval we mean merely a convex subset of R; thus Iⱼ may be open or closed or neither, and it may consist of just a single number".

Equations

• Rockafellar.IsRealInterval I = Convex ℝ I

def Rockafellar.rectangle {N : ℕ} (I : Fin N → Set ℝ) : Set (TdafSurface.Rn N)

The generalized rectangle C = {(ζ₁, …, ζ_N) | ζⱼ ∈ Iⱼ, j = 1, …, N} of p. 203, the set the subspace L of Theorem 22.6 either meets or is separated from.

Equations

• Rockafellar.rectangle I = {z : TdafSurface.Rn N | ∀ (j : Fin N), z.ofLp j ∈ I j}

@[simp]

theorem Rockafellar.mem_rectangle {N : ℕ} {I : Fin N → Set ℝ} {z : TdafSurface.Rn N} : z ∈ rectangle I ↔ ∀ (j : Fin N), z.ofLp j ∈ I j

theorem Rockafellar.convex_rectangle {N : ℕ} {I : Fin N → Set ℝ} (h : ∀ (j : Fin N), IsRealInterval (I j)) : Convex ℝ (rectangle I)

A generalized rectangle of real intervals is convex.

def Rockafellar.intervalCombo {N : ℕ} (z : TdafSurface.Rn N) (I : Fin N → Set ℝ) : Set ℝ

The set ζ*₁I₁ + ⋯ + ζ*_N I_N of p. 202, the left side of Rockafellar's Σ ζ*ⱼIⱼ > 0.

Equations

• Rockafellar.intervalCombo z I = ∑ j : Fin N, z.ofLp j • I j

def Rockafellar.posIntervalCombo {N : ℕ} (z : TdafSurface.Rn N) (I : Fin N → Set ℝ) : Prop

Rockafellar's Σ ζ*ⱼIⱼ > 0 (p. 202), which is a set containment: ζ*₁ζ₁ + ⋯ + ζ*_NζN > 0 for every choice of ζⱼ ∈ Iⱼ, that is, Σ ζ*ⱼIⱼ ⊆ (0, +∞).

Equations

• Rockafellar.posIntervalCombo z I = (Rockafellar.intervalCombo z I ⊆ Set.Ioi 0)

theorem Rockafellar.posIntervalCombo_iff {N : ℕ} {z : TdafSurface.Rn N} {I : Fin N → Set ℝ} : posIntervalCombo z I ↔ ∀ c ∈ intervalCombo z I, 0 < c

theorem Rockafellar.isRealInterval_intervalCombo {N : ℕ} (z : TdafSurface.Rn N) {I : Fin N → Set ℝ} (h : ∀ (j : Fin N), IsRealInterval (I j)) : IsRealInterval (intervalCombo z I)

"The set Σ ζ*ⱼIⱼ is a real interval, by the way, since a linear combination of convex sets is convex" (p. 203).

The interval reading of a linear system (p. 202)

A system in ℝⁿ with m constraints becomes a rectangle problem in ℝᴺ, N = n + m: append the m constraint values to the n unknowns, and the system says exactly that the resulting vector lies both in a fixed n-dimensional subspace L — the graph of A, written in ℝᴺ — and in the generalized rectangle cut out by the intervals I₁, …, I_N. Which system one started from survives only in the choice of intervals.

noncomputable def Rockafellar.intervalVector {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (x : TdafSurface.Rn n) : TdafSurface.Rn (n + m)

The vector z = (ξ₁, …, ξ_n, (Ax)₁, …, (Ax)_m) of ℝᴺ, N = n + m, that a solution x becomes when the constraint values are appended to the unknowns (p. 202).

Equations

• Rockafellar.intervalVector A x = (Tdaf.ConvexAnalysis.euclideanProdEquiv n m) (x, A x)

@[simp]

theorem Rockafellar.intervalVector_castAdd {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (x : TdafSurface.Rn n) (j : Fin n) : (intervalVector A x).ofLp (Fin.castAdd m j) = x.ofLp j

@[simp]

theorem Rockafellar.intervalVector_natAdd {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (x : TdafSurface.Rn n) (i : Fin m) : (intervalVector A x).ofLp (Fin.natAdd n i) = (A x).ofLp i

noncomputable def Rockafellar.intervalSubspace {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) : Submodule ℝ (TdafSurface.Rn (n + m))

The subspace L of p. 202: the vectors z ∈ ℝᴺ with ζ_{n+i} = ∑ⱼ αᵢⱼζⱼ, that is the graph of A written in ℝᴺ. Theorem 22.6 is stated about it, in place of the matrix.

Equations

• Rockafellar.intervalSubspace A = (↑↑(Tdaf.ConvexAnalysis.euclideanProdEquiv n m) ∘ₗ LinearMap.id.prod A).range

@[simp]

theorem Rockafellar.mem_intervalSubspace {m n : ℕ} {A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m} {z : TdafSurface.Rn (n + m)} : z ∈ intervalSubspace A ↔ ∃ (x : TdafSurface.Rn n), intervalVector A x = z

theorem Rockafellar.intervalVector_mem_rectangle {m n : ℕ} {A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m} {x : TdafSurface.Rn n} {I : Fin (n + m) → Set ℝ} : intervalVector A x ∈ rectangle I ↔ (∀ (j : Fin n), x.ofLp j ∈ I (Fin.castAdd m j)) ∧ ∀ (i : Fin m), (A x).ofLp i ∈ I (Fin.natAdd n i)

A vector lies in the rectangle exactly when its unknowns and its constraint values do.

def Rockafellar.leIntervals (n : ℕ) {m : ℕ} (α : TdafSurface.Rn m) : Fin (n + m) → Set ℝ

The intervals of the system Ax ≤ a (p. 202): Iⱼ = (-∞, +∞) for j = 1, …, n and I_{n+i} = (-∞, αᵢ] for i = 1, …, m.

Equations

• Rockafellar.leIntervals n α i = Fin.addCases (fun (x : Fin n) => Set.univ) (fun (i : Fin m) => Set.Iic (α.ofLp i)) i

@[simp]

theorem Rockafellar.leIntervals_castAdd {n m : ℕ} (α : TdafSurface.Rn m) (j : Fin n) : leIntervals n α (Fin.castAdd m j) = Set.univ

@[simp]

theorem Rockafellar.leIntervals_natAdd {n m : ℕ} (α : TdafSurface.Rn m) (i : Fin m) : leIntervals n α (Fin.natAdd n i) = Set.Iic (α.ofLp i)

def Rockafellar.nonnegEqIntervals (n : ℕ) {m : ℕ} (α : TdafSurface.Rn m) : Fin (n + m) → Set ℝ

The intervals of the system x ≥ 0, Ax = a (p. 202): Iⱼ = [0, +∞) for j = 1, …, n and I_{n+i} = {αᵢ} for i = 1, …, m.

Equations

• Rockafellar.nonnegEqIntervals n α i = Fin.addCases (fun (x : Fin n) => Set.Ici 0) (fun (i : Fin m) => {α.ofLp i}) i

@[simp]

theorem Rockafellar.nonnegEqIntervals_castAdd {n m : ℕ} (α : TdafSurface.Rn m) (j : Fin n) : nonnegEqIntervals n α (Fin.castAdd m j) = Set.Ici 0

@[simp]

theorem Rockafellar.nonnegEqIntervals_natAdd {n m : ℕ} (α : TdafSurface.Rn m) (i : Fin m) : nonnegEqIntervals n α (Fin.natAdd n i) = {α.ofLp i}

theorem Rockafellar.interval_reading_le {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (α : TdafSurface.Rn m) : (∃ (x : TdafSurface.Rn n), ∀ (i : Fin m), (A x).ofLp i ≤ α.ofLp i) ↔ (↑(intervalSubspace A) ∩ rectangle (leIntervals n α)).Nonempty

p. 202, the first interval reading: Ax ≤ a has a solution in ℝⁿ exactly when L meets the generalized rectangle cut out by Iⱼ = (-∞, +∞) for j ≤ n and I_{n+i} = (-∞, αᵢ]. This is the correspondence the second half of §22 is stated over.

theorem Rockafellar.interval_reading_nonneg_eq {m n : ℕ} (A : TdafSurface.Rn n →ₗ[ℝ] TdafSurface.Rn m) (α : TdafSurface.Rn m) : (∃ (x : TdafSurface.Rn n), (∀ (j : Fin n), 0 ≤ x.ofLp j) ∧ A x = α) ↔ (↑(intervalSubspace A) ∩ rectangle (nonnegEqIntervals n α)).Nonempty

Rockafellar, p. 202, the second interval reading: the system x ≥ 0, Ax = a in ℝⁿ has a solution exactly when the subspace L meets the generalized rectangle cut out by Iⱼ = [0, +∞) for j ≤ n and I_{n+i} = {αᵢ}.

theorem Rockafellar.isRealInterval_leIntervals {n m : ℕ} (α : TdafSurface.Rn m) (j : Fin (n + m)) : IsRealInterval (leIntervals n α j)

The intervals of both readings are real intervals, so both rectangles are convex — which is what makes the conjectured alternative of Theorem 22.6 a separation theorem.

theorem Rockafellar.isRealInterval_nonnegEqIntervals {n m : ℕ} (α : TdafSurface.Rn m) (j : Fin (n + m)) : IsRealInterval (nonnegEqIntervals n α j)