theorem helperForTheorem_22_1_dualMargin_realForm {m n : ℕ} (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ) (lam : Fin m →₀ ℝ) (ε : ℝ) (hmargin : ∀ (x : Fin n → ℝ), ↑ε ≤ ∑ i ∈ lam.support, ↑(lam i) * ↑(a i ⬝ᵥ x - α i)) (x : Fin n → ℝ) : ε ≤ ∑ i ∈ lam.support, lam i * (a i ⬝ᵥ x - α i)

Helper for Theorem 22.1: convert the EReal dual margin inequality from Theorem 21.4 into an ordinary real inequality over the finite support.

theorem helperForTheorem_22_1_dualMargin_to_linearCertificate {m n : ℕ} (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ) (lam : Fin m →₀ ℝ) (ε : ℝ) (hlamNonneg : ∀ (i : Fin m), 0 ≤ lam i) (hε : 0 < ε) (hmargin : ∀ (x : Fin n → ℝ), ε ≤ ∑ i ∈ lam.support, lam i * (a i ⬝ᵥ x - α i)) : ∃ (l : Fin m → ℝ), 0 ≤ l ∧ ∑ i : Fin m, l i • a i = 0 ∧ ∑ i : Fin m, l i * α i < 0

Helper for Theorem 22.1: a dual margin certificate for the affine family yields the classical nonnegative linear multiplier certificate.

theorem helperForTheorem_22_1_certificate_excludes_feasible {m n : ℕ} (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ) {x : Fin n → ℝ} (hx : ∀ (i : Fin m), a i ⬝ᵥ x ≤ α i) {l : Fin m → ℝ} (hl_nonneg : 0 ≤ l) (hsum_zero : ∑ i : Fin m, l i • a i = 0) (hscalar_neg : ∑ i : Fin m, l i * α i < 0) : False

Helper for Theorem 22.1: a feasible point and a negative nonnegative-multiplier certificate cannot coexist.

theorem farkasAlternative_linearInequalities {m n : ℕ} (a : Fin m → Fin n → ℝ) (α : Fin m → ℝ) : ((∃ (x : Fin n → ℝ), ∀ (i : Fin m), a i ⬝ᵥ x ≤ α i) ∨ ∃ (l : Fin m → ℝ), 0 ≤ l ∧ ∑ i : Fin m, l i • a i = 0 ∧ ∑ i : Fin m, l i * α i < 0) ∧ ¬((∃ (x : Fin n → ℝ), ∀ (i : Fin m), a i ⬝ᵥ x ≤ α i) ∧ ∃ (l : Fin m → ℝ), 0 ≤ l ∧ ∑ i : Fin m, l i • a i = 0 ∧ ∑ i : Fin m, l i * α i < 0)

Theorem 22.1: Let a_i ∈ ℝ^n and α_i ∈ ℝ for i = 1, ..., m. Exactly one of the following alternatives holds: (a) there exists x ∈ ℝ^n such that ⟪a_i, x⟫ ≤ α_i for every i; (b) there exist nonnegative real numbers λ_1, ..., λ_m such that ∑ i, λ_i a_i = 0 and ∑ i, λ_i α_i < 0.