Operations Research

Motivation

The data of a linear program are often not known exactly: they are measured or estimated, or they are forecasts. The robust counterpart approach, going back to Soyster (1973), asks for a solution that is feasible for every data matrix in a prescribed uncertainty set and is best among such solutions. Ben-Tal and Nemirovski's 1999 paper [1] showed that the method stays computationally tractable for a broad class of uncertainty sets, the ellipsoidal uncertainties: the robust counterpart of an uncertain LP is then a conic quadratic program (CQP), solvable by interior point methods at roughly the cost of an LP of similar size. This result is the basis of robust linear optimization as it is used today [2], [3]. It is also the reason ellipsoidal sets are the default choice in robust portfolio selection (§4 of the paper) and in many later robust models.

Timeline. Soyster (1973) treated column-wise box uncertainty, for which the counterpart is again an LP [4]. Ben-Tal and Nemirovski (1998) developed the general theory of robust convex optimization [5]. The present paper (1999) proved the ellipsoidal-to-CQP reduction for LPs (Theorem 3.1). Its proof relies on the conic duality theory of Nesterov and Nemirovski (1994) [6].

Setting

An uncertain linear program in the homogeneous form (6) is

$$\min\{c^Tx \mid Ax \ge 0,\ f^Tx = 1\},$$

where $c, f \in \mathbb R^n$ are fixed and the matrix $A \in \mathbb R^{m\times n}$ lies in an uncertainty set $\mathcal U$. A point $x$ is robust feasible if $f^Tx = 1$ and $Ax \ge 0$ for every $A \in \mathcal U$. The robust counterpart $(P_{\mathcal U})$ minimizes $c^Tx$ over the robust feasible set

$$G_{\mathcal U} = \{x \mid Ax \ge 0\ \forall A \in \mathcal U,\ f^Tx = 1\}.$$

An ellipsoid in $\mathbb R^{m\times n}$ (display (14)) is a set

$$U(\Pi, Q) = \{\Pi(u) \mid \|Qu\| \le 1\},$$

where $\Pi(u) = P^0 + \sum_{j=1}^L u_jP^j$ is affine in $u \in \mathbb R^L$, $Q$ is an $M\times L$ matrix, and $\|\cdot\|$ is the Euclidean norm. A singular $Q$ gives an ellipsoidal cylinder, which may be unbounded. An ellipsoidal uncertainty is a set

$$\mathcal U = \bigcap_{\ell=0}^k U(\Pi_\ell, Q_\ell)$$

(condition A) that is bounded (condition B) and contains a matrix $A$ with $A = \Pi_\ell(u^\ell)$ and $\|Q_\ell u^\ell\| < 1$ for every $\ell$ (condition C, a Slater condition).

Formalization targets

Goal: Theorem 3.1

For every $x \in \mathbb R^n$,

$$x \in G_{\mathcal U} \iff f^Tx = 1 \ \text{ and }\ \forall i \le m\ \ \exists\, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)} :\ (x, \lambda^{(i)}, \mu^{(i)}, \nu^{(i)}) \text{ satisfies } (\mathcal C_i).$$

Here $(\mathcal C_i)$ is an explicit system: linear equations and one linear inequality in $(x, \lambda, \mu, \nu)$, together with the second-order cone constraints $\|\mu^{(i)}_\ell\| \le \nu^{(i)}_\ell$. Its coefficients are the matrices $P^j_\ell$ and $Q_\ell$. The robust feasible set is therefore the projection of the feasible set of the conic quadratic program (CQP), which minimizes $c^Tx$ subject to $(\mathcal C_1), \dots, (\mathcal C_m)$ and $f^Tx = 1$.

Milestones, in the order of the Appendix's proof

1. $\mathcal U$ equals the image of the feasible set of the problem $(P_i[x])$ under $u \mapsto \Pi_0(u^0)$ (p. 15).
2. Claim (I): with $f^Tx = 1$, $x$ is robust feasible iff every $(P_i[x])$ has nonnegative optimal value (p. 15).
3. Claim (II): conic quadratic duality. A strictly feasible primal that is bounded below has a solvable dual with equal optimal value (p. 15).
4. Conditions B and C make every $(P_i[x])$ strictly feasible and bounded below (p. 16).

Companion results

The CQP forms (16) and (17) of the simplest cases (a single ellipsoid; constraint-wise ellipsoids), Remark 3.1 (bounded polytopes are ellipsoidal uncertainties), and the robust portfolio counterpart (22).

Significance

The result. Theorem 3.1 turns a semi-infinite constraint system (one constraint for every $A \in \mathcal U$) into finitely many conic quadratic constraints whose size is polynomial in the data. Robust LPs with ellipsoidal uncertainty, which by Remark 3.1 include polytopic uncertainty, can therefore be solved by standard conic solvers. Later robust optimization results, such as budgeted uncertainty, affinely adjustable policies and distributionally robust LPs, refine this pattern.

Formalizing it. The theorem is classical and its proof is complete, but no machine-checked proof exists. A formal proof needs a conic quadratic strong duality theorem with dual attainment (claim (II)), which Mathlib does not have in this form. That duality theorem can be reused well beyond this mission. The companion results (16), (17) and (22) are self-contained computations of a minimum of a linear function over a Euclidean ball.

Difficulty

The "if" direction is weak duality: a solution of $(\mathcal C_i)$ certifies that the $i$-th constraint holds for all of $\mathcal U$. The content is the "only if" direction. It requires dual attainment, not merely equality of optimal values, because a solution of $(\mathcal C_i)$ must exist. Dual attainment fails without a constraint qualification. Condition C must hold strictly for every ellipsoid, including $\ell = 0$, and the ellipsoids may be cylinders, so the variables $u^\ell$ can range over unbounded sets even though $\mathcal U$ is bounded. Projecting the problem onto a single parameter space is not available in general, because the maps $\Pi_\ell$ need not be injective.

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ. The indices $\ell = 0, \dots, k$ are Fin (k + 1), and the $k$ equality multipliers $\lambda_\ell$, $\ell \ge 1$, are indexed by Fin k. Every norm is Euclidean, written out as euclidNorm v = √(∑ v_j²), because Mathlib's norm on Fin M → ℝ is the sup norm, under which ellipsoids would become boxes. Condition B is a uniform bound on all matrix entries, and condition C is required for every $\ell = 0, \dots, k$. The page's words say "$\ell = 1, \dots, k$", but its display and the proof use every $\ell$. Injectivity of $\Pi_\ell$ is not assumed, and neither is §2.1's standing assumption that $\mathcal U$ is convex and closed. An ellipsoidal uncertainty is convex automatically, and closedness is not used, so both omissions generalize the statement. Three printed slips are corrected and disclosed: the sum in the equality constraint of (CQP$_d$) runs over $\ell = 0, \dots, k$; $(\mathcal C_i)$ has $\varphi^{(i)}[x]$ where the page prints $f^{(i)}[x]$; and Remark 3.1 has the factor $2/(r_i - s_i)$ where the page prints $(r_i - s_i)/2$.

The goal is not the contentless statement "some conic quadratic program has $G_{\mathcal U}$ as a projection", which holds for every closed convex set. It names the system $(\mathcal C_i)$ built from the data $P^j_\ell$, $Q_\ell$. The goal also does not mention optimal values, (CQP$_p$) or strict feasibility; those are milestones.

Contributions are welcome on the conic duality theorem (II) as a standalone result, on the finite-dimensional facts that minimize a linear function over a Euclidean ball (used in (16), (17) and (22)), and on the goal itself.

Selected references

1. A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
2. A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
3. D. Bertsimas, D. B. Brown, C. Caramanis, Theory and applications of robust optimization, SIAM Review 53(3):464–501, 2011. https://doi.org/10.1137/080734510
4. A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154
5. A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
6. Yu. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM Studies in Applied Mathematics 13, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Robust linear optimization replaces an uncertain constraint $\tilde a'x \ge b$ by the requirement that $a'x \ge b$ hold for every $a$ in an uncertainty set $\mathcal U$ (Ben-Tal and Nemirovski 1999). The method leaves open where $\mathcal U$ should come from. Risk theory answers a related question from the other side: a decision maker's attitude to an uncertain reward is described by a risk measure $\mu$, and the constraint is imposed as $\mu(\tilde a'x - b) \le 0$.

Bertsimas and Brown (2009) connect the two. When $\mu$ is coherent and $\tilde a$ is supported on finitely many observed data points $a_1, \dots, a_N$, the risk constraint is exactly a robust constraint whose uncertainty set is built from the data and the family of probability vectors generating $\mu$. For the class of distortion risk measures, the uncertainty set has an explicit polyhedral form, the $q$-permutohull of the data, and the robust constraint has a reformulation of polynomial size. This mission formalizes that chain of results, Sections 2–4.3 of the paper.

Setting

The sample space is finite, $\Omega = \{\omega_1, \dots, \omega_N\}$, and a random variable is a vector $X \in \mathbb R^N$, read as a reward; $X \ge Y$ means $X_i \ge Y_i$ for every $i$. The probability simplex is $\Delta^N = \{p \in \mathbb R^N_+ : e'p = 1\}$, and $\mathbb E_q[X] = \sum_i q_i X_i$.

A risk measure is a function $\mu : \mathbb R^N \to \mathbb R$ with $X \ge Y \Rightarrow \mu(X) \le \mu(Y)$ and $\mu(X + c) = \mu(X) - c$. It is coherent if it is moreover convex and positively homogeneous. A set $\mathcal Q \subseteq \Delta^N$ generates $\mu$ if $\mu(X) = \sup_{q \in \mathcal Q} \mathbb E_q[-X]$ for all $X$. The conditional value-at-risk under a probability vector $p$ is $\mathrm{CVaR}_\alpha(X) = \inf_{\nu \in \mathbb R}\{\nu + \frac1\alpha \mathbb E_p[(-\nu - X)^+]\}$ for $\alpha \in (0,1]$.

Two random variables are comonotone if $(X(\omega) - X(\omega'))(Y(\omega) - Y(\omega')) \ge 0$ for all $\omega, \omega'$; $\mu$ is comonotonic if it is additive on comonotone pairs, and law invariant if it takes equal values on random variables with the same distribution. A distortion risk measure is a coherent, comonotonic, law-invariant risk measure. From Section 4.2 on, $\Omega$ carries the uniform distribution $\mathbb P\{\omega_i\} = 1/N$.

The restricted simplex is $\hat\Delta^N = \{q \in \Delta^N : q_1 \ge \cdots \ge q_N\}$. For $q \in \hat\Delta^N$ put

$$\mu_q(X) = -\sum_{i=1}^N q_i x_{(i)},$$

where $x_{(1)} \le \cdots \le x_{(N)}$ are the increasing order statistics of $X$. The data are $\mathcal A = \{a_1, \dots, a_N\} \subseteq \mathbb R^n$, the uncertain vector $\tilde a$ takes the value $a_i$ at $\omega_i$, and the $q$-permutohull of $\mathcal A$ is

$$\Pi_q(\mathcal A) = \operatorname{conv}\Big\{\sum_{i=1}^N q_{\sigma(i)} a_i : \sigma \in S_N\Big\}.$$

Formalization targets

Goal: Theorem 4.3

Under the uniform distribution, for every distortion risk measure $\mu$ there is $q \in \hat\Delta^N$ with $\mu = \mu_q$, and for this $q$, all data and every $b$,

$$\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \Pi_q(\mathcal A)\} = \{x : \exists y_1, y_2 \in \mathbb R^N,\ e'y_1 + e'y_2 \ge b,\ y_{1,i} + y_{2,j} \le q_i\, a_j'x\ \forall i, j\}.$$

The vector $q$ depends on $\mu$ only; the data are quantified after it.

Milestones

1. Theorem 2.1. $\mu$ is coherent if and only if some family $\mathcal Q \subseteq \Delta^N$ generates it.
2. Theorem 3.1. For coherent $\mu$ generated by $\mathcal Q$, $\{x : \mu(\tilde a'x - b) \le 0\} = \{x : a'x \ge b\ \forall a \in \operatorname{conv}\{Aq : q \in \mathcal Q\}\}$; conversely every nonempty $\mathcal U \subseteq \operatorname{conv}(\mathcal A)$ arises from the coherent measure generated by $\{q \in \Delta^N : Aq \in \mathcal U\}$.
3. Generation of (4). $\mu_q$ is generated by the permuted vectors $q \circ \sigma$, $\sigma \in S_N$.
4. Theorem 4.1 (Schmeidler). A coherent $\mu$ is comonotonic if and only if $\mu(X) = \int (-X)\,dg$ (Choquet integral) for a monotone, normalized, submodular $g : 2^\Omega \to [0,1]$.
5. Second differences (proof of Lemma 4.1). A submodular $g$ depending only on $|A|$ has nonincreasing increments along $\emptyset \subset \{\omega_1\} \subset \{\omega_1, \omega_2\} \subset \cdots$.
6. Lemma 4.1. A risk measure is a distortion risk measure if and only if $\mu(X) = \int_{(0,1]} \mathrm{CVaR}_\alpha(X)\,\nu(d\alpha)$ for a probability measure $\nu$.
7. The CVaR display (proof of Theorem 4.2). $\mathrm{CVaR}_\alpha(X) = \sup\{\mathbb E_q[-X] : q \in \Delta^N,\ q_i \le 1/(N\alpha)\} = \mu_{q^\alpha}(X)$ with $q^\alpha \in \hat\Delta^N$.
8. Theorem 4.2. A risk measure is a distortion risk measure if and only if $\mu = \mu_q$ for some $q \in \hat\Delta^N$; every such $q$ is a convex combination of the generators $\hat q^j$ of $\mathrm{CVaR}_{j/N}$.
9. Assignment duality (proof of Theorem 4.3). $a'x \ge b$ on $\Pi_q(\mathcal A)$ if and only if the linear system in $(y_1, y_2)$ above is feasible.

A companion item states Corollary 4.3: $\Pi_{\sum_j \lambda_j \hat q^j}(\mathcal A) = \operatorname{conv}\{\sum_j \lambda_j \frac1j \sum_{i \le j} a_{\sigma_j(i)} : \sigma_j \in S_N\}$, and the class equality it yields: the uncertainty sets $\Pi_q(\mathcal A)$ of all distortion risk measures $\mu = \mu_q$ are exactly the polytopes $\mathcal U_\lambda(\mathcal A)$, $\lambda \ge 0$, $\sum_j \lambda_j = 1$.

Significance

The goal theorem identifies the uncertainty set implied by any distortion risk measure: it is a permutohull of the data, a polytope with up to $N!$ vertices that is nevertheless representable with $2N$ extra variables and $N^2$ linear constraints. Combined with Theorem 4.2, the uncertainty sets of distortion measures are exactly the mixtures of the sets of $j$-point averages of the data (Corollary 4.3), with $\mathrm{CVaR}_{j/N}$ as the generators. The later sections of the paper build on this: centrally symmetric permutohulls (Section 4.4) and the construction of a distortion risk measure from a given polyhedral uncertainty set (Section 4.5) are the subjects of the two companion missions.

The results are proved in the paper; no machine-checked version is known. The formalization adds checked statements of the finite-space representation theory of coherent and distortion risk measures, which the paper obtains partly by citing general results, and records the corrections the printed statements need.

Difficulty

The two equalities of the goal have unequal weight. The second is a statement about one polytope with up to $N!$ vertices and a linear system of size $O(N^2)$; it is finite-dimensional linear programming. The first requires the complete characterization of distortion risk measures on a finite uniform space, and that is where the obvious approach fails. The known representation of law-invariant comonotonic coherent measures as mixtures of CVaR (Kusuoka 2001) is proved for atomless spaces and does not transfer to a discrete $\Omega$. The uniform distribution is essential, not a convenience: Remark 4.2 of the paper gives a two-point space with probabilities $1/3, 2/3$ and a monotone, normalized, submodular set function depending only on probability whose induced distortion is not concave, so the conclusion of Theorem 4.2 fails there.

Formalization scope

• $\Omega$ is Fin N with $N \ge 1$; random variables are Fin N → ℝ; indices are 0-based throughout, so qhat j is the paper's $\hat q^{j+1}$ and $q_1 \ge \cdots \ge q_N$ is Antitone q. Order statistics are X ∘ Tuple.sort X.
• Probability measures on $\Omega$ are probability vectors in stdSimplex ℝ (Fin N). Generation (1) is an IsLUB over an arbitrary set of probability vectors, not a maximum over a finite family (that version is false).
• Sign of the risk constraint. Display (2) and Theorem 4.3 print $\mu(\tilde a'x - b) \ge 0$. The paper introduces the constraint as $\mu(\tilde a'x - b) \le 0$ (p. 1486) and the proof of Theorem 3.1 computes $\mu(\tilde a'x - b) = -\inf_{a \in \mathcal U} a'x + b$; all statements use $\le 0$.
• Standing assumptions. Theorems 2.1 and 3.1 assume a probability vector $p$ with $p_i > 0$ (full support makes $\mathbb Q \ll \mathbb P$ vacuous; with a null atom Theorem 2.1 fails for functions on $\Omega$). From Lemma 4.1 on the distribution is uniform (Assumption 4.1). Theorem 3.1's converse adds $\mathcal U \neq \emptyset$.
• CVaR is a real infimum, used only for $\alpha \in (0,1]$, where the objective is bounded below by $\mathbb E[-X]$. In Lemma 4.1 the mixing measure $\nu$ is a probability measure on $(0,1]$; the page's $\int_0^1$ is read over $(0,1]$. The CVaR display uses the corrected coefficient $(N\alpha - \lfloor N\alpha \rfloor)/(N\alpha)$ in place of the printed $/\lfloor N\alpha \rfloor$. The assignment-duality milestone is stated for every $q \in \mathbb R^N$.
• The goal must assert the representation $\mu = \mu_q$ together with the set equalities: a statement "there is some $q$ for which the sets coincide" would let $q$ depend on the data and is not Theorem 4.3. The goal does not assume $\mu = \mu_q$, which is Theorem 4.2's conclusion.
• Needed infrastructure: Birkhoff's theorem (in Mathlib), LP duality, the rearrangement inequality, Choquet integrals of step functions. Lemmas about $\mu_q$ and order statistics are reusable beyond this mission; proofs of any milestone are welcome.

Selected references

• D. Bertsimas, D. B. Brown, Constructing uncertainty sets for robust linear optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0646
• A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/S0167-6377(99)00016-4
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• D. Schmeidler, Integral representation without additivity, Proceedings of the AMS 97(2):255–261, 1986. https://doi.org/10.1090/S0002-9939-1986-0835875-8
• R. T. Rockafellar, S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
• S. Kusuoka, On law invariant coherent risk measures, Advances in Mathematical Economics 3:83–95, 2001. https://doi.org/10.1007/978-4-431-67891-5_4
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075

Motivation

A linear decision made with uncertain coefficients can be protected by requiring the constraint to hold for every coefficient vector in an uncertainty set. Choosing that set determines how conservative the decision is. Bertsimas and Brown connect this choice to a risk measure: a functional that assigns a cost to the random reward left by a decision. Their construction turns certain risk constraints into robust linear constraints over a convex hull of weighted samples. This mission isolates the structural question asked in §4.4 of their paper: which such risk measures always produce uncertainty sets that are centrally symmetric about the sample mean? The answer matters because this symmetric family is the class used in the paper's subsequent approximation of general polyhedral uncertainty sets. Bertsimas and Brown (2009), §§4.3–4.5.

Setting

There are $N\ge1$ observations, indexed by $i=1,\ldots,N$, with equal reference probabilities. A probability weight vector $q=(q_1,\ldots,q_N)$ has nonnegative entries summing to one. The restricted simplex $\widehat\Delta^N$ contains those vectors whose entries are nonincreasing: $q_1\ge\cdots\ge q_N$. For a reward vector $X=(x_1,\ldots,x_N)$, write $x_{(1)}\le\cdots\le x_{(N)}$ for its increasing order statistics. The associated distortion risk measure is $\mu_q(X)=-\sum_iq_i x_{(i)}$. A larger reward therefore reduces risk. Under the uniform distribution, the paper's Theorem 4.2 identifies these functionals, for $q\in\widehat\Delta^N$, with its distortion risk measures. Bertsimas and Brown (2009), Theorem 4.2.

Take arbitrary sample vectors $a_1,\ldots,a_N\in\mathbb R^n$. For a permutation $\sigma$ of their indices, form the weighted vector $\sum_iq_{\sigma(i)}a_i$. The $q$-permutohull $\Pi_q(\mathcal A)$ is the convex hull of all these vectors. Its center of interest is the sample mean $\widehat a=N^{-1}\sum_i a_i$. A set $P$ is centrally symmetric through $x_0\in P$ when $x_0+x\in P$ implies $x_0-x\in P$ for every $x$. The quantifier “for any data” ranges over every dimension $n$ and every choice of $N$ sample vectors. It is stronger than symmetry for one selected data set. Bertsimas and Brown (2009), Definitions 4.7–4.8.

Formalization targets

The first target is Proposition 4.1's characterization of weights giving universal symmetry. If $e_N$ is the vector with every entry $1/N$, then

$$\bigl[\Pi_q(\mathcal A)\text{ is centrally symmetric through }\widehat a \text{ for every }n,\mathcal A\bigr] \quad\Longleftrightarrow\quad \exists\sigma\in S_N:\ q=2e_N-q_\sigma.$$

This condition defines the symmetric restricted simplex $\widehat\Delta^N_{\mathrm{sym}}$ inside $\widehat\Delta^N$. Bertsimas and Brown (2009), Proposition 4.1 and Definition 4.9.

The main target is Theorem 4.4. Put $\widehat N=\lfloor N/2\rfloor+1$. For $1\le j\le\widehat N$, define a generator $\bar q^{\,j}$ by

$$\bar q_i^{\,j}= \begin{cases} 2/N,&i<j,\\ 1/N,&j\le i\le N-j+1,\\ 0,&\text{otherwise}. \end{cases}$$

A functional represented by a $q\in\widehat\Delta^N$ whose permutohull is symmetric for every data set is exactly a convex mixture of the $\widehat N$ generator functionals:

$$\mu(X)=\sum_{j=1}^{\widehat N}\lambda_j\mu_{\bar q^{\,j}}(X), \qquad \lambda_j\ge0,\qquad\sum_{j=1}^{\widehat N}\lambda_j=1.$$

The milestones also state the two set inclusions behind the equality of $\widehat\Delta^N_{\mathrm{sym}}$ with the convex hull of these generators, including the coordinate reversal identity. Bertsimas and Brown (2009), Theorem 4.4 and its proof.

Significance

The result gives a finite list of risk functionals from which every member of the universally symmetric distortion subclass can be formed. The number of generators is $\lfloor N/2\rfloor+1$, rather than an unspecified family. It also connects a geometric property of a robust uncertainty set to a checkable condition on its weights. The paper uses this symmetric subclass to formulate the inner approximation problem in §4.5, where a symmetric permutohull is fitted inside another polytope. Bertsimas and Brown (2009), §§4.4–4.5.

The mathematical result is proved in the 2009 paper. This formalization task is to obtain Lean proofs of the classification and its source-stated intermediate claims. The definition layer is a reusable interface for finite distortion risk measures, permutohulls, and symmetry under coordinate permutations. Formal proofs here would provide a checked foundation for later robust optimization statements using the same finite sample model. The proposed goal and milestones are open Lean statements; compiling them verifies their syntax and types, not their proofs.

Difficulty

Symmetry of one pictured polygon does not determine its weight vector. The hypothesis demands symmetry for every possible collection of sample vectors, so the converse in Proposition 4.1 must recover a relation among weights from a universal geometric property. Another difficulty is that the explicit generators change shape at the midpoint, and the odd and even cases have different middle ranges. The paper writes the calculation for odd $N$ and says the even case is analogous; the theorem itself makes no parity restriction. A proof therefore has to cover the even boundary, including the generator whose $1/N$ band is empty. Bertsimas and Brown (2009), Proposition 4.1 and proof of Theorem 4.4.

Formalization scope

The Lean sample space is Fin N, with $N>0$. Its indices start at zero; the prose and source formulas above start at one. The source's $\widehat N$ is N / 2 + 1 in natural numbers. Probability vectors use Mathlib's standard simplex together with antitone coordinate order. Permutohulls use convexHull of the finite permutation family, and order statistics use Tuple.sort. The reference distribution is uniform, as in the paper's Assumption 4.1. Real vector spaces of dimension zero are allowed because the claim quantifies over every dimension; the nonempty sample condition excludes division by zero.

The goal takes an arbitrary functional $\mu$ and requires an actual representation $\mu=\mu_q$ by a restricted-simplex weight. This is the paper's Theorem 4.2 parametrization of distortion risk measures, stated directly because that theorem is being drafted in a separate mission of the same series. Universal symmetry is derived from the data quantifier; it is not assumed as a condition on $q$. The generator mixture is likewise the conclusion, with its coefficients nonnegative and summing to one. Central symmetry includes membership of the center in the set.

Useful contributions include proofs of the source's permutation characterization, validity and symmetry of generator mixtures, and their converse spanning property. The definitions of finite probability weights and weighted permutation hulls can support further finite sample robust optimization results. The paper's inconsistent accent on the generator risk measure in Theorem 4.4 is read as the functional of the displayed generator vector; its intermediate sum on p. 1492 does not alter the stated normalized mixture.

Selected references

• Dimitris Bertsimas and David B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6), 1483–1495, 2009. DOI: 10.1287/opre.1080.0646.

Motivation

A firm holds a fixed stock of a perishable or seasonal product: airline seats, hotel rooms, fashion goods, tickets. It must sell the stock over a finite season, and whatever is left at the end is worth nothing. The firm can change its price at any time, and demand responds to the price at random. Should it adjust its price continually as sales occur and time runs out, or is one well-chosen price nearly as good?

Gallego and van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons (Management Science 40(8), 1994, doi:10.1287/mnsc.40.8.999), set up this question as a continuous-time stochastic control problem and answered it. The source for this mission is the published 1994 article. Its answer is quantitative: the expected revenue of a single fixed price is within a factor $1-1/(2\sqrt{\min\{n,\lambda^*t\}})$ of the best possible dynamic policy. The paper is one of the founding results of dynamic pricing in revenue management. The deterministic (fluid) upper bound it introduced became the standard benchmark of the field, and later work on re-solving heuristics, network revenue management and learning-while-pricing builds on it.

Setting

Demand. The firm chooses a demand intensity $\lambda$ from an interval $\Lambda\ni 0$ of allowable rates, and the market charges the inverse-demand price $p(\lambda)$. On nonzero rates, $p$ is strictly decreasing and nonnegative; rate $0$ corresponds to the null price $p_\infty$, at which nothing sells. The revenue rate is $r(\lambda)=\lambda p(\lambda)$. It has $r(0)=0$, and it is continuous, concave and bounded on $\Lambda$. $\lambda^*$ denotes its least maximizer, and $p^*=p(\lambda^*)$, $r^*=r(\lambda^*)$. Such data form a regular demand function (§2.1).

The stochastic problem. At time $0$ the firm holds $n$ items and has a horizon $[0,t]$. A non-anticipating pricing policy $u$ chooses the intensity $\lambda_s\in\Lambda$ at each elapsed time $s$ as a function of the sales history so far. Sales follow a Poisson process with this controlled intensity, and at most $n$ items can be sold. A sale at time $s$ earns the current price $p_s$. The expected revenue is $J_u(n,t)=E_u[\int_0^t p_s\,dN_s]$, where $N_s$ counts the sales, and the optimal expected revenue is $J^*(n,t)=\sup_u J_u(n,t)$.

The deterministic problem. Replacing random sales by their rates gives

$$J^D(x,t)=\sup\Big\{\int_0^t r(\lambda(s))\,ds:\ \lambda(s)\in\Lambda,\ \int_0^t\lambda(s)\,ds\le x\Big\}.$$

It is solved by the constant rate $\lambda^D=\min\{\lambda^*,x/t\}$ (Proposition 2).

Fixed-price heuristics. $J^{FP}(n,t)$ is the expected revenue of charging $p^D=p(\lambda^D)$ for the whole horizon. $J^{OFP}(n,t)$ is the expected revenue of the best constant price.

Formalization targets

Goal: Theorem 3

For $\lambda^*>0$, $n\ge1$ and $t>0$, $J^*(n,t)$ is finite and positive, and

$$\frac{J^{OFP}(n,t)}{J^*(n,t)}\ \ge\ \frac{J^{FP}(n,t)}{J^*(n,t)}\ \ge\ 1-\frac{1}{2\sqrt{\min\{n,\lambda^*t\}}}.$$

Milestones

1. Proposition 2: $\lambda^D$ solves (11), and $J^D(x,t)=t\,r(\lambda^D)$.
2. Eqs. (13)–(14): $E_u[N_t]=E_u[\int_0^t\lambda_s ds]\le n$ and $J_u(n,t)=E_u[\int_0^t r(\lambda_s)ds]$ for every policy.
3. Eq. (15) and Lemma 1: $J_u(n,t)\le J_u(n,t,\mu)\le J^D(n,t,\mu)$ for all $\mu\ge0$.
4. The zero duality gap: $J^D(n,t)=\min_{\mu\ge0}J^D(n,t,\mu)$.
5. Theorem 2: $J^*(n,t)\le J^D(n,t)$ for all $n\ge 0$, $t\ge0$.
6. Eq. (17): a fixed price $p$ earns $p\,E[\min\{n,N_{\lambda(p)t}\}]$, with $N$ Poisson.
7. Inequality (18), Gallego's bound $E[(N-n)^+]\le(\sqrt{\sigma^2+(n-\mu)^2}-(n-\mu))/2$, already on the platform.
8. The two case bounds of the proof of Theorem 3, including (19), and the exact fixed-price revenue of the Remark.

Significance

The result. Theorem 2 says that uncertainty can only cost revenue. The deterministic value is a computable upper bound for every policy, so any heuristic can be judged against it. Theorem 3 turns this into a guarantee: with 400 items and scarce stock, a single price earns at least 97.5% of the optimum. The loss vanishes as the expected sales volume grows. This is the justification for the stable, rarely changed prices seen in practice, and the template for the asymptotic-optimality analyses that followed: fluid bounds, re-solving, bid prices.

Formalizing it. The results are proved on paper, and none is formalized. The platform has a discrete-time Bernoulli analogue of Theorem 2 (Talluri–van Ryzin, RevenueManagement.deterministic_upper_bound) and Bitran–Caldentey's periodic-review version as open items. Neither is this continuous-time model. A formalization would add a controlled Poisson sales process with a policy-dependent intensity, the compensator identities (13)–(14) for it, and a Lagrangian-duality argument over measurable rate paths. These are reusable for every continuous-time revenue-management model on the platform. Gallego's moment bound (18) is already proved there.

Difficulty

The deterministic side (Proposition 2, the duality gap) is convex analysis on one concave function. The fixed-price bounds reduce to a Poisson computation and (18). The obstacle is Theorem 2's stochastic step. The revenue is collected at random jump times chosen by an adaptive policy, and comparing it with a deterministic integral requires the compensator identity $E_u[\int p_s\,dN_s]=E_u[\int r(\lambda_s)\,ds]$ for an arbitrary non-anticipating intensity. The paper cites Brémaud's martingale theory for this, which Mathlib does not have. A first idea is to apply Jensen's inequality to $J_u$ directly. It fails because the stock constraint holds only pathwise, through $N_t\le n$, and not in expectation for a rate path. Restricting to Markovian policies does not remove the need for the identity.

Formalization scope

• Model. Rates are real numbers, and $\Lambda\subseteq[0,\infty)$ is an interval containing $0$. $p$ is a real function, strictly decreasing and nonnegative on $\Lambda\setminus\{0\}$. $r(\lambda)=\lambda p(\lambda)$ is continuous, concave and bounded above on $\Lambda$, and $\lambda^*$ is its least maximizer. $p(0)$ is never used, since the null price may be $+\infty$.
• Policies depend on elapsed time and the past sale times (the internal history); randomized policies are not included. Intensities are jointly measurable and locally integrable.
• The sales process is built from i.i.d. $\mathrm{Exp}(1)$ clocks, one per item. A sale occurs when the intensity integrated since the last sale reaches the next clock, so at most $n$ items are sold. Constraint (2) is part of the construction, not a hypothesis.
• Values. Expected revenues and $J^*$ are in $[0,\infty]$, as lower Lebesgue integrals and suprema. $J^D$ is a real supremum over measurable, integrable rate paths, nonempty and bounded for $x,t\ge0$. $J^{FP}$ and $J^{OFP}$ are expected revenues of constant-price policies of this process, and the goal also asserts $0<J^*<\infty$. Defining $J_u$ by the right side of (14), $J^*$ by the HJB equation, or $J^{FP}$ by formula (17) would trivialize the mission, and is ruled out.
• Added hypotheses. Theorem 3 assumes $n\ge1$, $t>0$ and $\lambda^*>0$, which the page leaves implicit: the ratios divide by $J^*$, which vanishes otherwise. Eqs. (13)–(14) are stated for every policy, without Proposition 1's bound $\lambda_s\le\lambda^*$, and without the reduction to Markovian policies.
• Corrected slips. (12) prints $J^D(x,t)=t\min\{r^*,r^0\}$, which is false for $x>\lambda^*t$ (exponential demand with $x=at$ gives $r^0=0$). The statement uses $t\,r(\lambda^D)$, and the printed form where $x\le\lambda^*t$. The Remark's "$E(N_n-n)^+=n(1-P\{N_n=n\})$" should read $E[\min\{N_n,n\}]$; its displayed $J^{FP}$ formula is right. Proposition 2's "the optimal solution" is stated as optimality, since uniqueness fails without strict concavity.
• Welcome contributions. Infrastructure for counting processes with stochastic intensity (the clock construction, the compensator identity), Jensen and Lagrangian duality for concave integral functionals on rate paths, and Poisson truncated-mean computations.

Selected references

• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, A Minmax Distribution Free Procedure for the (Q, R) Inventory Model, Operations Research Letters 11:55–60, 1992 (cited in the paper's references, p. 1019).
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer-Verlag, New York, 1980 (as cited in the paper).
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004 (Chapter 5; on the platform as RevenueManagement.*).
• G. Bitran, R. Caldentey, An Overview of Pricing Models for Revenue Management, Manufacturing & Service Operations Management 5(3):203–229, 2003 (on the platform as PricingRM.DetHeuristic.*).

Motivation

A controller often cannot see the state of the system it steers. It sees only measurements that are noisy functions of that state. In operations research this happens in machine maintenance and inspection, in queues observed only partially, and in inventory systems with inexact stock records. In control engineering it is the usual case. The question is what the controller should base its decisions on. The full record of past measurements is the obvious choice, but that record grows with time, so a law that uses it is a function on a space whose dimension grows with the horizon.

K. J. Åström's 1965 paper Optimal Control of Markov Processes with Incomplete State Information answered this question for finite Markov chains. The answer is that the conditional distribution of the hidden state given the measurements is a sufficient statistic. The problem with incomplete information is equivalent to a problem with complete information whose state is that distribution. This is the model now called a partially observable Markov decision process (POMDP), and the conditional distribution is now called the belief state.

Timeline. For linear systems with quadratic cost and Gaussian noise, the separation theorem of Joseph and Tou (1961) and Gunckel and Franklin (1963) says that the optimal control is a fixed function of the conditional mean of the state. Åström (1965) proved the reduction for finite-state Markov chains with arbitrary costs, with the conditional distribution as the new state. Smallwood and Sondik (1973) showed that for finite horizons the value function is piecewise linear and concave in the belief, which made exact computation possible. Bertsekas and Shreve (1978) and Bäuerle and Rieder (2011) gave the reduction for general Borel models.

Setting

The hidden state $x_t$, $t = 1, \dots, N$, takes values in a finite set $S$. The controls $u = (u_1, \dots, u_r)$ range over a compact nonempty set $U \subset \mathbb R^r$. The state moves by the transition probabilities $p_{ij}(u, t) = P\{x_t = j \mid x_{t-1} = i\}$, which are continuous in $u$. The state is observed through outputs $y_t$ in a finite set $Y$, with $q_{ij} = P\{y_t = j \mid x_t = i\}$, conditionally independent given the states. The law of $x_1$ is $p^1$. An instantaneous cost $g(u, i, t)$, continuous in $u$, is paid at each time.

A control law chooses $u(t) = c(\eta_1, \dots, \eta_t, t) \in U$ from the outputs observed so far, $\eta(t) = (\eta_1, \dots, \eta_t)$. With $u(t)$ moving $x_t$ to $x_{t+1}$, a law determines the joint law of $(x_1, \dots, x_N, y_1, \dots, y_N)$ and the expected cost

$$EL = E \sum_{t=1}^N g(u(t), x_t, t). \tag{2.6}$$

Problem P.1 is to find an admissible law minimizing (2.6).

The conditional state distribution is $w_i(t) = P\{x_t = i \mid \eta(t)\}$. It is updated by Bayes' rule: with $z^j(u, w)_i = \sum_s q_{ij}\, p_{si}(u, t+1)\, w_s$ and $\|z\| = \sum_i |z_i|$, the output $\eta_{t+1} = j$ gives $w(t+1) = z^j(u(t), w(t)) / \|z^j(u(t), w(t))\|$, and $\|z^j\|$ is the probability of that output. The cost-to-go $V_k(w)$ is the minimal expected cost of the steps $k, \dots, N$ when $x_k$ has distribution $w$, with $V_{N+1} = 0$. Problem P.2 controls the process $w(t)$ directly: a law chooses $u(t)$ from $w(1), \dots, w(t)$ to minimize $E\sum_{t=1}^N \sum_i g(u(t), i, t)\, w_i(t)$.

Formalization targets

Goal: Theorem 3

P.1 has a solution if and only if P.2 has one. For every solution $(V, c^0)$ of the functional equation

$$V_k(w) = \min_{u \in U} \Big\{ \sum_i g(u, i, k)\, w_i + \sum_j V_{k+1}\Big(\frac{z^j(u, w)}{\|z^j(u, w)\|}\Big) \|z^j(u, w)\| \Big\}, \qquad V_{N+1} = 0, \tag{3.28}$$

with $c^0(w, k)$ attaining the minimum, the law

$$u(t) = c^0(w(t), t)$$

is optimal for P.1 and for P.2, among all admissible laws of each, and both minimal values equal $E_{\eta_1} V_1(w(1))$.

Milestones

1. (3.20)–(3.25): the conditional distributions obey the Bayes recursion, and $\|z^j\| = P[y_{t+1} = j \mid \eta(t)]$.
2. Theorem 1: the cost-to-go satisfies (3.28) with the minimum attained, and an optimal Markov law attains it.
3. Theorem 2: a solution of (3.28) gives an optimal law for P.1 with value (3.29).
4. Lemma 1: under $u(t) = c(w(t), t)$, $\{w(t)\}$ is a Markov process with transition probabilities $P(y, \Gamma, u) = \sum_{k \in K} \|z^k(u, y)\|$.
5. Proof of Theorem 3: the integral against this kernel is the sum in (3.28).

Significance

The result. Theorem 3 replaces a minimization over functions of ever longer measurement records with a recursion over a fixed space, the probability simplex over the states. Every exact and approximate POMDP algorithm starts from it: value iteration on beliefs, the piecewise-linear representation of Smallwood and Sondik, point-based methods. It also splits the controller in two. A filter computes $w(t)$ in real time, and the function $c^0$ can be computed off-line. This is the decomposition the paper draws on p. 189, and it extends the linear-quadratic separation theorem to arbitrary finite chains.

Formalizing it. The theorem is proved. The platform has the reduction in Bäuerle and Rieder's discounted Borel model with an observable state component and rewards in extended reals. It does not have Åström's model: finite chains, time-dependent transition matrices, an unobservable state, costs, and laws of the raw output history. This mission formalizes Åström's statements as he gives them. The cost (2.6) is defined from the joint law of states and outputs, and the comparison classes are all laws of the outputs (P.1) and all laws of the distribution history (P.2). The finite setting makes every expectation a finite sum, so a complete development needs no measure theory.

Difficulty

The obvious argument is backward induction on the conditional distributions. The difficulty is that $w(t)$ depends on the controls already used, so it is not given in advance: the state of the reduced problem is produced by the law being optimized. It has to be shown that the expected cost of an arbitrary law of the outputs, computed from the joint law, splits as the reduced recursion says. In particular, laws that use more of the record than $w(t)$ must gain nothing. Restricting the comparison class to laws of the form $c(w(t), t)$ assumes this conclusion.

A second difficulty is attainment. "Min" in (3.28) and "has a solution" presuppose that minima over $U$ are attained, which needs continuity of $V_{k+1}$ on the simplex. The weights $\|z^j(u, w)\|$ can vanish, and then the update $z^j/\|z^j\|$ is undefined.

Formalization scope

States and outputs are finite types, St and Obs, with the chain given by the structure Model. Controls are Fin r → ℝ, and $U$ is compact and nonempty. The law $p^1$ of $x_1$ is the datum in place of the paper's law of $x_0$, since no control $u(0)$ exists. The transition from $x_t$ to $x_{t+1}$ uses $u(t)$ and the matrix $p(u(t), t+1)$. Times $1, \dots, N$ are indexed by Fin N as $0, \dots, N-1$.

The norm $\|\cdot\|$ is the $\ell^1$ norm l1, not Mathlib's sup norm. Conditional distributions are ratios of path sums, condState, and are claimed only on output histories of positive probability. When $\|z^j\| = 0$ the update is the zero vector and is always multiplied by $0$.

The cost-to-go costToGo is an infimum over admissible tail laws. Its index set is nonempty and the costs are bounded below, so the real infimum is a true infimum. It is never defined through (3.28), since that would make Theorem 1 circular. The P.2 functional sums branch by branch over the outputs, with weights $\|z^j\|$. "Given by Theorem 1" is read as "$c^0(w, k) \in U$ attains the minimum in (3.28)" (IsSolution328).

The goal is not the bare equivalence of solvability. In this compact, continuous, finite setting both problems always have solutions, so that sentence alone is trivially true. The goal also requires the law $c^0(w(t), t)$ to be optimal in both problems, against every admissible law, with equal minimal values.

Reusable beyond this mission are the finite POMDP model, the joint path law, the Bayes filter and the belief-MDP kernel. Welcome contributions include proofs of the milestones, the continuity of $V_k$ on the simplex, and existence of solutions of (3.28).

Selected references

• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10(1):174–205, 1965. https://doi.org/10.1016/0022-247X(65)90154-X
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5):1071–1088, 1973. https://doi.org/10.1287/opre.21.5.1071
• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9
• P. D. Joseph and J. T. Tou, On linear control theory, Transactions of the AIEE, Part II 80(4):193–196, 1961. https://doi.org/10.1109/TAI.1961.6371743

Why this problem arose

Dynamic programming often replaces a search over whole plans with an equation for a value function. That replacement is useful only when solving the equation recovers the value actually available through policies. In his 1967 paper, Eric Denardo isolated conditions on an abstract return function that make this identification possible, without committing to a particular transition law or a finite state space. The framework covers discounted decision models and other examples discussed in the paper, while allowing different decisions at different states. Denardo, 1967.

The mission concerns the paper's first regime: a one-step contraction together with monotonicity. It focuses on the question raised just after equation (4): does the solution of the functional equation equal the supremum of the return functions generated by policies? The paper proves that it does under these assumptions. Its later $N$-stage regime is a separate mission. Denardo, 1967, pp. 167–169.

States, decisions, and returns

Let $\Omega$ be a set of states. At each $x\in\Omega$ there is a decision set $D_x$. A policy $\delta$ selects a decision $\delta_x\in D_x$ at every state, so the policy space $\Delta$ is the full Cartesian product $\prod_{x\in\Omega}D_x$. Let $V$ be the bounded real functions on $\Omega$, with the uniform metric $\rho(u,v)=\sup_{x\in\Omega}|u(x)-v(x)|$. A return function $h(x,d,v)$ assigns a real return to a state, an available decision, and a continuation value $v\in V$. Denardo, 1967, p. 166.

For a policy $\delta$, its policy operator $H_\delta$ acts by $(H_\delta v)(x)=h(x,\delta_x,v)$. Under the contraction assumption, some $c$ satisfies $0\le c<1$ and $|h(x,d,u)-h(x,d,v)|\le c\rho(u,v)$ for all eligible $x,d,u,v$. Each $H_\delta$ then has a unique fixed point $v_\delta\in V$, called that policy's return function. The optimal return function is defined pointwise by $f(x)=\sup_{\delta\in\Delta}v_\delta(x)$. These are the paper's definitions, rather than a presumed equality between $f$ and a Bellman fixed point. Denardo, 1967, pp. 166–167.

The maximization operator $A$ instead chooses the best decision at each state for a supplied continuation value: $(Av)(x)=\sup_{d\in D_x}h(x,d,v)$. Denardo assumes that $H_\delta v$ and $Av$ remain bounded, so both operators act on $V$. The monotonicity assumption says that $u\ge v$ pointwise implies $H_\delta u\ge H_\delta v$ for every policy. These are separate conditions: contraction controls distance between value functions, while monotonicity controls their order. Denardo, 1967, pp. 166–168.

Formalization targets

The central target is Theorem 3. Under contraction and monotonicity, the unique bounded solution $v^*$ of equation (4) is the optimal return:

$$Av^*=v^*,\qquad v^*(x)=f(x)=\sup_{\delta\in\Delta}v_\delta(x)\quad(x\in\Omega).$$

The milestones follow the paper's route to that assertion. Theorem 1 bounds a policy's return by its fixed-point residual, $\rho(v_\delta,w)\le\rho(H_\delta w,w)/(1-c)$. Theorem 2 says that $A$ itself has modulus at most $c$. The text accompanying equation (4) establishes that $A$ has exactly one fixed point. Corollary 1 then gives, for each $\varepsilon>0$, a policy with residual at most $\varepsilon(1-c)$ at that fixed point and return within $\varepsilon$ of it, together with an exact equality criterion for zero residual. Denardo, 1967, pp. 167–168.

What the result gives

Theorem 3 justifies reading the functional equation as an optimization equation: its solution is the pointwise supremum of returns realized by the paper's policy model. Corollary 1 supplies policy returns arbitrarily close to that solution in the uniform metric. With the compactness and continuity assumptions of Corollary 2, the paper also obtains a policy that attains it, though that optional result is outside this mission's milestone list. Denardo, 1967, pp. 167–168.

The mathematical result was proved in the cited paper. This mission asks for machine-checked proofs of its abstract statements in Lean, including the residual estimate, the maximization operator's contraction, fixed-point existence, and the identification with optimal policy return. The definitions are reusable for decision models whose returns fit Denardo's assumptions; they do not prescribe a probability kernel or a finite action set.

Where the difficulty lies

The fixed-point theorem alone identifies a unique solution of $Av=v$; it does not identify that solution with $f$, because $f$ is defined through the separate fixed points of all $H_\delta$. The distinction matters: the paper observes that contraction without monotonicity can leave $v^*$ different from $f$, and gives $h(x,d,v)=-v(x)/2$ as a nonmonotone example. The formal goal therefore retains both definitions and requires monotonicity. Denardo, 1967, pp. 167–168.

There is also a choice issue in Corollary 1. A near-maximizing decision is available separately at every state, while its conclusion asks for one policy choosing all those decisions at once. The full Cartesian policy space is essential to the statement. On an infinite state set, the value functions must remain bounded even after applying $A$ or a policy operator; contraction of differences by itself does not provide that range condition. Denardo, 1967, pp. 166–168.

Formalization scope

Lean represents $V$ by bounded real functions lp (fun _ : Ω => ℝ) ⊤; its metric is $\rho$. The state type may be infinite or empty, and decision sets depend on the state. Policies are precisely dependent functions $\delta:(x:\Omega)\to D_x$. The operators $H_\delta$ and $A$ are maps into $V$ supplied with equations fixing their values from $h$. This expresses the bounded-range assumptions on pages 166–167. Pointwise order is explicit because the bounded-function type has no order instance. Denardo, 1967, pp. 166–168.

Every supremum in the mission is a genuine real least upper bound. IsMaxOperator requires it for the decision returns at each state; IsOptimalReturn requires it for the policy returns. These predicates avoid assigning a default value to an empty or unbounded supremum. Where states exist, IsMaxOperator also entails a nonempty decision set. The family $v_\delta$ is supplied with $H_\delta v_\delta=v_\delta$; contraction ensures each such return exists uniquely. Equation (4) and the main goal explicitly assert existence of the fixed point of $A$, so the goal cannot hold merely because there is no solution to identify. Defining $f$ from the fixed point of $A$, or defining $v^*$ from the policy supremum, would erase the paper's substantive claim and is excluded.

The definition layer needs bounded functions, uniform distance, real least upper bounds, and dependent policies. The theorem layer needs fixed-point and order reasoning on these objects. Contributions toward those general operator facts and the paper's four milestone statements are within scope.

Selected references

• Eric V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2), 165–177, 1967. DOI: 10.1137/1009030.