Motivation

A loss network is a model of a circuit-switched network: telephone networks, and more generally any system in which a request seizes several resources at once and is lost if any of them is unavailable. Exact loss probabilities in such networks are given by a product-form distribution over a state space whose size grows exponentially with the number of routes, so practitioners compute an approximation instead: the Erlang fixed point, also called the reduced-load approximation. It pretends that links block independently, computes the traffic offered to each link after thinning by the other links, and applies Erlang's single-link formula link by link. Reduced-load approximations of this kind recur throughout §§3–4 of Kelly 1991, where they appear as limits of networks with fixed and with alternative routing.

An approximation defined by a fixed point equation raises an immediate question: does the equation have exactly one solution? Under fixed routing it does, and Kelly's Theorem 3.7 (Ann. Appl. Probab. 1991, p. 338, citing Kelly 1986, reference [33] of the paper) proves it by identifying the fixed point with the optimum of a strictly convex program, the revised dual problem. The convex characterization is specific to fixed routing; the paper notes (p. 337) that for networks with dynamic routing and control nonuniquely determined behaviour can occur.

Setting

There are $J$ links, link $j$ having $C_j \ge 1$ circuits, and a finite set of routes $r$. A call on route $r$ uses $A_{jr} \in \mathbb Z_+$ circuits of link $j$, and calls on route $r$ arrive as a Poisson stream of rate $\nu_r > 0$.

Erlang's formula (1.1) gives the blocking probability of a single link with $C$ circuits offered Poisson traffic of intensity $\nu$:

$$E(\nu, C) = \frac{\nu^C}{C!}\Big[\sum_{n=0}^{C} \frac{\nu^n}{n!}\Big]^{-1}.$$

The Erlang fixed point equations (3.1)–(3.2) for the vector of link blocking probabilities $(E_1, \dots, E_J)$ are

$$E_j = E(\rho_j, C_j), \qquad \rho_j = (1 - E_j)^{-1} \sum_r A_{jr}\,\nu_r \prod_i (1 - E_i)^{A_{ir}}, \qquad j = 1, \dots, J.$$

The utilization function $U(y, C)$ is defined by the implicit relation (3.4),

$$U\big(-\log(1 - E(\nu, C)),\, C\big) = \nu\,\big(1 - E(\nu, C)\big), \qquad \nu \ge 0:$$

the mean number of busy circuits on a single link whose blocking probability is $1 - e^{-y}$.

The revised dual problem (3.5) is

$$\text{minimize} \quad \sum_r \nu_r \exp\Big(-\sum_j y_j A_{jr}\Big) + \sum_j \int_0^{y_j} U(z, C_j)\,dz \qquad \text{subject to } y \ge 0,$$

and its stationarity conditions (3.6) are

$$\sum_r A_{jr}\,\nu_r \exp\Big(-\sum_i y_i A_{ir}\Big) = U(y_j, C_j), \qquad j = 1, \dots, J.$$

The revised dual differs from the dual problem (2.3) of §2, whose optimum gives the limiting blocking probabilities of a large network, only in its last term: $\sum_j y_j C_j$ becomes $\sum_j \int_0^{y_j} U(z, C_j)\,dz$.

Formalization targets

Goal: Theorem 3.7

The revised dual problem (3.5) has an optimum $y$, every optimum equals $y$, and

$$E \in [0,1]^J \text{ solves (3.1)–(3.2)} \iff E_j = 1 - \exp(-y_j) \text{ for every } j.$$

The goal states the characterization, not only the existence and uniqueness of the fixed point: the solution is $1 - e^{-y}$ for the optimum $y$ of (3.5).

Milestones (p. 338, in the order the argument uses them)

1. (3.4) defines a function: $\nu \mapsto -\log(1 - E(\nu, C))$ is a continuous strictly increasing bijection of $[0,\infty)$ onto itself for $C \ge 1$, $U$ satisfies (3.4), and $U \ge 0$.
2. $y \mapsto U(y, C)$ is strictly increasing on $[0, \infty)$.
3. $y \mapsto \int_0^y U(z, C)\,dz$ is strictly convex, and so is the objective of (3.5) on $y \ge 0$.
4. (3.5) has exactly one optimum.
5. A vector $y \ge 0$ is optimal for (3.5) if and only if it satisfies (3.6).
6. A solution of (3.1)–(3.2) in $[0,1]^J$ has all $E_j < 1$; and for $y \ge 0$, $E_j = 1 - e^{-y_j}$ solves (3.1)–(3.2) if and only if $y$ satisfies (3.6).

Significance

The theorem turns a nonlinear system of $J$ equations into a smooth strictly convex minimization over the nonnegative orthant. Uniqueness of the fixed point follows at once, and the program gives a computational handle: any convex-minimization method computes the Erlang fixed point, without relying on the convergence of repeated substitution. The comparison with the dual problem (2.3) also explains the approximation: (3.6) relaxes the conditions (2.7), which force a link's carried traffic to equal its capacity before it can block, into a smooth relation in which blocking grows with carried traffic as Erlang's formula prescribes (Remark 3.8).

On Prove2Me, existence and uniqueness of the fixed point alone is already the Proved theorem KellyStochasticNetworks.erlang_fixed_point_unique (Kelly–Yudovina, Stochastic Networks, Theorem 3.20), referenced by this mission. Also referenced: KellyStochasticNetworks.erlang_strictMono (Proved: $\nu \mapsto E(\nu, C)$ and $\nu \mapsto \nu(1 - E(\nu, C))$ are strictly increasing for $C \ge 1$) and KellyStochasticNetworks.erlang_mean_busy_circuits (Proved: the mean number of busy circuits is $\nu(1 - E(\nu, C))$, the reading of $U$ as a utilization). What this mission adds is the revised dual problem itself, the utilization function $U$, and the identification of the fixed point with the optimum of (3.5); none of these is formalized on the platform.

Difficulty

The function $U$ is defined only implicitly, through the inverse of $\nu \mapsto -\log(1 - E(\nu, C))$, so every property of the objective of (3.5) passes through properties of Erlang's formula: monotonicity, continuity, and the limit $E(\nu, C) \to 1$ as $\nu \to \infty$. Differentiating $\int_0^{y} U$ needs continuity of $U$, which must be derived from the inverse.

The paper's sentence "strictly convex: it thus has a unique minimum" covers only uniqueness. Existence of a minimizer on the unbounded set $y \ge 0$ is a separate fact, a growth estimate for the integral terms, and it is part of milestone 4. The first term of (3.5) is not strictly convex when $A$ has rank less than $J$, so strict convexity must come from the separable integral terms. Finally, optimality over $y \ge 0$ yields only one-sided conditions at coordinates with $y_j = 0$; that (3.6) is an equality there uses $U(0, C) = 0$.

Formalization scope

Lean namespace KellyLossNetworks.RevisedDual. Links are Fin J, routes Fin R, the incidence matrix is A : Fin J → Fin R → ℕ, rates ν : Fin R → ℝ, capacities C : Fin J → ℕ, following the published Kelly–Yudovina definitions. Every statement assumes $\nu_r > 0$ and $C_j \ge 1$; the paper uses both without stating them, and a link with $C_j = 0$ makes (3.4) meaningless, since $E(\nu, 0) = 1$.

Erlang's formula is the published KellyStochasticNetworks.erlang and the fixed point equations (3.1)–(3.2) are the published KellyStochasticNetworks.ErlangFixedPoint, whose factor $(1 - E_j)^{-1}$ is Lean's total inverse; milestone 6 shows that no solution in $[0,1]^J$ reaches $E_j = 1$. Solutions are sought in $[0,1]^J$, as on p. 338.

$U$ is defined by choice: $U(y, C) = \nu(1 - E(\nu, C))$ for a $\nu \ge 0$ with $-\log(1 - E(\nu, C)) = y$, and $0$ if none exists. For $C \ge 1$, $y \ge 0$ the $\nu$ is unique, and that (3.4) holds is milestone 1, a theorem, not an axiom built into the definition. Values at $y < 0$ or $C = 0$ are placeholders that no statement uses. The integral in (3.5) is the interval integral $\int_0^{y_j}$. An optimum of (3.5) is a $y \ge 0$ whose objective value is at most that of every $z \ge 0$.

A trivializing formalization is ruled out: replacing $U$ by any closed form other than the one fixed by (3.4) (for instance $U(z, C) = C$, the fluid utilization of Remark 3.8) would change the problem and reduce (3.5) to the dual (2.3); and the goal asserts the identification $E = 1 - e^{-y}$ rather than restating the existence and uniqueness that is already Proved.

A complete development needs: inverse-function arguments for a strictly increasing continuous map of $[0, \infty)$, derivatives of interval integrals with continuous integrands, strict convexity of separable sums, and first-order optimality conditions for convex functions on the nonnegative orthant. The facts about Erlang's formula and about $U$ are reusable in any reduced-load analysis. Proofs of individual milestones are welcome independently.

Selected references

• F. P. Kelly, Loss networks, The Annals of Applied Probability 1(3):319–378, 1991. https://doi.org/10.1214/aoap/1177005872
• F. P. Kelly, Blocking probabilities in large circuit-switched networks, Advances in Applied Probability 18:473–505, 1986 (reference [33] of Kelly 1991; DOI not verified offline).
• F. P. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014 (the source of the Proved platform items referenced here; DOI not verified offline).

Motivation

Nonlinear conjugate gradient methods minimize a smooth function $f$ of $n$ variables using only function values, gradients and a few vectors of storage. They are the method of choice when $n$ is so large that quasi-Newton matrices cannot be stored, and they remain a standard component of large-scale optimization software. Their convergence theory is delicate: the classical results assume exact line searches, while practical codes accept any steplength satisfying inexpensive inexact conditions.

Gilbert and Nocedal (INRIA RR-1268, 1990; journal version SIAM J. Optim. 2 (1992)) organized the global convergence theory of these methods around a single device and proved two families of results. This mission covers the first: every conjugate gradient method whose parameter $\beta_k$ is bounded in absolute value by the Fletcher–Reeves value converges under the strong Wolfe line search.

Timeline. Fletcher and Reeves (1964) and Polak and Ribière (1969) introduced the two best-known choices of $\beta_k$. Zoutendijk (1970) and Wolfe (1969, 1971) established the summability condition now called Zoutendijk's condition. Al-Baali (1985) proved that the Fletcher–Reeves method with the strong Wolfe line search and $\sigma_2 < \tfrac12$ generates descent directions and satisfies $\liminf\|g_k\| = 0$. Touati-Ahmed and Storey (1990) treated nonnegative hybrids. Gilbert and Nocedal (1990) extended Al-Baali's theorem to every $\beta_k$ with $|\beta_k| \le \beta_k^{FR}$, which admits negative values and yields a convergent modification of the Polak–Ribière method.

Setting

Let $E$ be a finite-dimensional real inner product space and $f : E \to \mathbb R$ continuously differentiable, with gradient $g = \nabla f$ for that inner product. Starting from $x_1$, the method generates

$$d_1 = -g_1,\qquad d_k = -g_k + \beta_k d_{k-1}\ (k\ge 2),\qquad x_{k+1} = x_k + \alpha_k d_k,$$

where $g_k = g(x_k)$, $\beta_k$ is a scalar and $\alpha_k > 0$ a steplength found by a one-dimensional search. The Fletcher–Reeves and Polak–Ribière scalars are

$$\beta_k^{FR} = \frac{\|g_k\|^2}{\|g_{k-1}\|^2},\qquad \beta_k^{PR} = \frac{\langle g_k, g_k - g_{k-1}\rangle}{\|g_{k-1}\|^2}.$$

Assumptions 2.1: the level set $\mathcal L = \{x : f(x) \le f(x_1)\}$ is bounded, and on an open neighbourhood $\mathcal N$ of $\mathcal L$ the gradient is Lipschitz: $\|g(x) - g(\tilde x)\| \le L\|x - \tilde x\|$.

A steplength satisfies the Wolfe conditions with $0 < \sigma_1 < \sigma_2 < 1$ if

$$f(x_k + \alpha_k d_k) \le f(x_k) + \sigma_1\alpha_k\langle g_k, d_k\rangle,\qquad \langle g(x_k+\alpha_k d_k), d_k\rangle \ge \sigma_2\langle g_k, d_k\rangle,$$

and the strong Wolfe conditions if the second inequality is replaced by $|\langle g(x_k+\alpha_k d_k), d_k\rangle| \le -\sigma_2\langle g_k, d_k\rangle$. The angle $\theta_k$ between $-g_k$ and $d_k$ is given by $\cos\theta_k = -\langle g_k, d_k\rangle/(\|g_k\|\|d_k\|)$, and the Zoutendijk condition is $\sum_{k\ge1}\cos^2\theta_k\|g_k\|^2 < \infty$.

Formalization targets

Goal: Theorem 3.2

Under Assumptions 2.1, for any method of the above form with

$$|\beta_k| \le \beta_k^{FR}\quad (k \ge 2)$$

and steplengths satisfying the strong Wolfe conditions with $0 < \sigma_1 < \sigma_2 < \tfrac12$,

$$\liminf_{k\to\infty}\|g_k\| = 0 .$$

The sequence $\beta_k$ is arbitrary within the bound; the statement contains no constants.

Milestones

• Theorem 2.1 (i) (Zoutendijk): for any iteration $x_{k+1} = x_k + \alpha_k d_k$ with descent directions and Wolfe steps, $\sum_{k\ge1}\cos^2\theta_k\|g_k\|^2 < \infty$.
• Lemma 3.1: under $|\beta_k| \le \beta_k^{FR}$ and the strong Wolfe curvature condition with $\sigma_2 < \tfrac12$, every $d_k$ is a descent direction and

$$-\sum_{j=0}^{k-1}\sigma_2^j \le \frac{\langle g_k, d_k\rangle}{\|g_k\|^2} \le -2 + \sum_{j=0}^{k-1}\sigma_2^j .$$

• (3.5): there are $c_1, c_2 > 0$ with $c_1\|g_k\|/\|d_k\| \le \cos\theta_k \le c_2\|g_k\|/\|d_k\|$.

Further statements

Theorem 2.1 (ii) (the same conclusion for an ideal line search that does no worse than the first stationary point along $d_k$) and the convergence of the hybrid method (3.7), $\beta_k = \max(-\beta_k^{FR}, \min(\beta_k^{PR}, \beta_k^{FR}))$.

Significance

Theorem 3.2 shows that descent and global convergence of Fletcher–Reeves-type methods do not depend on the exact formula for $\beta_k$, only on the bound $|\beta_k| \le \beta_k^{FR}$. Its main consequence is the hybrid method (3.7), which keeps the Polak–Ribière choice whenever it lies in $[-\beta_k^{FR}, \beta_k^{FR}]$, and so retains the practical efficiency of Polak–Ribière while inheriting the convergence guarantee of Fletcher–Reeves. Lemma 3.1 also shows that, under these conditions, descent need not be enforced by the line search.

The results are proved in the paper. To our knowledge none of them, nor Zoutendijk's theorem for general iterations, has a machine-checked proof in Lean; Mathlib has no theory of line search methods. A formalization would provide a reusable Zoutendijk theorem for any descent method with Wolfe steps, and a verified convergence statement for the conjugate gradient methods used in practice.

Difficulty

The obvious route to convergence of a descent method is to show $\cos\theta_k$ bounded away from zero and apply Zoutendijk's condition. For conjugate gradient methods this fails: $d_k$ accumulates previous directions and $\cos\theta_k$ can tend to zero. The argument must instead control the growth of $\|d_k\|$, which requires bounding $\langle g_k, d_{k-1}\rangle$ through the line search, and this in turn requires knowing that every $d_k$ is a descent direction with $\langle g_k, d_k\rangle$ comparable to $\|g_k\|^2$. The threshold $\sigma_2 < \tfrac12$ is exactly what keeps the geometric series in these bounds below $2$; the result fails without it.

Formalization scope

All items live in the namespace NonlinCG.FRBound. The space is a finite-dimensional real inner product space E (the paper uses "the scalar product used to compute the gradient"), and gradient f is the gradient for that product. Conventions committed to:

• Indexing follows the paper: sequences ℕ → E, used from index 1; index 0 is never constrained.
• Smoothness: every statement assumes $f$ globally $C^1$, from (1.1) "f is smooth", in addition to Assumptions 2.1 (bounded level set; $C^1$ and Lipschitz gradient on an open neighbourhood $\mathcal N$ of $\mathcal L$, with $L > 0$).
• Steplengths are positive, as in the paper's line searches.
• $\beta_k$ is a free sequence constrained by $|\beta_k| \le \beta_k^{FR}$, not the Fletcher–Reeves formula. Fixing $\beta_k = \beta_k^{FR}$ would state Al-Baali's theorem instead.
• Division: $\beta^{FR}$, $\beta^{PR}$, $\cos\theta_k$ are Lean divisions (value 0 on a zero denominator). Theorem 3.2 does not assume $g_k \ne 0$; Lemma 3.1 and (3.5) assume it, since the paper divides by $\|g_k\|^2$ there and descent is impossible at $g_k = 0$.
• Zoutendijk's sum is the summability of $\langle g_k, d_k\rangle^2/\|d_k\|^2$, which equals $\cos^2\theta_k\|g_k\|^2$ under descent.
• liminf is stated as: for every $\varepsilon > 0$ and $K$ there is $k \ge K$ with $\|g_k\| < \varepsilon$.
• (3.5) asserts existence of the constants only, as the paper does.

The goal does not assume Zoutendijk's condition or descent: both are consequences (Theorem 2.1 and Lemma 3.1) and assuming either would remove part of the theorem's content. The hypotheses are jointly satisfiable (for $f(x) = x^2/2$ on $\mathbb R$, $x_1 = 1$, $\beta_k = 0$, $\alpha_k = 0.9$, $\sigma_1 = 0.1$, $\sigma_2 = 0.25$), so the goal is not vacuous.

Needed infrastructure: line-search conditions, the descent lemma for functions with Lipschitz gradient on a set, and summability arguments for $\sum\|d_k\|^{-2}$. Zoutendijk's theorem is reusable for any descent method. Proofs of any item, and alternative arguments, are welcome.

Selected references

• J. C. Gilbert, J. Nocedal, Global convergence properties of conjugate gradient methods for optimization, INRIA Rapport de Recherche 1268, 1990. https://hal.inria.fr/inria-00075291 ; SIAM J. Optim. 2(1) (1992) 21–42, https://doi.org/10.1137/0802003
• M. Al-Baali, Descent property and global convergence of the Fletcher–Reeves method with inexact line search, IMA J. Numer. Anal. 5 (1985) 121–124. https://doi.org/10.1093/imanum/5.1.121
• R. Fletcher, C. M. Reeves, Function minimization by conjugate gradients, Comput. J. 7 (1964) 149–154. https://doi.org/10.1093/comjnl/7.2.149
• P. Wolfe, Convergence conditions for ascent methods, SIAM Rev. 11 (1969) 226–235. https://doi.org/10.1137/1011036
• D. Touati-Ahmed, C. Storey, Efficient hybrid conjugate gradient techniques, J. Optim. Theory Appl. 64 (1990) 379–397. https://doi.org/10.1007/BF00939455

Motivation

A linear program often has two objectives that pull in different directions, for example cost and risk, or two policy goals whose relative weight is a matter of judgment. Gass and Saaty (NRLQ 1955) put the question in its simplest form: let every cost coefficient be an affine function $d_j + \lambda d'_j$ of one real parameter $\lambda$, and find, for every value of $\lambda$, an optimal solution. Their paper turned this into a procedure that runs the simplex method once and then walks along the $\lambda$-axis, changing one basis column at a time. This parametric objective function method became a standard chapter of linear programming texts and is the prototype of parametric and sensitivity analysis in optimization software.

Timeline.

• 1951: Dantzig publishes the simplex method (Cowles Commission Monograph No. 13, Ch. XXI; the paper's reference [1]), with the optimality test $z_j - c_j \le 0$ for a minimization problem.
• 1954: Gass and Saaty summarize the parametric procedure (J. Oper. Res. Soc. Amer. 2 (1954), 316–319).
• 1955: the present paper gives the procedure in detail, proves the THEOREM that makes it work, and reports computations on the National Bureau of Standards SEAC computer.

Setting

For each real $\lambda$ the problem is

$$\text{minimize } \sum_{j=1}^n (d_j + \lambda d'_j)\,x_j \quad\text{subject to}\quad x_j \ge 0\ (j = 1,\dots,n),\qquad \sum_{j=1}^n a_{ij}x_j = a_{i0}\ (i = 1,\dots,m).$$

Write $A = (a_{ij})$, an $m\times n$ real matrix with columns $A_1,\dots,A_n$, and $b = (a_{i0})$. A basis is a list of $m$ linearly independent columns $A_{B(1)},\dots,A_{B(m)}$; its basic solution $x$ has $x_j = 0$ off the basis and $Ax = b$, and it is a basic feasible solution when also $x \ge 0$. Every column has coordinates $y_{ij}$ in the basis, $A_j = \sum_i y_{ij}A_{B(i)}$. For a cost vector $c$ the simplex method uses $z_j = \sum_i y_{ij}c_{B(i)}$; for the cost $c = d + \lambda d'$ the number $z_j - c_j$ is affine in $\lambda$:

$$z_j - c_j = \alpha_j + \lambda\beta_j .$$

The basis is optimal at $\lambda$ when $\alpha_j + \lambda\beta_j \le 0$ for all $j$ (inequalities (3)). The critical values of the basis are

$$\underline\lambda = \max_{\beta_j<0}\Big(-\frac{\alpha_j}{\beta_j}\Big)\ (-\infty \text{ if all }\beta_j\ge 0),\qquad \bar\lambda = \min_{\beta_j>0}\Big(-\frac{\alpha_j}{\beta_j}\Big)\ (+\infty \text{ if all }\beta_j\le 0).$$

The paper assumes throughout that the problem is nondegenerate: no basic feasible solution has more than $n - m$ zero components.

Case A is the situation where the current basis is optimal for some $\lambda$, so that (3) is consistent. If $\bar\lambda$ is finite, attained at an index $s$ with $\beta_s > 0$, and some $y_{is} > 0$, the method brings $A_s$ into the basis and removes the column $A_r$, $r = B(\ell)$, chosen by the simplex ratio test; $y_{rs} > 0$. Call the new basis $B'$ and its basic feasible solution $x'$.

Formalization targets

Goal: the THEOREM (p. 41)

$$\bar\lambda = \min\big\{\lambda\in\mathbb R : x' \text{ minimizes } (d+\lambda d')^{\top}x \text{ over } Ax = b,\ x \ge 0\big\}.$$

This contains both sentences of the paper's THEOREM: the new basis yields a minimum for at least one $\lambda$ (namely $\bar\lambda$), and the left end $\underline\lambda'$ of its interval of optimality equals $\bar\lambda$. The statement uses "least element" and so does not presuppose that the set is an interval.

Milestones

1. (3): under nondegeneracy, a basic feasible solution is a minimum at $\lambda$ if and only if $\alpha_j + \lambda\beta_j \le 0$ for all $j$.
2. (4)–(5): if (3) is consistent, it holds exactly for $\underline\lambda \le \lambda \le \bar\lambda$.
3. The reduced-cost optimality criterion and its nondegenerate converse, and feasibility of the basis after a simplex pivot (both already proved on the platform).
4. [1]: $\bar\lambda$ satisfies the inequalities (3') $\alpha'_j + \lambda\beta'_j \le 0$ of the new basis.
5. (7): $\alpha'_r = -\alpha_s/y_{rs}$ and $\beta'_r = -\beta_s/y_{rs}$.
6. (7)–(8): no $\lambda < \bar\lambda$ satisfies (3').
7. Case A stop: in the nondegenerate Case A setup, if every $y_{is} \le 0$, there is no minimum for any $\lambda > \bar\lambda$.
8. Summary (4): under the section's standing assumptions, the set of $\lambda$ for which a minimum exists is closed and connected.

Significance

The THEOREM is what makes the parametric procedure correct. The optimality intervals of successive bases meet end to end: the basis entered at $\bar\lambda$ takes over exactly where the old one stops, with no gap and no overlap. Together with the stopping rule this gives the paper's summary: starting from one optimal basis, the procedure produces a finite list of bases and characteristic values covering every $\lambda$ for which the problem has a minimum, and that set is a closed interval. The same structure underlies the piecewise linear, concave optimal value as a function of $\lambda$, the parametric right-hand-side method by duality, and the shadow-vertex simplex method.

The result is classical and its proof is short, but as printed it contains a sign slip: display (8) on p. 41 states the inequality in the wrong direction, so the contradiction the authors claim does not follow from what they wrote. The formal development states the corrected argument. To our knowledge none of these parametric statements has a machine-checked proof; the fixed-cost facts they rest on (the reduced-cost optimality criterion, Bertsimas–Tsitsiklis Theorem 3.1, and the feasibility of the pivoted basis, Theorem 3.2) are already proved on the platform in Shuze Chen's LinearOptimization library and are reused here as reference items.

Difficulty

The natural first idea is to observe that $\bar\lambda$ satisfies (3') and conclude. This proves only that the new basis is optimal at $\bar\lambda$. The statement that nothing below $\bar\lambda$ works is a statement about optimality, not about the inequalities (3'): one must know that failure of (3') at $\lambda$ means that $x'$ is not optimal at $\lambda$. That converse of the optimality test is false for a degenerate basic solution, which can be optimal while some $z_j - c_j$ is positive. The nondegeneracy assumption is therefore essential, and it must be transported to the new basic solution. The other ingredient is the pivot update of $z_j - c_j$ when one column leaves and another enters, which the paper uses through (7) without writing it down.

Formalization scope

The problem data are A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ and cost vectors d d' : Fin n → ℝ; the parameter $\lambda$ is the Lean variable t (λ is a Lean keyword). Indices are 0-based. Feasible set, optimality, bases, reduced costs, basic directions, the coordinates $y_{ij}$ (pivotColumn) and basic feasible solutions (IsSimplexState) are the published LinearOptimization definitions. The commitments and readings of the paper's phrases are:

• Sign. The platform's reduced cost is $\bar c_j = c_j - c_B'B^{-1}A_j = -(z_j - c_j)$; $\alpha_j$ and $\beta_j$ are defined as the negatives of the reduced costs for $d$ and $d'$, and (3), (3'), (5), (7) are stated in the paper's sign.
• "Yields a minimum" means that the point is feasible and its cost is at most that of every feasible point (IsLpOptimal), never a comparison of values.
• $\bar\lambda$ is finite in the THEOREM; it is the real number $-\alpha_s/\beta_s$ for an index $s$ with $\beta_s > 0$ attaining the minimum. As a function, (5) is valued in WithTop ℝ and WithBot ℝ; no real infimum of a possibly empty set is used.
• Nondegeneracy is stated for every basic feasible solution, including in the Case A stopping rule and Summary (4). The stopping rule also carries Case A consistency, and Summary (4) carries the section's available basic feasible solution. Linear independence of the rows of $A$ is assumed where the platform's criteria need it; it follows from the existence of a basis.
• "By the simplex method" is the reduced-cost optimality criterion; "the simplex prescription" is the ratio test; "no minimum" in the stopping rule is the unbounded outcome, optimal value $-\infty$, with the absence of a minimizer stated explicitly.
• The paper's interval $\delta \le \lambda \le \phi$ of interest plays no role in the THEOREM and is dropped.

The goal is not satisfied by a degenerate reading: its set is defined by optimality, not by the inequalities (3'), and its hypotheses hold on an explicit instance, so the statement is neither the definition of the critical value restated nor vacuous.

Not formalized: Case B (the search for a first $\lambda$ with a minimum), Summary (1)–(2) on the whole procedure, the no-repetition remark, the computing experience (§3) and the worked example (§4). Contributions welcome include the pivot-update formula for reduced costs, which is reusable for any simplex-based argument, and the closedness of the set of cost vectors with a finite optimum.

Selected references

• S. Gass and T. Saaty, The computational algorithm for the parametric objective function, Naval Research Logistics Quarterly 2 (1955), 39–45. https://doi.org/10.1002/nav.3800020106
• T. Saaty and S. Gass, The parametric objective function, Journal of the Operations Research Society of America 2 (1954), 316–319. https://doi.org/10.1287/opre.2.3.316
• G. B. Dantzig, Maximization of a linear function of variables subject to linear inequalities, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, Ch. XXI (Cowles Commission Monograph No. 13).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.1–3.2 and §5.2.

Motivation

A Markov decision problem with the average reward criterion asks for a policy that maximises the long-run reward per period of a controlled finite Markov chain. It is the standard model for repeated operational decisions with no natural horizon: inventory replenishment, machine maintenance, queue admission and routing. For finitely many states and actions, Howard (1960) and Blackwell (1962) showed that a pure stationary average optimal policy exists, and policy iteration finds one.

Linear programming formulations are older for the discounted problem (d'Epenoux, 1960) and for chains with a single recurrent class (Manne, 1960). Without a structural assumption, a stationary policy can split the state space into several recurrent classes, the multichain case, and the gain becomes a vector rather than a number. Denardo and Fox (1968) gave a linear programming approach for this case. Hordijk and Kallenberg (1979) showed that a single pair of dual linear programs suffices: an optimal policy can be read off an extreme optimal solution of the dual program. Kallenberg's tract (1983, Chapter 4) is the systematic account of this theory, and this mission formalizes its §4.2–4.4.

Setting

Let $E$ be a finite set of states. Each state $i$ has a nonempty finite set $A(i)$ of actions, a reward $r_{ia}\in\mathbb R$ for each action, and transition probabilities $p_{iaj}\ge 0$ with $\sum_j p_{iaj}=1$. A policy $R$ chooses, at each epoch $t=1,2,\dots$, a probability distribution on $A(X_t)$ that may depend on the whole history. A stationary policy $\pi^\infty$ uses fixed weights $\pi_{ia}$ at every epoch. A pure stationary policy $f^\infty$ always plays $f(i)\in A(i)$. Write $P(\pi)_{ij}=\sum_a p_{iaj}\pi_{ia}$, $r(\pi)_i=\sum_a r_{ia}\pi_{ia}$, and $P(f)$, $r(f)$ in the pure case.

The average reward of $R$ from state $i$ is

$$\phi_i(R)=\liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a\mathbb P_R(X_t=j,\ Y_t=a\mid X_1=i)\,r_{ja},$$

and $\hat\phi_i(R)$ is the same expression with $\limsup$. The AMD-value-vector is $\phi_i=\sup_R\phi_i(R)$, where $R$ ranges over all policies, and $R^*$ is average optimal if $\phi(R^*)=\phi$. A policy is Blackwell optimal if it maximises the discounted reward $v^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\mathbb E_R[r_{X_tY_t}]$ for all discount factors $\alpha$ in some interval $[\alpha_0,1)$.

For a stochastic matrix $P$, the stationary matrix $P^*$ is the Cesàro limit of $P^n$, and the deviation matrix is $D=(I-P+P^*)^{-1}-P^*$. For a pure policy, $\phi(f^\infty)=P^*(f)r(f)$ and $u(f^\infty)=D(f)r(f)$.

A vector $\tilde\phi$ is AMD-superharmonic if some $\tilde u$ satisfies $\tilde\phi_i\ge\sum_jp_{iaj}\tilde\phi_j$ and $\tilde\phi_i+\tilde u_i\ge r_{ia}+\sum_jp_{iaj}\tilde u_j$ for all $a\in A(i)$, $i\in E$. For weights $\beta_j>0$ with $\sum_j\beta_j=1$, the primal program (4.2.10) minimises $\sum_j\beta_j\tilde\phi_j$ over such pairs. Its dual is

$$\max\Big\{\sum_{i,a}r_{ia}x_{ia}\ \Big|\ \sum_{i,a}(\delta_{ij}-p_{iaj})x_{ia}=0,\ \ \sum_ax_{ja}+\sum_{i,a}(\delta_{ij}-p_{iaj})y_{ia}=\beta_j\ \ (j\in E),\ \ x,y\ge0\Big\}.\tag{4.2.11}$$

Write $E_x=\{i\mid\sum_ax_{ia}>0\}$.

Formalization targets

Goal: Theorem 4.2.4

If $(x^*,y^*)$ is an optimal solution of (4.2.11) and an extreme point of its feasible set, then a decision rule $f_*$ with

$$x^*_{if_*(i)}>0\ \ (i\in E_{x^*}),\qquad y^*_{if_*(i)}>0\ \ (i\in E\setminus E_{x^*})$$

exists, and every such $f_*^\infty$ is average optimal.

The goal is stated for every finite model, with no assumption on the chain structure, and for every rule-conforming $f_*$.

Milestones

1. Optimality equations (Theorem 4.2.1): a Blackwell optimal pure policy gives $(\phi^\circ,u^\circ)$ with $\phi^\circ_i=\max_{a\in A(i)}\sum_jp_{iaj}\phi^\circ_j$ and $\phi^\circ_i+u^\circ_i=\max_{a\in\bar A(i)}\{r_{ia}+\sum_jp_{iaj}u^\circ_j\}$.
2. Superharmonic characterisation (Theorem 4.2.2): $\phi$ is the smallest AMD-superharmonic vector.
3. Lim sup optimality (Theorem 4.2.3): a pure stationary average optimal $f^\infty$ satisfies $\hat\phi(f^\infty)\ge\hat\phi(R)$ for every $R$.
4. The three propositions inside the proof of Theorem 4.2.4: complementary slackness along $f_*$ (4.2.1), closedness of $E_{x^*}$ under $P(f_*)$ (4.2.2), and transience of $E\setminus E_{x^*}$ under $P(f_*)$ (4.2.3).
5. The policy–solution correspondence (§4.3): the representative $(x(\pi),y(\pi))$ is feasible (Theorem 4.3.1); the map is one-to-one with inverse (4.3.1) (Theorem 4.3.2); $E_x$ is closed under, and is exactly the recurrent set of, $P(\pi(x,y))$ (Propositions 4.3.2–4.3.3); the correspondence preserves optimality (Theorem 4.3.3); pure policies map to extreme points (Theorem 4.3.4).
6. Policy evaluation (Theorem 4.4.1): the system $(I-P(f))\tilde\phi=0$, $\tilde\phi+(I-P(f))\tilde u=r(f)$, $\tilde u+(I-P(f))\tilde z=0$ is solvable, and every solution has $\tilde\phi=\phi(f^\infty)$ and $\tilde u=u(f^\infty)$.

Significance

Theorem 4.2.4 reduces the multichain average reward problem to one linear program. Combined with Theorems 4.3.3 and 4.3.4, every pure stationary average optimal policy arises from some extreme optimal solution, so enumerating extreme optimal solutions enumerates all of them (Remark 4.2.5). The same program is the starting point for the constrained average reward problems of §4.7, where a policy must also satisfy linear constraints on its state–action frequencies. Theorem 4.4.1 is the evaluation step of multichain policy iteration.

The results are proved in the tract and, earlier, in Hordijk and Kallenberg (1979). None of them is formalized in a proof assistant. The platform has machine-checked average reward results only for unichain models, where the gain is a scalar. This mission adds the multichain theory, with general history-dependent randomized policies as competitors, and also yields reusable statements about stationary and deviation matrices of finite chains.

Difficulty

Under a unichain assumption, the dual variables $x$ form a stationary distribution and the $y$-variables are unnecessary, so the obvious argument reads a policy off $x$ alone. In the multichain case the $x$-part of an optimal solution can vanish on whole sets of states, and on those states the policy must be read off $y$. The argument then has to show that these states are transient under the selected policy, which is where extremality is essential. For a non-extreme optimal solution the book passes instead to the randomized policy (4.3.1), which needs the separate argument of Theorem 4.3.3. A second obstacle is that optimality is against all history-dependent randomized policies, so the comparison of $\phi(f_*^\infty)$ with $\phi$ must pass through the superharmonic characterisation (Theorem 4.2.2), whose proof uses the existence of a Blackwell optimal policy.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP: finite state and action types, a nonempty Finset of admissible actions per state, and stochastic rows. General policies are the published AvgHRPolicy (decision rules depending on the epoch and the full history). The criteria are the published gainInf, gainSup and optGainInf; all values are real. Average optimality is the book's lim inf notion, $\phi_i(R^*)=\sup_R\phi_i(R)$ for every $i$. It is not Puterman's stronger IsAverageOptimal. The stationary and deviation matrices are the published Cesàro limitMatrix and deviationMatrix. Their existence and invertibility (Theorem 2.4.1) are never assumed as hypotheses. LP variables are indexed by admissible state–action pairs, so Set.extremePoints is the book's notion of extreme feasible solution. Recurrence is the classical finite-chain notion: every state accessible from $i$ leads back to $i$. The ergodic set of a recurrent state is the set of states accessible from it.

A formalization that assumes a unichain or ergodic model trivializes the mission (it reduces Theorem 4.2.4 to known unichain results). No statement here makes such an assumption, and the weights $\beta_j$ are strictly positive and sum to one, as in (4.2.10).

The proofs need finite Markov chain theory: the Cesàro limit, $P^*P=PP^*=P^*$, $P^*D=0$, transience versus $P^*_{\cdot j}=0$, and positivity of the stationary distribution on ergodic sets. They also need LP duality with complementary slackness and the existence of a Blackwell optimal pure policy. The last result is posed separately on the platform (Blackwell 1962, Theorem 5). LP duality is available as proved platform theorems (LinearOptimization.*), whose sign conventions must be matched. Contributions on the Markov chain layer are reusable across the whole series.

Selected references

• L. C. M. Kallenberg, Linear Programming and Finite Markovian Control Problems, Mathematical Centre Tracts 148, Mathematisch Centrum, Amsterdam, 1983. https://ir.cwi.nl/pub/13008
• A. Hordijk and L. C. M. Kallenberg, Linear programming and Markov decision chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete dynamic programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• E. V. Denardo and B. L. Fox, Multichain Markov renewal programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968.
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.

Motivation

A Markov decision chain with finitely many states and actions is the basic model of sequential decision making under uncertainty in operations research. Inventory control, maintenance, queueing control and many other problems reduce to it. Under the average reward criterion the decision maker optimizes the long-run reward per period. For the discounted criterion one linear program yields an optimal pure stationary policy (d'Epenoux 1960). For the average criterion, De Ghellinck (1960) and Manne (1960, DOI 10.1287/mnsc.6.3.259) gave linear programs for the unichain case, where every stationary policy has a single recurrent class. In a multichain model the optimal average reward may differ from state to state, and the unichain construction no longer applies.

Hordijk and Kallenberg (Management Science 25(4):352–362, 1979, DOI 10.1287/mnsc.25.4.352) proved that in the general multichain case an average optimal policy can be found by solving only one linear program. This mission formalizes that result, Theorem 7 of the paper, together with the chain of results its proof rests on.

Timeline, following the paper's introduction:

• 1960: d'Epenoux introduces linear programming for the discounted case; De Ghellinck and Manne treat the unichain average case.
• 1962: Blackwell (DOI 10.1214/aoms/1177704593) proves that some pure stationary policy is discounted-optimal for all discount factors near 1, and expands the discounted value near $\alpha = 1$.
• 1968–1970: Denardo and Fox (DOI 10.1137/0116038) and Denardo (DOI 10.1287/mnsc.16.5.281) give the first analysis of linear programs for the multichain case. Derman's 1970 monograph streamlines it: in the worst case two linear programs and one search problem must be solved. Denardo and Fox record Bruce Miller's conjecture that the policy of Theorem 7 below is optimal.
• 1979: Hordijk and Kallenberg prove the conjecture (Theorem 7), so one linear program suffices.

Setting

The state space is a finite nonempty set $E$. In state $i$ a finite nonempty set $A(i)$ of actions is available; choosing $a \in A(i)$ earns the reward $r_{ia}$ and moves the system to state $j$ with probability $p_{iaj}$ ($p_{iaj} \ge 0$, $\sum_j p_{iaj} = 1$). A policy $R$ chooses actions at times $t = 1, 2, \dots$, possibly at random and using the whole history. For a policy $R$ and an initial state $i$,

$$\varphi_i(R) = \liminf_{T\to\infty}\frac1T\sum_{t=1}^T\sum_j\sum_a \mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$$

is the average expected reward, and $\varphi_i = \sup_R \varphi_i(R)$ is the optimal one. A policy $R^*$ is average optimal if $\varphi_i(R^*) = \varphi_i$ for every $i \in E$. A decision rule $f$ picks $f(i) \in A(i)$ in every state; $f^\infty$ is the pure stationary policy that always applies $f$. Its transition matrix is $P(f) = (p_{if(i)j})$ and its reward vector $r(f) = (r_{if(i)})$. The α-discounted value $v_i^\alpha(R)=\sum_{t\ge1}\alpha^{t-1}\sum_j\sum_a\mathbf P_R(X_t=j,Y_t=a\mid X_1=i)\,r_{ja}$ enters through Theorems 1, 3, 4 and 5.

Fix weights $\beta_j > 0$ with $\sum_j \beta_j = 1$. The dual program has a variable pair $x_{ia}, y_{ia}$ for every state $i$ and every $a \in A(i)$:

$$\max \sum_i\sum_a r_{ia}x_{ia}\quad\text{s.t.}\quad \sum_i\sum_a(\delta_{ij}-p_{iaj})x_{ia}=0,\quad \sum_a x_{ja}+\sum_i\sum_a(\delta_{ij}-p_{iaj})y_{ia}=\beta_j,\quad x,y\ge0,$$

for all $j \in E$. Its linear programming dual, the primal program, minimizes $\sum_j\beta_j\tilde\varphi_j$ over superharmonic pairs $(\tilde\varphi,\tilde u)$: $\tilde\varphi_i \ge \sum_j p_{iaj}\tilde\varphi_j$ and $\tilde\varphi_i + \tilde u_i \ge r_{ia} + \sum_j p_{iaj}\tilde u_j$ for all $a \in A(i)$, $i \in E$. For a dual solution $(x, y)$ put $E_x = \{i \mid \sum_a x_{ia} > 0\}$.

Formalization targets

Goal: Theorem 7

Let $(x, y)$ be an optimal solution of the dual program that is an extreme point of its feasible set, which is what the simplex method returns. Let $f$ be any decision rule with

$$x_{if(i)} > 0 \ \ (i \in E_x), \qquad y_{if(i)} > 0 \ \ (i \notin E_x).$$

Then $f^\infty$ is average optimal: $\varphi_i(f^\infty) = \varphi_i$ for every $i \in E$, the comparison running over all policies.

Milestones

In the order the proof uses them:

1. Theorem 1 (Blackwell): some pure stationary $f_0^\infty$ is α-discounted optimal for all α near 1.
2. Theorem 2a: $\varphi(f^\infty) = P^*(f)r(f)$. The other clauses of Theorem 2 are Blackwell's Lemma 1(a), (d), referenced as published theorems.
3. Theorem 3 (Blackwell): $v_i^\alpha(f^\infty) - \varphi_i(f^\infty)/(1-\alpha) \to (D(f)r(f))_i$ as $\alpha \uparrow 1$.
4. Theorem 4 (Derman): the policy of Theorem 1 is average optimal.
5. Theorem 5: $\varphi^0 = \varphi(f_0^\infty)$ and $u^0 = D(f_0)r(f_0)$ solve the two nested optimality equations.
6. Proof of Theorem 6: $(\varphi^0, u^0 + M\varphi^0)$ is superharmonic for some $M$.
7. Theorem 6: $\varphi$ is the smallest function that admits $u$ with $(\varphi, u)$ superharmonic.
8. §3.2: $(\varphi(f_0^\infty), D(f_0)r(f_0) + M\varphi(f_0^\infty))$ is primal optimal for all large $M$.
9. Proof of Theorem 7: $\sum_a x_{ja} + \sum_a y_{ja} \ge \beta_j > 0$, so the rule always defines a policy; and every primal optimum has first component $\varphi$.
10. Propositions 1–3: $\varphi$ is $P(f)$-harmonic and the gain–bias equation holds on $E_x$; $E_x$ is closed under $P(f)$; at an extreme optimal dual solution, the states outside $E_x$ are transient under $P(f)$.

Significance

Theorem 7 turns the multichain average-reward problem into one linear program and one pass over its solution. No unichain or communicating assumption is required, and neither the second linear program nor the search step of the earlier Denardo–Fox–Derman procedure is needed. The rule is local: any action with a positive $x$-variable, otherwise any action with a positive $y$-variable, gives an optimal policy. The paper's later results (Theorem 8, the correspondence between optimal dual solutions and optimal randomized stationary policies, and Theorem 10, on extreme points) build on the same program. Companion missions of this series formalize them.

The results are proved in the paper; no machine-checked proof of any of them is known. The formalization adds a machine-checked link between linear programming duality (complementary slackness, extreme points of polyhedra) and the limit theory of finite Markov chains (Cesàro limit matrices, transient states), over the history-dependent policy class of the published average-reward model.

Difficulty

The obvious argument reads $f$ off any optimal dual solution and uses complementary slackness to obtain $\varphi = P(f)\varphi$ and $\varphi + (I - P(f))u = r(f)$. The second equation holds only on $E_x$, and outside $E_x$ nothing controls the reward of $f$. The argument closes only when $E \setminus E_x$ is transient under $P(f)$, so that the stationary distribution of $f$ ignores those states. Transience is not a consequence of optimality. It uses extremality: an ergodic set inside $E\setminus E_x$ would make the corresponding $y$-columns of the constraint matrix linearly dependent. For a general optimal solution the paper proves optimality only of a randomized stationary policy built from $(x, y)$ (its Theorem 8(b), a companion mission), not of a pure selection. The extremality hypothesis is therefore part of the statement.

Upstream of the linear program, Theorem 6 depends on Derman's theorem and Blackwell's expansion of the discounted value near $\alpha = 1$. Both compare against all history-dependent policies and need the full limit theory of $P^*$ and $D$.

Formalization scope

The model is the published MarkovDecisionProcesses.StationaryMDP (finite nonempty S, finite A, nonempty admissible sets, stochastic transitions) with history-dependent randomized policies AvgHRPolicy. $\varphi_i(R)$ is gainInf (the lim inf of the average of the first $T$ expected rewards) and $\varphi_i$ is optGainInf, a real supremum that is finite because rewards are bounded. $P^*$ and $D$ are the published limitMatrix and deviationMatrix; the identities of Theorem 2 are the published Blackwell Lemma 1(a), (d). Conventions:

• Average optimality is Hordijk and Kallenberg's $\varphi(R^*) = \varphi$, not the stronger Puterman criterion IsAverageOptimal in the published file.
• The discounted value is the limit of the $N$-epoch discounted reward, defined by the same backward recursion as totalReward. "α near enough to 1" means some $\alpha_0 \in [0,1)$ such that the property holds on $[\alpha_0, 1)$.
• Dual variables are indexed by the admissible pairs only (Pair M), so the feasible set lies in (Pair M → ℝ) × (Pair M → ℝ) and its extreme points are those of the paper's polyhedron.
• "The simplex method is used" is encoded as "$(x, y)$ is an extreme point of the feasible set" (Set.extremePoints). A goal without extremality is a different and unproved statement, and any version that quantifies over some $f$ instead of every $f$ obeying the rule is weaker than the paper's. Both are ruled out.
• "Transient" is the negation of the published IsRecurrent. Maxima over $A(i)$ and $A^0(i)$ are stated as an upper bound plus attainment, so that $A^0(i) \ne \emptyset$ is part of Theorem 5.

A complete development needs Cesàro limits of stochastic matrices, the deviation matrix, Abelian limits of discounted values, linear programming duality with complementary slackness, and the characterization of extreme points of $\{z \ge 0 : Az = b\}$ by linear independence of the active columns. The last two are reusable well beyond this mission, as is the identification of gainInf of a stationary policy with $P^*r$. Contributions to any of them, including proofs of individual milestones, are welcome.

Selected references

• A. Hordijk, L. C. M. Kallenberg, Linear Programming and Markov Decision Chains, Management Science 25(4):352–362, 1979. https://doi.org/10.1287/mnsc.25.4.352
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• E. V. Denardo, On Linear Programming in a Markov Decision Problem, Management Science 16(5):281–288, 1970. https://doi.org/10.1287/mnsc.16.5.281
• E. V. Denardo, B. L. Fox, Multichain Markov Renewal Programs, SIAM Journal on Applied Mathematics 16(3):468–487, 1968. https://doi.org/10.1137/0116038
• J. G. Kemeny, J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• C. Derman, Finite State Markovian Decision Processes, Academic Press, 1970.

Motivation

A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).

The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.

Setting

Let $m,n$ be positive integers and $(\Omega,P)$ a probability space. A fixed real $m\times n$ matrix $A$ has rows $a_i'$. Random vectors $b:\Omega\to\mathbb R^m$ and $c:\Omega\to\mathbb R^n$ give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule $x=Db$, where the real $n\times m$ matrix $D$ is chosen before $b$ is realized. Write $\mu_b=E[b]$ and $\mu_c=E[c]$. A number $z_0$ is the given aspiration value. For each row $i$, its reliability level $\alpha_i$ is strictly between $1/2$ and $1$, and $K_i=\Phi^{-1}(\alpha_i)>0$ is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.

The residual $a_i'Db-b_i$ has raw second moment $\sigma_i^2(D)=E[(a_i'Db-b_i)^2]$ and negative mean $\mu_i(D)=\mu_{b_i}-a_i'D\mu_b$. The aspiration error has raw second moment $V(D)=E[(c'Db-z_0)^2]$. These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is $\mu_c'D\mu_b$; the model records the paper's assumption that the components of $b$ and $c$ are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.

Program (38) chooses $(D,v,v_0,w_0)$ and maximizes $v_0/w_0$. Its inequalities bound the mean objective below by $z_0+v_0$, bound $w_0$ below by the root-mean-square aspiration error, and bound each nonnegative $v_i$ between the row's risk term and $\mu_i(D)$. The denominator satisfies $w_0>0$. Program (39) introduces a nonnegative scale $t$ and barred variables. It fixes $\bar w_0=1$ and maximizes the linear objective $\bar v_0$. The barred moments are calculated from $\bar D$ and $t$ by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.

Formalization targets

Convex transformed program

Let $F_{39}$ contain every point satisfying all of (39), including $t=0$. The paper's convex-programming claim becomes

$$F_{39}\text{ is convex}.$$

The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.

Equal optimal values

Let $F_{38}$ be the feasible set of (38). Provided $F_{38}$ is nonempty, the mission goal states that the normalized substitution sends each point of $F_{38}$ to a point of $F_{39}$ with the same objective, and that

$$\sup_{(D,v,v_0,w_0)\in F_{38}}\frac{v_0}{w_0} =\sup_{(\bar D,\bar v,\bar v_0,\bar w_0,t)\in F_{39}}\bar v_0.$$

The suprema may be infinite. The equality concerns the complete program (39), including $t=0$. Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.

Significance

The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at $t=0$ occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.

The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.

Difficulty

The pointwise substitution $t=1/w_0$ only reaches points of (39) with $t>0$, while (39) explicitly permits $t=0$. Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: $\bar\sigma_i^2$ is a raw second moment and $\bar\mu_i^2$ is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.

Formalization scope

Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure $P$, and Bochner integrals for the moments. Square integrability is stated for every component of $b$ and $c$ and every product $c_jb_k$; this keeps the expected squares meaningful. The paper assumes $b$ and $c$ are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile $K_i$ is imported from the published Cohen2019.Robust.PhiInvReal, with $1/2<\alpha_i<1$ excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.

The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization $\bar w_0=1$, strict $w_0>0$, and weak $t\ge0$ are separate conditions. The $t=0$ slice is included, and the main theorem assumes $F_{38}$ nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.

Selected references

• A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, pp. 18–39. DOI.
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4), 1962, pp. 181–186. DOI.
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 1962, pp. 16–24. DOI.
• J. Cohen, E. Rosenfeld, and Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML, 2019. arXiv.