Finite Standard-Form Primal and Dual Linear Programs

PrimalDual.FinitePrimalDual: For arbitrary types $\iota$ and $\kappa$, with no finiteness, nonemptiness, or other typeclass assumptions, a finite-primal-dual datum $P$ consists of three unrestricted real-valued functions: coefficients $a=P.\mathrm{coeff}:\iota\to\kappa\to\mathbb R$, a right-hand side $b=P.\mathrm{rhs}:\kappa\to\mathbb R$, and a cost $c=P.\mathrm{cost}:\iota\to\mathbb R$. No sign or boundedness conditions are imposed. Either indexing type may be empty or infinite; for an empty domain the corresponding functions are the unique empty-domain functions.

PrimalDual.FinitePrimalDual.primalConstraintValue: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\iota$ but no finiteness assumption on $\kappa$, a datum $P$ with coefficients $a:\iota\to\kappa\to\mathbb R$, an arbitrary vector $x:\iota\to\mathbb R$, and an index $j:\kappa$, the primal constraint value is the real number $\sum_{i\in\iota}a_{ij}x_i$. Neither $a$ nor $x$ is assumed nonnegative. If $\iota$ is empty, the sum is $0$; if $\kappa$ is empty, there is no index $j$ at which this function can be evaluated.

PrimalDual.FinitePrimalDual.dualConstraintValue: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\kappa$ but no finiteness assumption on $\iota$, a datum $P$ with coefficients $a:\iota\to\kappa\to\mathbb R$, an arbitrary vector $y:\kappa\to\mathbb R$, and an index $i:\iota$, the dual constraint value is the real number $\sum_{j\in\kappa}a_{ij}y_j$. Neither $a$ nor $y$ is assumed nonnegative. If $\kappa$ is empty, the sum is $0$; if $\iota$ is empty, there is no index $i$ at which this function can be evaluated.

PrimalDual.FinitePrimalDual.primalObjective: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\iota$ but no finiteness assumption on $\kappa$, a datum $P$ with cost $c:\iota\to\mathbb R$, and an arbitrary vector $x:\iota\to\mathbb R$, the primal objective is $\sum_{i\in\iota}c_i x_i$. No sign or feasibility assumptions are imposed on $c$ or $x$. If $\iota$ is empty, this objective equals $0$.

PrimalDual.FinitePrimalDual.dualObjective: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\kappa$ but no finiteness assumption on $\iota$, a datum $P$ with right-hand side $b:\kappa\to\mathbb R$, and an arbitrary vector $y:\kappa\to\mathbb R$, the dual objective is $\sum_{j\in\kappa}b_j y_j$. No sign or feasibility assumptions are imposed on $b$ or $y$. If $\kappa$ is empty, this objective equals $0$.

PrimalDual.FinitePrimalDual.PrimalFeasible: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\iota$ but no finiteness assumption on $\kappa$, a datum $P=(a,b,c)$, and an arbitrary vector $x:\iota\to\mathbb R$, primal feasibility is exactly the conjunction $(\forall i\in\iota,\ 0\le x_i)$ and $(\forall j\in\kappa,\ b_j\le\sum_{i\in\iota}a_{ij}x_i)$. No separate sign assumptions are imposed on $a,b,$ or $c$, and $c$ does not occur in the condition. If $\iota$ is empty, the first clause is vacuous and every displayed sum is $0$, so feasibility reduces to $b_j\le0$ for every $j$; if $\kappa$ is empty, the second clause is vacuous; if both are empty, the proposition holds.

PrimalDual.FinitePrimalDual.DualFeasible: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\kappa$ but no finiteness assumption on $\iota$, a datum $P=(a,b,c)$, and an arbitrary vector $y:\kappa\to\mathbb R$, dual feasibility is exactly the conjunction $(\forall j\in\kappa,\ 0\le y_j)$ and $(\forall i\in\iota,\ \sum_{j\in\kappa}a_{ij}y_j\le c_i)$. No separate sign assumptions are imposed on $a,b,$ or $c$, and $b$ does not occur in the condition. If $\kappa$ is empty, the first clause is vacuous and every displayed sum is $0$, so feasibility reduces to $0\le c_i$ for every $i$; if $\iota$ is empty, the second clause is vacuous; if both are empty, the proposition holds.

PrimalDual.FinitePrimalDual.SatisfiesPrimalApproxCS: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\kappa$ but no finiteness assumption on $\iota$, a datum $P=(a,b,c)$, an arbitrary real number $\alpha$, and arbitrary vectors $x:\iota\to\mathbb R$ and $y:\kappa\to\mathbb R$, this proposition asserts that for every $i\in\iota$, $0<x_i$ implies both $c_i/\alpha\le\sum_{j\in\kappa}a_{ij}y_j$ and $\sum_{j\in\kappa}a_{ij}y_j\le c_i$. It assumes neither primal nor dual feasibility and imposes nothing at indices with $x_i\le0$; hence it holds vacuously if $\iota$ is empty or $x$ has no positive component. The parameter $\alpha$ may be any real number, including zero or a negative number; division is total, so $c_i/0=0$. If $\kappa$ is empty, each sum is $0$.

PrimalDual.FinitePrimalDual.SatisfiesDualApproxCS: For arbitrary types $\iota,\kappa$, a chosen Fintype structure on $\iota$ but no finiteness assumption on $\kappa$, a datum $P=(a,b,c)$, an arbitrary real number $\beta$, and arbitrary vectors $x:\iota\to\mathbb R$ and $y:\kappa\to\mathbb R$, this proposition asserts that for every $j\in\kappa$, $0<y_j$ implies both $b_j\le\sum_{i\in\iota}a_{ij}x_i$ and $\sum_{i\in\iota}a_{ij}x_i\le\beta b_j$. It assumes neither primal nor dual feasibility and imposes nothing at indices with $y_j\le0$; hence it holds vacuously if $\kappa$ is empty or $y$ has no positive component. The parameter $\beta$ may be any real number, including zero or a negative number. If $\iota$ is empty, each sum is $0$.

PrimalDual.FinitePrimalDual.IsCoveringPacking: For arbitrary types $\iota,\kappa$, with no finiteness, nonemptiness, or other typeclass assumptions, and a datum $P=(a,b,c)$, this proposition is a structure whose inhabitant supplies all three proofs $\forall i\in\iota\,\forall j\in\kappa,\ 0\le a_{ij}$, $\forall j\in\kappa,\ 0\le b_j$, and $\forall i\in\iota,\ 0\le c_i$. If $\iota$ is empty, the coefficient and cost conditions are vacuous; if $\kappa$ is empty, the coefficient and right-hand-side conditions are vacuous; if both are empty, all three conditions are vacuous.