Lean declarations

def EconCSLib.LinearProgramming.PrimalFeasible EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality
Primal feasibility: `∃ x, A x ≥ b ∧ x ≥ 0`.
```
def PrimalFeasible (A : I → Fin n → 𝕜) (b : I → 𝕜) : Prop :=
  ∃ x : Fin n → 𝕜, (∀ i, b i ≤ ∑ j, A i j * x j) ∧ (∀ j, 0 ≤ x j)
```
def EconCSLib.LinearProgramming.DualFeasible EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality
Dual feasibility of `u`: `u ≥ 0 ∧ uᵀA ≤ c`.
```
def DualFeasible (A : I → Fin n → 𝕜) (c : Fin n → 𝕜) (u : I → 𝕜) : Prop :=
  (∀ i, 0 ≤ u i) ∧ (∀ j, ∑ i, u i * A i j ≤ c j)
```

theorem EconCSLib.LinearProgramming.lp_weak_duality EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality

theorem lp_weak_duality (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜)
    {x : Fin n → 𝕜} (hxA : ∀ i, b i ≤ ∑ j, A i j * x j) (hxnn : ∀ j, 0 ≤ x j)
    {u : I → 𝕜} (hu_du : DualFeasible A c u) :
    ∑ i, u i * b i ≤ ∑ j, c j * x j

abbrev EconCSLib.LinearProgramming.DualAugRow EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality
Augmented row index for the LP-Farkas reduction.
```
abbrev DualAugRow (I : Type*) (n : ℕ) : Type _ := I ⊕ Fin n
```

def EconCSLib.LinearProgramming.dualAugA EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality

Augmented matrix combining `A` rows with `x ≥ 0` unit rows.

def dualAugA (A : I → Fin n → 𝕜) : DualAugRow I n → Fin n → 𝕜
  | Sum.inl i, j => A i j
  | Sum.inr j', j => if j = j' then 1 else 0

/-- Augmented RHS. -/

def EconCSLib.LinearProgramming.dualAugB EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality

Augmented RHS.

def dualAugB (b : I → 𝕜) : DualAugRow I n → 𝕜
  | Sum.inl i => b i
  | Sum.inr _ => 0

@[simp] theorem dualAugA_inl (A : I → Fin n → 𝕜) (i : I) (j : Fin n) :
    dualAugA A (Sum.inl i) j = A i j := rfl

theorem EconCSLib.LinearProgramming.isFeasible_dualAug_iff EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality
Augmented feasibility is the primal feasibility (with `x ≥ 0`).
```
theorem isFeasible_dualAug_iff (A : I → Fin n → 𝕜) (b : I → 𝕜) :
    IsFeasible (dualAugA A) (dualAugB b) ↔ PrimalFeasible A b
```

theorem EconCSLib.LinearProgramming.lp_strong_duality EconCSLib @ cef01c7, EconCSLib.Math.LinearProgramming.StrongDuality

theorem lp_strong_duality (A : I → Fin n → 𝕜) (b : I → 𝕜) (c : Fin n → 𝕜) (d : 𝕜)
    (hP_feas : PrimalFeasible A b)
    (hP_bound : ∀ x : Fin n → 𝕜,
      (∀ i, b i ≤ ∑ j, A i j * x j) → (∀ j, 0 ≤ x j) → d ≤ ∑ j, c j * x j) :
    ∃ u : I → 𝕜, DualFeasible A c u ∧ d ≤ ∑ i, u i * b i

Modules: EconCSLib.Math.LinearProgramming.StrongDuality

Strong Duality For Linear Programming

Setup

Fix a linearly ordered field $\mathbb{K}$, a finite nonempty index type $I$, and $n \in \mathbb{N}$. Let $A \colon I \times \mathrm{Fin}\,n \to \mathbb{K}$, $b \colon I \to \mathbb{K}$, $c \colon \mathrm{Fin}\,n \to \mathbb{K}$. Consider the standard-form linear programming pair:

Primal $\mathrm{P}$: $\min \langle c, x\rangle$ subject to $A x \ge b$ and $x \ge 0$ (i.e. $x_j \ge 0$ for every $j \in \mathrm{Fin}\,n$).
Dual $\mathrm{D}$: $\max \langle u, b\rangle$ subject to $u^{\mathsf T} A \le c$ (componentwise, i.e. $\sum_i u_i A_{ij} \le c_j$ for every $j$) and $u \ge 0$.

Statements

Weak duality. For every primal-feasible $x$ and dual-feasible $u$, $\langle c, x\rangle \ge \langle u, b\rangle$.

Strong duality. If the primal is feasible and bounded below by $d \in \mathbb{K}$ (i.e. $\langle c, x\rangle \ge d$ for every primal-feasible $x$), then there exists a dual-feasible $u$ with $\langle u, b\rangle \ge d$.

Combining the two yields that the optimal primal and dual values coincide when either exists.

Proof

Weak duality

Let $x$ be primal-feasible and $u$ dual-feasible. Weighting the primal constraints by $u \ge 0$: $$ \langle u, A x\rangle = \langle u^{\mathsf T} A, x\rangle \le \langle c, x\rangle $$ (using $u^{\mathsf T} A \le c$ and $x \ge 0$, so weighting term by term preserves $\le$). And $\langle u, A x\rangle \ge \langle u, b\rangle$ from $A x \ge b$ and $u \ge 0$. Hence $\langle c, x\rangle \ge \langle u, b\rangle$.

Strong duality

Apply the Farkas lemma (Farkas Lemma) to the augmented system that combines $A x \ge b$ and $x \ge 0$. Concretely, define $A_{\mathrm{aug}} \colon (I \sqcup \mathrm{Fin}\,n) \times \mathrm{Fin}\,n \to \mathbb{K}$ and $b_{\mathrm{aug}} \colon I \sqcup \mathrm{Fin}\,n \to \mathbb{K}$ by

$A_{\mathrm{aug}}(\mathrm{inl}\,i,\, j) = A_{i,j}$, $b_{\mathrm{aug}}(\mathrm{inl}\,i) = b_i$ for $i \in I$ (the original rows);
$A_{\mathrm{aug}}(\mathrm{inr}\,j',\, j) = [j = j']$ (Kronecker delta) and $b_{\mathrm{aug}}(\mathrm{inr}\,j') = 0$ for $j' \in \mathrm{Fin}\,n$ (the unit rows $x_{j'} \ge 0$).

Primal feasibility coincides with feasibility of $A_{\mathrm{aug}}\,x \ge b_{\mathrm{aug}}$. By hypothesis, the primal is feasible and bounded below by $d$. Farkas yields $u_{\mathrm{aug}} \colon I \sqcup \mathrm{Fin}\,n \to \mathbb{K}$ with $u_{\mathrm{aug}} \ge 0$, $u_{\mathrm{aug}}^{\mathsf T} A_{\mathrm{aug}} = c$, and $\langle u_{\mathrm{aug}}, b_{\mathrm{aug}}\rangle \ge d$.

Decompose $u_{\mathrm{aug}} = (u, v)$ with $u \colon I \to \mathbb{K}$ and $v \colon \mathrm{Fin}\,n \to \mathbb{K}$. The column conditions read

For each $j \in \mathrm{Fin}\,n$: $\sum_i u_i A_{i,j} + \sum_{j'} v_{j'} [j = j'] = c_j$, i.e. $u^{\mathsf T} A\, j + v_j = c_j$, i.e. $u^{\mathsf T} A = c - v$. Since $v \ge 0$, $u^{\mathsf T} A \le c$.

The RHS condition reads $$ \langle u_{\mathrm{aug}}, b_{\mathrm{aug}}\rangle = \langle u, b\rangle + \langle v, 0\rangle = \langle u, b\rangle \ge d. $$

So $u \ge 0$, $u^{\mathsf T} A \le c$ (dual feasibility), and $\langle u, b\rangle \ge d$. This is the required dual-feasible point with dual objective at least $d$.

Remarks

The proof is purely algebraic and constructive: the dual certificate $u$ is built explicitly from the Farkas certificate of the augmented system.
Works over any linearly ordered field (in particular $\mathbb{Q}$).
"Optimal value" is not used as a primitive; instead, the theorem is phrased for any lower bound $d$. The primal optimum is recovered by combining strong duality with weak duality: $$ \sup_{u \text{ dual-feasible}} \langle u, b\rangle \;\ge\; d \quad\text{whenever}\quad d \le \inf_{x \text{ primal-feasible}}\langle c, x\rangle, $$ and weak duality gives the converse inequality.

Consequences

Complementary slackness: optimal primal-dual pairs satisfy strict slack conditions on every variable (downstream from this theorem).
Matrix-game value: zero-sum value computed via row and column LPs (downstream from this theorem).

References

[MFoGT, Section 2.8, Exercise 9] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Primal-dual strong duality for linear programming.