# 線性規劃對偶

對固定primal max c^Tx、Ax≤b、x≥0，其dual為min b^Ty、A^Ty≥c、y≥0；feasible pair滿足弱對偶。

mko-linear-program-duality · theorem · v0.10.0



## 數學敘述

先核A為m×n exact rational matrix、b∈R^m、c∈R^n，dual variable y∈R^m且A^Ty≥c。對feasible x,y逐項驗c^Tx≤y^TAx≤b^Ty。若兩方feasible且objectives相等，zero gap即同時給primal與dual optimality certificate。缺任一方feasibility時objective equality不證optimality；有限grid不證一般strong duality，infeasible或unbounded cases也不得套用。一般有限維LP strong duality保留為明示定理，非本輪enumeration結果。





## 代表公式（精確 TeX）

g(x,y)=b^\top*y-c^\top*x





## 成立條件


- 沿用唯一maximize/≤/nonnegative primal convention。
- matrix、vectors與candidate points皆為bounded exact rationals。





## 符號作用域


- g — 固定問題資料下的逐點對偶間隙函數
- A — 限制矩陣
- b — primal 右端向量
- c — primal 目標向量
- x — primal 候選點
- y — dual 候選點





## 直觀、定義與常見誤解

從固定primal完整構造dual。

weak duality chain逐項exact核對。

zero-gap certificate與strong-duality一般定理分層。

記號對齊候選：固定問題資料 (A,b,c)，g(x,y)=b^T y−c^T x 是依候選點 x,y 變動的純量間隙；A 留在周圍可行性陳述。對 maximize／≤／nonnegative 慣例，須 x>=0、Ax<=b、y>=0、A^Ty>=c 才能使用弱對偶的非負間隙證書；單純目標相等或有限 grid 不證一般 strong duality。

混用另一套dual符號，或只因兩個objective數字相等就宣稱optimal。





## 已採用的推導導讀

[弱對偶鏈與零間隙最優證書](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-linear-program-duality-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [線性規劃標準形](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-program-standard-form/) — 固定primal convention。
- [最佳化問題](https://ocme.evemisslab.com/zh-Hant/mko/mko-optimization-problem/) — feasible與optimal語義。
- [實數大小與順序](https://ocme.evemisslab.com/zh-Hant/mko/mko-order-relation/) — componentwise inequalities。





## 驗證界線

有限候選點或grid搜尋不能證一般strong duality；不處理infeasible/unbounded對偶分類。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

加入complementary slackness與LP optimality conditions。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/source13-20261018-linear-program-duality.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-linear-program-duality/index.md)