Finite Farkas lemma and finite LP strong duality

Built on fg_cone_isClosed (Weyl, in FgConeClosed.lean) and Mathlib's convex-cone hyperplane separation:

• LeanPool.Erdos81PaperIContrib.farkas_ge — finite Farkas lemma (inequality form).
• LeanPool.Erdos81PaperIContrib.covering_packing_duality — finite LP duality (covering/packing form): a maximum packing is attained and its value equals the covering infimum.

These stay over EuclideanSpace ℝ ι (a finite-dimensional real inner-product space), the natural setting for the ProperCone/inner-dual separation used here.

The Farkas and LP conclusions overlap the pooled Duality project's more general inequalityFarkas_neg and StandardLP.strongDuality results. This module gives a self-contained specialization built directly from the finitely generated cone closedness theorem in FgConeClosed.lean.

noncomputable def LeanPool.Erdos81PaperIContrib.toE {ι : Type u_1} (f : ι → ℝ) : EuclideanSpace ℝ ι

A real vector viewed in EuclideanSpace ℝ ι by its coordinates.

Equations

• LeanPool.Erdos81PaperIContrib.toE f = (WithLp.equiv 2 (ι → ℝ)).symm f

@[simp]

theorem LeanPool.Erdos81PaperIContrib.toE_apply {ι : Type u_1} (f : ι → ℝ) (i : ι) : (toE f).ofLp i = f i

theorem LeanPool.Erdos81PaperIContrib.inner_toE {ι : Type u_1} [Fintype ι] (f : ι → ℝ) (y : EuclideanSpace ℝ ι) : inner ℝ (toE f) y = ∑ i : ι, f i * y.ofLp i

theorem LeanPool.Erdos81PaperIContrib.farkas_ge {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (N : ι → κ → ℝ) (c : ι → ℝ) (hinfeas : ¬∃ (x : κ → ℝ), (∀ (j : κ), 0 ≤ x j) ∧ ∀ (i : ι), c i ≤ ∑ j : κ, N i j * x j) : ∃ (y : ι → ℝ), (∀ (i : ι), 0 ≤ y i) ∧ (∀ (j : κ), ∑ i : ι, N i j * y i ≤ 0) ∧ 0 < ∑ i : ι, c i * y i

Finite Farkas lemma (inequality form). If the primal system x ≥ 0, N x ≥ c is infeasible, then there is a Farkas certificate y ≥ 0 with Nᵀ y ≤ 0 and ⟨c, y⟩ > 0.

theorem LeanPool.Erdos81PaperIContrib.covering_packing_duality {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (A : ι → κ → ℝ) (r : ι → ℝ) (hA : ∀ (e : ι) (t : κ), 0 ≤ A e t) (hr : ∀ (e : ι), 0 ≤ r e) (hcol : ∀ (t : κ), ∃ (e : ι), 0 < A e t) : ∃ (w : κ → ℝ), (∀ (t : κ), 0 ≤ w t) ∧ (∀ (e : ι), ∑ t : κ, A e t * w t ≤ r e) ∧ ∑ t : κ, w t = sInf {v : ℝ | ∃ (x : ι → ℝ), (∀ (e : ι), 0 ≤ x e) ∧ (∀ (t : κ), 1 ≤ ∑ e : ι, A e t * x e) ∧ v = ∑ e : ι, r e * x e}

Finite LP duality (covering/packing). For a nonnegative incidence matrix A with nonnegative capacities r, in which every column has a positive entry, there is a maximum packing w whose unit-objective value equals the infimum cost of nonnegative coverings with unit demand. This conclusion does not assert that the covering infimum is attained.