Dynamic Programming

Motivation

Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return $f$ solves the optimality equation $v = Av$, where $A$ maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return $h$, contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.

The plain contraction assumption (each one-step operator shrinks distances by a factor $c<1$) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only $N$ steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.

Timeline:

• 1953: Shapley proves that the value of a discounted stochastic game is the fixed point of a contraction.
• 1960: Howard introduces policy iteration for finite discounted Markov decision processes.
• 1962–1965: Blackwell studies discrete and discounted dynamic programming, including the existence of optimal stationary policies.
• 1967: Denardo, in this paper, states the contraction and monotonicity assumptions for an abstract return and proves Theorems 1–4.
• 1977: Bertsekas, "Monotone mappings with application in dynamic programming", drops contraction and keeps only monotonicity.

Setting

Let $\Omega$ be a set of points. Each point $x$ has a decision set $D_x$. A policy $\delta$ picks a decision $\delta_x\in D_x$ at every point, so the policy space is $\Delta=\times_{x\in\Omega}D_x$. Let $V$ be the bounded real functions on $\Omega$ with the metric $\rho(u,v)=\sup_x|u(x)-v(x)|$; $V$ is complete. Write $u\ge v$ when $u(x)\ge v(x)$ for every $x$.

The return $h$ assigns a real number $h(x,d_x,v)$ to each point $x$, decision $d_x\in D_x$ and $v\in V$. It defines two kinds of operators on $V$:

$$[H_\delta v](x)=h(x,\delta_x,v),\qquad (Av)(x)=\sup_{d_x\in D_x}h(x,d_x,v),$$

and both are assumed to map $V$ into $V$. An operator $B$ on $V$ has modulus $c$ or less when $\rho(Bu,Bv)\le c\,\rho(u,v)$ for all $u,v$.

• Monotonicity assumption: if $u\ge v$ then $H_\delta u\ge H_\delta v$ for every $\delta$.
• N-stage contraction assumption: for a positive integer $N$ and a number $c<1$, both independent of $\delta$, every $H_\delta^N$ has modulus $c$ or less and every $H_\delta$ has modulus $1$ or less.

Under these assumptions $H_\delta^N$ is a contraction, so it has a unique fixed point $v_\delta$, the return function of $\delta$. The optimal return is $f(x)=\sup_\delta v_\delta(x)$. The auxiliary operator $E$ is $(Ev)(x)=\sup_\delta(H_\delta^Nv)(x)$.

Formalization targets

Goal: Theorem 4 (p. 169)

Under the monotonicity and N-stage contraction assumptions:

$$\text{(a) } H_\delta v_\delta=v_\delta \text{ and } v_\delta \text{ is the only fixed point of } H_\delta;\qquad \text{(b) } \rho(v_\delta,v)\le\frac{\rho(H_\delta v,v)\,N}{1-c};$$ $$\text{(c) } E \text{ has modulus } c \text{ or less};\qquad \text{(d) } f\in V,\ Ef=f,\ Af=f,\ \text{ and } f \text{ is the only fixed point of } E \text{ and of } A;$$ $$\text{(e) } v\le f\ \Longrightarrow\ \rho(A^Nv,f)\le c\,\rho(v,f).$$

Milestones

1. The observation at the end of §3 (p. 168): if every operator in a nonempty family has modulus $c$ or less, then their pointwise supremum has modulus $c$ or less, provided it maps $V$ into $V$.
2. Lemma 1 (p. 168): under monotonicity, $A$ is monotone; $Av\ge v$ implies that $A^nv$ is nondecreasing in $n$; $H_\delta v\ge v$ implies that $H_\delta^nv$ is nondecreasing in $n$.
3. Theorem 4 (a)–(c), the part the paper proves in the text of §5 before stating the theorem. This milestone also includes the existence of $E$ as an operator on $V$ and $f\in V$.
4. Lemma 2 (p. 169): $Av\le v$ implies $v\ge f$, and $Av\ge v$ implies $v\le f$; $Av_\delta\ge v_\delta$; $H_\delta v\ge v$ implies $v_\delta\ge H_\delta v$.

The mission also contains two consequences that are not milestones: $f$ is optimal for the mathematical programs $\min v$ s.t. $Av\le v$ and $\max v$ s.t. $Av\ge v$ (§6, p. 171), and a policy is optimal exactly when it attains $f(x)=h(x,\delta_x,f)$ at every point (§7, p. 173).

Significance

Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation $v=Av$ has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that $f$ is the least $v$ with $Av\le v$ and the greatest $v$ with $Av\ge v$. This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization $\Delta^*=\Delta^+$ reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.

The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after $N$ steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.

Difficulty

The obvious argument would apply the Banach fixed-point theorem to $A$. That does not work: under the N-stage assumption, $A^N$ need not be a contraction. The paper gives an example (p. 170) with $N=2$, $c=\tfrac12$, where $A^n$ has modulus $1$ for every $n$. The supremum over decisions does not commute with composition, so the contraction of each $H_\delta^N$ says nothing directly about $A^N$. The paper therefore works through the auxiliary operator $E$, which is a contraction. The hard step is to show that $f$, the supremum of the policy returns, is a fixed point of $A$. This is the second half of Lemma 2(a), an $\varepsilon$-argument that uses both monotonicity and the modulus-$1$ bound on $H_\delta$.

Part (e) holds only for $v\le f$. It is not a contraction property of $A^N$ on all of $V$.

Formalization scope

• $V$ is lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is $\rho$. The order is pointwise (PLe).
• $H$, $A$ and $E$ are given as functions $V\to V$, which is the paper's "range contained in $V$". They are tied to $h$ by IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including $f$ (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.
• "Modulus $c$ or less" is the inequality ModulusLE B c. NStageContractionAssumption H N c holds $0<N$, $c<1$, ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with $N$ and $c$ independent of $\delta$.
• The return functions are a family v with $H_\delta^Nv_\delta=v_\delta$, the paper's §5 definition. $H_\delta v_\delta=v_\delta$ is the conclusion (a), never a hypothesis.
• In the goal, $E$ is an operator with IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. $f$ is never defined as a fixed point of $A$ or $E$. The goal asserts that the pointwise least upper bound of $\{v_\delta(x)\}$ exists in $V$ and is the unique fixed point of both.
• The trivializing formalizations are ruled out explicitly: assuming $H_\delta v_\delta=v_\delta$, defining $f$ as $A$'s fixed point, or dropping $v\le f$ from (e) would each change the theorem.

A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to $H_\delta^N$), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.

Selected references

• E. V. Denardo, Contraction Mappings in the Theory Underlying Dynamic Programming, SIAM Review 9(2) (1967) 165–177. https://doi.org/10.1137/1009030
• L. S. Shapley, Stochastic Games, Proc. Nat. Acad. Sci. 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36 (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• D. P. Bertsekas, Monotone Mappings with Application in Dynamic Programming, SIAM J. Control Optim. 15(3) (1977) 438–464. https://doi.org/10.1137/0315031

Motivation

A seller with replenishable inventory must decide how much to order and what price to charge before demand is known. A price that increases current revenue can also change the inventory left for later periods; a fixed charge for placing any positive order adds a discontinuity to the decision. Chen and Simchi-Levi study this coordination problem over a finite horizon with backlogging and random, price-dependent demand. Their general-demand result characterizes an optimal order-and-price policy even when a conventional two-threshold ordering rule can fail. The paper gives explicit counterexamples to ordinary $k$-concavity and to optimality of a standard $(s,S,p)$ policy in this setting (Chen and Simchi-Levi, 2004, §4, Lemmas 3–4).

Setting

There are periods $t=1,\ldots,T$. At the start of period $t$, the firm has inventory $x$, which may be negative because unmet demand is backlogged. It may order to any level $y\ge x$. If $y>x$, it pays a fixed ordering cost $k$ as well as a variable cost $c_t(y-x)$. After ordering it chooses an expected demand level $d$ in a closed interval $[\underline d_t,\overline d_t]$. The corresponding price is $P_t(d)$, the inverse of the period's decreasing demand curve, and expected revenue is $R_t(d)=dP_t(d)$.

Actual demand is $\alpha_t d+\beta_t$. The random pair $(\alpha_t,\beta_t)$ has a period-dependent law $\mu_t$, with $\mathbb E[\alpha_t]=1$ and $\mathbb E[\beta_t]=0$. No sign restriction is placed on $\alpha_t$ in the paper's general model. The inventory after demand is $y-\alpha_t d-\beta_t$, incurring a convex holding or backlog cost $h_t$ and entering the next period. The paper assumes the random perturbations are independent across periods. Its Bellman equation uses their individual period laws (Chen and Simchi-Levi, 2004, §2, Assumptions 1–5).

The profit-to-go $v_t(x)$ starts with $v_{T+1}(x)=0$. For a post-order inventory $y$ and expected demand $d$, write

$$g_t(y,d)=R_t(d)-c_ty+\mathbb E[-h_t(y-\alpha_t d-\beta_t)+v_{t+1}(y-\alpha_t d-\beta_t)].$$

The firm maximizes $g_t(y,d)$ over admissible $d$ and then maximizes the resulting value, less the fixed ordering charge, over $y\ge x$. This defines $v_t(x)$ by equation (2) of the paper. A symmetrically $k$-convex real function $f$ satisfies

$$f((1-\lambda)x_0+\lambda x_1)\le(1-\lambda)f(x_0)+\lambda f(x_1)+\max\{\lambda,1-\lambda\}k$$

for every $x_0,x_1\in\mathbb R$ and $\lambda\in[0,1]$. A function is symmetrically $k$-concave when its negative is symmetrically $k$-convex. This is Definition 4.1, equation (8), and preserves the symmetry between the two endpoint inventories (Chen and Simchi-Levi, 2004, p. 891).

Formalization targets

The goal is Theorem 4.1(c)–(d). If $G_t(y)=\max_{d\in[\underline d_t,\overline d_t]}g_t(y,d)$, then for every period

$$G_t\text{ and }v_t\text{ are symmetrically }k\text{-concave}.$$

There are thresholds $s_t\le S_t$ and a possibly empty set $A_t\subseteq[s_t,(s_t+S_t)/2]$. An optimal policy orders to $S_t$ if $x<s_t$ or $x\in A_t$, and places no order otherwise. It chooses the maximizing expected demand for the resulting post-order level. In particular, all states that order to $S_t$ can use the same demand level $d_t(S_t)$ and hence the same price $P_t(d_t(S_t))$.

The milestones state the preceding polynomial growth and continuity assertions from Theorem 4.1(a)–(b), the threshold structure of Lemma 5(d), and the named steps in the proof on p. 892. The link from the paper's earlier $k$-convexity to symmetric $k$-convexity is also included. These targets preserve the paper's general demand law rather than restricting it to the additive case.

Significance

The theorem describes an optimal decision at every inventory level under random price-dependent demand. The exceptional set $A_t$ records states where ordering to $S_t$ is optimal inside the interval where a single reorder threshold need not describe all optimal actions. Thus the result retains a concise policy description while allowing the behavior exhibited by the paper's counterexamples (Chen and Simchi-Levi, 2004, §4).

Formalizing the result requires a reusable account of symmetric $k$-convexity, a fixed-cost ordering envelope, and a finite-horizon Bellman recursion with real-valued expectations. The source proves Theorem 4.1 on paper. This mission poses its statements as Lean goals; the theorem files currently contain sorry and therefore are not machine-checked proofs. The published platform definition BertsekasKConvex supplies the earlier notion from Definition 2.1, so the bridge to Definition 4.1 can be stated without duplicating it.

Difficulty

In the additive-demand case, a maximizing expected-demand choice can be selected so that post-demand inventory changes monotonically with the initial inventory. For general demand $\alpha_t d+\beta_t$, that monotonicity can fail: the random multiplier changes how a pricing choice moves the next inventory state. The earlier ordered-chord $k$-concavity argument therefore does not carry over unchanged. A second issue is the fixed ordering charge. It creates ties between ordering and not ordering, so the policy region can include isolated or noninterval states within $[s_t,(s_t+S_t)/2]$. The statement must assert Bellman optimality at every $x$, including those ties, rather than only the geometry of $A_t$ (Chen and Simchi-Levi, 2004, pp. 891–892).

Formalization scope

The Lean model uses expected demand $d$ as the decision variable and obtains price from $P_t(d)$, matching the paper's reformulation after Assumption 5. The admissible demand interval is nonempty. Periods are natural numbers $1,\ldots,T$, with $T>0$ and terminal value $v_{T+1}=0$. Random demand is integrated against a probability measure on $\mathbb R\times\mathbb R$. The first moments and the paper's demand moment condition are explicit; holding-cost and continuation integrability prevent a nonintegrable real integral from acquiring Lean's default zero value. The paper's $O(|y|^\rho)$ statements are encoded by constants multiplying $1+|y|^\rho$.

The formal assumptions include $k\ge0$ and $c_t\ge0$, and set $c_{T+1}=0$ where the paper's Assumption 3 uses that otherwise undefined terminal coefficient. The latter two restrictions make the printed finite-horizon claim valid under its cost interpretation; they are stated rather than silently supplied. The paper assumes temporal independence, while the formal Bellman recursion starts from the marginal laws and so needs no separate joint process. The paper's $(y,p)$ in Theorem 4.1(b) is expressed as $(y,d)$ through the continuous one-to-one price–expected-demand correspondence. The model places no positivity condition on $\alpha_t$.

The optimized demand value and ordering value are real suprema. The statements include maximizing choices and Bellman attainment; a proof cannot rely on a default value for an empty or unbounded supremum. The goal requires an actual optimal action for every inventory state. Contributions that establish integrability, continuity, coercivity, symmetric convexity preservation, or the ordering-envelope structure are useful beyond this mission.

Selected references

• Xin Chen and David Simchi-Levi, Coordinating Inventory Control and Pricing Strategies with Random Demand and Fixed Ordering Cost: The Finite Horizon Case, Operations Research 52(6), 887–896, 2004. DOI: 10.1287/opre.1040.0127.

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.

Motivation

The multi-secretary problem is the simplest model of capacity allocation under uncertainty: a decision maker sees $n$ candidates one at a time and may hire at most $k$ of them, with every decision final. The same structure underlies single-resource revenue management (accepting or rejecting booking requests against a fixed inventory; see Talluri and van Ryzin, The Theory and Practice of Revenue Management, 2004), online knapsack and packing problems, and dynamic assortment of limited stock.

The performance of an online policy is measured against the offline benchmark, the value of the best $k$ candidates chosen with full hindsight. The gap between the two is the regret.

• In the version where the values arrive as a uniform random permutation, Kleinberg (2005) proved that the minimal regret is of order $\sqrt k$ and gave an algorithm attaining it (as summarized in Remark 1 of the paper below).
• Arlotto and Gurvich (arXiv:1710.07719, 2017; Stochastic Systems 2019) showed that when the values have a finite support, the optimal online policy, and an explicit simple policy, have regret bounded by a constant that does not depend on $n$ or $k$. The constant depends only on the smallest probability mass.

This mission formalizes that upper bound.

Setting

Abilities take values in a finite set $\mathcal A=\{a_m<a_{m-1}<\dots<a_1\}$ of distinct positive reals, with probabilities $f_j=\mathbb P(X=a_j)>0$, $\sum_j f_j=1$. Write $\bar F(a_j)=f_1+\dots+f_{j-1}$ for the mass strictly above $a_j$, and

$$\epsilon=\tfrac12\min\{f_m,\dots,f_1\}.$$

The abilities $X_1,\dots,X_n$ are independent with this distribution. Budget pairs range over the triangle $\mathcal T=\{(n,k):0\le k\le n\}$.

• Offline value. $V^*_{\mathrm{off}}(n,k)=\mathbb E\big[\max\{\sum_t X_t\sigma_t:\sigma\in\{0,1\}^n,\ \sum_t\sigma_t\le k\}\big]$.
• Online policies. A policy decides $\sigma_t\in\{0,1\}$ using only $X_1,\dots,X_t$ and must select at most $k$ candidates on every realization. $\Pi(n,k)$ is the set of such policies, $V^\pi_{\mathrm{on}}(n,k)=\mathbb E[\sum_t X_t\sigma^\pi_t]$, and $V^*_{\mathrm{on}}(n,k)=\max_{\pi\in\Pi(n,k)}V^\pi_{\mathrm{on}}(n,k)$.
• Counts. $Z^r_j$ is the number of $a_j$-candidates among the first $r$. The offline sort selects $\mathfrak S^r_j=\min\{Z^r_j,(k-\sum_{i<j}Z^r_i)_+\}$ of them. $S^{\pi,r}_j$ counts those selected by $\pi$.
• Action index. $j_0(n,k)$ is the largest $j$ with $\bar F(a_j)+\tfrac12f_j\le k/n$, or $1$ if there is none.
• Thresholds. $T_1=0$, $T_j=\bar F(a_j)+\tfrac12 f_j$ for $2\le j\le m$, and $T_{m+1}=+\infty$.
• Budget-Ratio (BR) policy. With remaining budget $K_t$ ($K_0=k$), at time $t+1$ the policy finds $j$ with $T_j\le K_t/(n-t)<T_{j+1}$. It selects $X_{t+1}$ if and only if $K_t>0$ and $X_{t+1}\ge a_j$.
• Stopping times. For $0<\delta<\epsilon$, $\tau_0$ is the first time the budget ratio comes within $\delta/2$ of a threshold, or the cut-off $n-2\delta^{-1}-1$. The time $\tau$ of (20) is the first later time the ratio leaves the $\delta$-band around that threshold, or the cut-off.

Formalization targets

Goal: Theorem 1 (first display)

For every $\epsilon>0$ there is a constant $M$ such that for every instance with $\tfrac12\min_jf_j=\epsilon$ and all $(n,k)\in\mathcal T$, $\mathrm{br}\in\Pi(n,k)$ and

$$V^*_{\mathrm{off}}(n,k)-V^*_{\mathrm{on}}(n,k)\le V^*_{\mathrm{off}}(n,k)-V^{\mathrm{br}}_{\mathrm{on}}(n,k)\le a_1M.$$

No constant is fixed. Only the shape is asserted: a bound uniform in $n$, $k$, the support size and the distribution, given $\epsilon$.

Milestones, in the order the proof uses them

• The benchmark inequality $V^\pi_{\mathrm{on}}\le V^*_{\mathrm{off}}$ (p. 5).
• The sort identity $V^*_{\mathrm{off}}=\sum_ja_j\mathbb E[\mathfrak S^n_j]$ (4).
• The binomial overshoot bound $\mathbb E[(B-k)_+]\le1/(4\varepsilon)$ (Lemma 2).
• The offline decomposition $V^*_{\mathrm{off}}=\sum_{i<j}a_i\mathbb E[Z^n_i]+a_j\mathbb E[\mathfrak S^n_j]+a_{j+1}\mathbb E[\mathfrak S^n_{j+1}]\pm a_1/(4\epsilon)$ (Proposition 1).
• The sufficient condition: four properties (i)–(iv) of a policy up to a stopping time imply regret at most $3a_1M+a_1/(4\epsilon)$ (Proposition 2).
• The identification $j_0(n,k)=j$ on $k/n\in[T_j,T_{j+1})$ (p. 17).
• The BR selection probability and the jump bound $|K_t/(n-t)-K_{t+1}/(n-t-1)|\le\delta/2$ (p. 13).
• $\mathbb E[\tau]\ge n-M$ (Theorem 2).
• BR and $\tau$ satisfy (i)–(iv) (Corollary 1).
• The state-space reduction $v_\ell(w,\kappa)=w+g_\ell(\kappa)$ of the Bellman recursion (Proposition 5).

Significance

The result. Bounded regret means that the loss from not knowing the future is a fixed number of candidates' worth of value, however long the horizon and however large the budget. The bound holds uniformly over all distributions with the same $\epsilon$. It is attained by an explicit, adaptive, non-randomized rule that compares one ratio with $m$ fixed thresholds. The companion result of the same paper shows that every non-adaptive policy suffers regret of order $\sqrt n$ in the interior regime. Together they quantify the value of adapting to the remaining budget. Lemma 1 of the paper shows the dependence on $\epsilon$ cannot be removed.

Formalizing it. The result is proved in the paper, but no part of it is machine-checked; there is no multi-secretary or bounded-regret development on the platform. The mission produces several pieces of machinery: a reusable finite model of sequential selection with online policies and the offline benchmark; an explicit online policy with its stopping-time analysis; and a binomial overshoot bound usable elsewhere. The constant $M$ is not made explicit in the paper. A formal proof would give one, and sharper constants are welcome.

Difficulty

The offline decomposition and the sufficient condition are bookkeeping with counts and one concentration bound. The hard step is Theorem 2: showing that the budget ratio $K_t/(n-t)$ stays within $\delta$ of its attracting threshold until a bounded expected number of periods before the end. Near the horizon a single selection moves the ratio by about $1/(n-t)$, so the band becomes easy to leave. Equivalently, the target $\delta(n-\tau_0-u)$ that the deviation process must exceed shrinks to zero. A standard martingale or drift argument with a fixed band therefore does not give a bound uniform in $n$. The paper combines the mean-reverting drift of the deviation process with an exponential tail bound (its Proposition 4) and a Lyapunov argument. A second subtlety is uniformity: every constant must depend on $\epsilon$ (and $\delta$) only, never on $m$, the $a_j$, $n$ or $k$.

Formalization scope

The source is arXiv:1710.07719v2; its printed page numbers equal the PDF page numbers.

Representation.

• Ability levels are Fin m, with index 0 the largest value $a_1$; Lean index $i$ is the paper's $i+1$.
• Each instance carries $a$ strictly decreasing and positive, $f$ positive with $\sum f=1$.
• Expectations are finite sums over sequences $x:\mathrm{Fin}\,n\to\mathrm{Fin}\,m$ weighted by $\prod_tf(x_t)$, so no measure theory is needed.
• Policies are deterministic selection rules $\sigma(x,t)$ that are non-anticipating and feasible. $V^*_{\mathrm{on}}$ is a maximum over this finite set. The paper allows randomized policies; for this finite problem the optimal values coincide (p. 39). In any case, restricting to deterministic policies can only lower $V^*_{\mathrm{on}}$ and so does not weaken the goal.
• $V^*_{\mathrm{off}}$ is defined as an expected maximum over selection vectors, not by the sort formula. The sort formula is a milestone.

Quantifiers. The constant $M$ in the goal is chosen after $\epsilon$ and before $m$, the instance, $n$ and $k$. A statement with $M$ chosen after the instance, or after $n$, is trivial (regret $\le a_1n$) and is excluded.

Corrections to the printed text, disclosed in the items.

1. In Theorem 2 and Corollary 1, $M$ depends on the auxiliary $\delta\in(0,\epsilon)$ as well, because $\tau$ does. $\delta$ is quantified before $M$. The goal itself is $\delta$-free.
2. Lemma 2's conditions $p+\varepsilon\le k/n$, $k/n\le p-\varepsilon$ are stated as $(p+\varepsilon)n\le k$, $k\le(p-\varepsilon)n$, the form used in its proof. This avoids a false case at $n=0$.
3. The BR rule is applied at every time $t+1\in\{1,\dots,n\}$; p. 11 writes $\{1,\dots,n-1\}$.
4. $\tau$ is capped at $n$, which matters only when $n=0$.
5. In Proposition 5 the recursions are imposed for $\kappa\ge1$ (boundary conditions at $\kappa=0$), and only identity (49) is stated.

Infrastructure. The model definitions (instance, offline value, online policies, counts, thresholds, action index) and the binomial overshoot lemma are reusable for other finite-support online selection and revenue-management results. All of the following are welcome:

• proofs of individual milestones;
• an explicit constant;
• a formal derivation of $V^*_{\mathrm{on}}(n,k)=v_n(0,k)$ connecting Proposition 5 to $V^*_{\mathrm{on}}$.

Selected references

• A. Arlotto, I. Gurvich, Uniformly Bounded Regret in the Multi-Secretary Problem, arXiv:1710.07719v2, 2018; Stochastic Systems 9(3), 2019. https://arxiv.org/abs/1710.07719
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004. https://doi.org/10.1007/b139000
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978.
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

Discounted dynamic programming with bounded cost per stage is the standard setting in which infinite-horizon sequential decision problems are well posed: the optimal cost exists, satisfies Bellman's equation, and can be computed by iterating the DP operator. Shapley proved this for stochastic games in 1953 (Shapley 1953), Blackwell for discounted Markov decision processes in 1965 (Blackwell 1965), and Denardo observed in 1967 that the arguments use only two properties of the DP operator: monotonicity and contraction in the supremum norm (Denardo 1967). Bertsekas (1975, 1977) and Bertsekas and Shreve (1978) turned this observation into an abstract dynamic programming framework, in which a single mapping $H$ encodes stochastic, deterministic, minimax and multiplicative-cost problems at once (Bertsekas 1977).

Chapter 4 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case, is the contraction part of that framework. Its results are the abstract form of what every course on Markov decision processes proves for the discounted case, and they are what later work on abstract DP (Bertsekas, Abstract Dynamic Programming, 2022) and on robust and regularized MDPs builds on.

Setting

A model consists of a state space $S$, a control space $C$, a nonempty constraint set $U(x)\subseteq C$ for each $x\in S$, a mapping $H:S\times C\times F\to[-\infty,\infty]$, where $F$ is the set of functions $S\to[-\infty,\infty]$, and a function $J_0\in F$ with $J_0>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$; $M$ is the set of selectors, and a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ in $M$. The operators are

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).$$

The cost of $\pi$ is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0)(x)$, the optimal cost is $J^*(x)=\inf_{\pi}J_\pi(x)$, and $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$.

$B$ is the Banach space of bounded real functions on $S$ with $\|J\|=\sup_x|J(x)|$. Assumption C asks for a closed set $\bar B\subseteq B$ containing $J_0$ and invariant under $T$ and every $T_\mu$; that every limit defining $J_\pi$ exist and be real; and that for some integer $m\ge1$ and scalars $0<\rho<1$, $\alpha>0$,

$$\|T_\mu(J)-T_\mu(J')\|\le\alpha\|J-J'\|\quad(J,J'\in B),\qquad \|(T_{\mu_0}\cdots T_{\mu_{m-1}})(J)-(T_{\mu_0}\cdots T_{\mu_{m-1}})(J')\|\le\rho\|J-J'\|\quad(J,J'\in\bar B).$$

Formalization targets

Goal: Proposition 4.2

Under Assumption C,

$$J^*\in\bar B,\qquad J^*=T(J^*),\qquad J'\in\bar B,\ J'=T(J')\ \Rightarrow\ J'=J^*,$$

$T(J')\le J'$ implies $J^*\le J'$ and $J'\le T(J')$ implies $J'\le J^*$ for $J'\in\bar B$; each $J_\mu$ is the unique fixed point of $T_\mu$ in $\bar B$; and for every $J\in\bar B$

$$\lim_{N\to\infty}\|T^N(J)-J^*\|=0,\qquad\lim_{N\to\infty}\|T_\mu^N(J)-J_\mu\|=0.$$

The statement carries no constants beyond those of Assumption C.

Milestones

• Fixed Point Theorem (p. 55): an $m$-step contraction of a nonempty closed subset of a Banach space has a unique fixed point, which attracts every orbit.
• Proposition 4.1 (p. 53): $J_\pi$ does not depend on the terminal function in $\bar B$; $\inf_\pi(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)=T^N(J)$; $T^m$ and $T_\mu^m$ are $\rho$-contractions on $\bar B$.
• Proposition 4.3 (p. 56): $(\mu^*,\mu^*,\dots)$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$; pointwise optimal policies yield a stationary optimal one; stationary $\varepsilon$-optimal policies exist.
• Proposition 4.4 (p. 57): compactness of the sets $\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ gives policies attaining the DP infimum, and their accumulation points are optimal stationary policies.
• Proposition 4.11 (p. 69): the discounted minimax model with $0\le g\le b$ and $\alpha<1$ satisfies Assumption C with $\bar B=B$, $m=1$, $\rho=\alpha$.

Further result

• Proposition 4.5 (p. 59), a draft theorem of this mission that is not a milestone: the error bound $J^*\le J_\mu\le J^*+(2\alpha\varepsilon_1+\varepsilon_2)(1+\alpha+\cdots+\alpha^{m-1})/(1-\rho)$.

Significance

Proposition 4.2 is the existence-and-uniqueness theorem for Bellman's equation in the contraction regime, together with the convergence of value iteration from an arbitrary start in $\bar B$. Propositions 4.3 to 4.5 turn it into statements about policies: when a stationary optimal policy exists, how one is found from the DP algorithm, and how much is lost when Bellman's equation is solved only approximately. Proposition 4.11 shows the assumption is met by a concrete class of problems, discounted minimax control, and so certifies that the abstract theorems are not vacuous.

The results are classical and have been proved in print since 1978; none of them is open. What this mission adds is a machine-checked version of the abstract theory itself, rather than of a single model. Mathlib has the Banach fixed point theorem for a contracting map of a complete space (ContractingWith) and a lemma for contracting iterates, but not the version on a closed subset with norm convergence of every orbit, and nothing on abstract DP. The platform has proved the finite-state discounted case for a concrete model (BertsekasDP.discounted_main_theorem); the abstract statements here cover infinite state spaces, minimax problems and $m$-step contractions, and are reused by the later missions of this series (generalized models, Chapter 6) and by papers that cite the book.

Difficulty

The first idea is to apply the contraction mapping principle to $T$ and read off $J^*$ as its fixed point. That gives a fixed point of $T$ but says nothing about $J^*$, which is defined as an infimum over all, generally nonstationary, policies of limits of compositions. The identification of the fixed point with $J^*$ is the content of the proposition, and it is where the Lipschitz condition (2) on all of $B$, not only on $\bar B$, enters.

Two further features block a direct appeal to Mathlib. The contraction is only $m$-step, so neither $T$ nor $T_\mu$ need be a contraction. And $H$ takes extended-real values, so every passage between $F$ and the Banach space $B$ must be justified by the invariance of $\bar B$.

Formalization scope

The state and control spaces are arbitrary types. $F$ is S → EReal; $B$ is Mathlib's lp (fun _ : S => ℝ) ⊤, whose norm is the supremum norm, and toF embeds $B$ into $F$. $\bar B$ is an arbitrary closed subset of $B$, not $B$ itself, and uniqueness of fixed points is asserted within $\bar B$. Policies are sequences ℕ → M; $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ is the pointwise limit (limUnder), which exists and is real under Assumption C; $J^*$ is the infimum over all policies.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$, whereas Mathlib's EReal has $\bot+\top=\bot$. No statement adds infinities of opposite sign. A norm bound $\|J-J'\|\le c$ between functions of $F$ is the predicate SupDistLe: both functions are real at every point and differ by at most $c$, which is what the bound means under the book's arithmetic. Condition (2) is imposed on all of $B$, as on p. 53. The scalars $m,\rho,\alpha$ of Assumption C are explicit parameters, so the constant of Proposition 4.5 is the book's exact expression. The Fixed Point Theorem assumes $\bar B$ nonempty, which the page leaves implicit and without which the statement is false.

Defining $J^*$ as the fixed point of $T$, or replacing it by the infimum over stationary policies, would make the goal trivial. Neither is done here: $J^*$ is the infimum of the policy costs, exactly as in Eq. (8) of Chapter 2.

A complete development needs the $m$-step fixed point theorem on closed subsets of a Banach space, which can be reused well beyond dynamic programming; the elementary calculus of SupDistLe and of the embedding of $B$ into S → EReal; and the monotone-operator inequalities of Section 2.1. Contributions of any of these, or alternative proofs of the milestones, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific reprint 1996, Chapter 4. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9 (1967) 165–177. https://doi.org/10.1137/1009030
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• L. S. Shapley, Stochastic games, Proc. Natl. Acad. Sci. USA 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979) 15–30. https://doi.org/10.1287/moor.4.1.15

Motivation

Every step of the dynamic programming algorithm on a general state space does three things: it takes a conditional expectation of the cost-to-go under a transition kernel, it minimizes the resulting function of state and control over the control, and, if a policy is to be produced, it picks a control for each state that attains or nearly attains that minimum. On a finite or countable state space all three are harmless. On an uncountable state space each can destroy the measurability needed to take the next expectation: the infimum over an uncountable family of measurable functions need not be measurable, and a minimizer chosen state by state need not be a measurable function of the state, so it does not define a policy at all.

Section 7.5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), settles the three operations for semicontinuous costs and continuous kernels. The results are the topological half of the book's measurability theory; the descriptive set theory half (lower semianalytic functions and analytically measurable selectors, §7.6–7.7) is a separate mission in this series. The semicontinuous results are what Propositions 8.6–8.7 and Corollaries 9.17.2–9.17.3 of the book use to obtain Borel-measurable optimal policies for finite-horizon and infinite-horizon models with lower semicontinuous costs and compact control sets.

Timeline. The exact selection theorem for lower semicontinuous functions (Proposition 7.33 below) is credited by the book's notes to Dubins and Savage, How to Gamble If You Must (1965). The Hausdorff metric on closed sets goes back to Hausdorff's Set Theory. Measurable selection in the closed-valued setting was later systematized by Kuratowski and Ryll-Nardzewski (1965), whose theorem gives a different route to results of this kind.

Setting

Throughout, $R^*=[-\infty,+\infty]$ is the extended real line. A function $f:X\to R^*$ on a metrizable space $X$ is lower semicontinuous if every sublevel set $\{x\mid f(x)\le c\}$, $c\in\mathbb R$, is closed, and upper semicontinuous if every superlevel set $\{x\mid f(x)\ge c\}$ is closed (Definition 7.13). $C(X)$ is the space of bounded continuous real-valued functions on $X$.

For a separable metrizable space $Y$, $P(Y)$ is the set of Borel probability measures on $Y$ with the weak topology (convergence of integrals of functions in $C(Y)$). A stochastic kernel $q(dy\mid x)$ on $Y$ given $X$ is a map $x\mapsto q(dy\mid x)$ from $X$ to $P(Y)$, and it is continuous if this map is continuous (Definition 7.12). The integral of a Borel-measurable $f:Y\to R^*$ is $\int f\,dp=\int f^+dp-\int f^-dp$ with the convention $-\infty+\infty=+\infty-\infty=+\infty$ (Eq. (43) of Chapter 7).

For a compact metric space $Y$, $2^Y$ is the collection of closed subsets of $Y$ with the topology of the Hausdorff metric (Appendix C). For $D\subseteq X\times Y$, the section at $x$ is $D_x=\{y\mid (x,y)\in D\}$, the projection is $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and a function $\varphi:\mathrm{proj}_X(D)\to Y$ has its graph in $D$ if $(x,\varphi(x))\in D$ for every $x\in\mathrm{proj}_X(D)$. "Borel-measurable" refers to the Borel σ-algebras of the topologies in question; on $\mathrm{proj}_X(D)$ this is the Borel σ-algebra of the subspace topology.

Formalization targets

Goal: Proposition 7.33

Let $X$ be metrizable, $Y$ compact metrizable, $D\subseteq X\times Y$ closed, and $f:D\to R^*$ lower semicontinuous. Put

$$f^*(x)=\min_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

Then $\mathrm{proj}_X(D)$ is closed, $f^*$ is lower semicontinuous, and there is a Borel-measurable $\varphi:\mathrm{proj}_X(D)\to Y$ with graph in $D$ and

$$f\bigl(x,\varphi(x)\bigr)=f^*(x)\qquad\forall x\in\mathrm{proj}_X(D).$$

Milestones

• Proposition 7.32: for $f^*(x)=\inf_{y\in Y}f(x,y)$, lower semicontinuity of $f$ and compactness of $Y$ give lower semicontinuity of $f^*$ and attainment; upper semicontinuity of $f$ gives upper semicontinuity of $f^*$.
• Lemma 7.18: there is a Borel-measurable $\sigma:2^Y-\{\emptyset\}\to Y$ with $\sigma(A)\in A$.
• Lemma 7.20: for lower semicontinuous $f$ on a nonempty compact $Y$, the argmin map $x\mapsto\{y\mid f(x,y)\le f^*(x)\}$ is Borel-measurable into $2^Y$.
• Lemma 7.14: $f$ is lower semicontinuous and bounded below iff $f_n\uparrow f$ for some $f_n\in C(X)$ (and dually).
• Proposition 7.30: $x\mapsto\int f(x,y)\,q(dy\mid x)$ is continuous for $f\in C(X\times Y)$ and continuous $q$.
• Proposition 7.31: the same map is lower (upper) semicontinuous and bounded below (above) when $f$ is.
• Lemma 7.21: an open $G\subseteq X\times Y$, $Y$ separable, has open projection and a Borel-measurable selector with graph in $G$.
• Proposition 7.34: for open $D$ and upper semicontinuous $f$, $\mathrm{proj}_X(D)$ is open, $f^*=\inf_{D_x}f$ is upper semicontinuous, and for each $\varepsilon>0$ there is a Borel-measurable $\varphi_\varepsilon$ with graph in $D$ and

$$f\bigl(x,\varphi_\varepsilon(x)\bigr)\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

Significance

The results. Propositions 7.31–7.33 are the closure properties that make the dynamic programming recursion stay inside the class of lower semicontinuous functions bounded below: the expectation step preserves the class (7.31), the minimization step preserves it (7.32, 7.33), and the minimization admits a Borel-measurable exact minimizer (7.33). This is why, in semicontinuous models, the optimal cost functions are lower semicontinuous and optimal policies can be taken Borel-measurable and nonrandomized. Proposition 7.34 gives the weaker, $\varepsilon$-optimal counterpart for upper semicontinuous costs, where the infimum need not be attained.

Formalizing them. All of these results are proved in the book; none is open. As far as is known, none has a machine-checked proof: Mathlib has semicontinuity, the Hausdorff extended metric on closed and on nonempty compact sets, and the weak topology on probability measures, but no theorem combining them into a measurable selection result of this kind. A formal development would supply measurable selectors for semicontinuous minimization in Lean and the Borel-measurability of set-valued maps into the hyperspace of closed sets, both reusable well beyond dynamic programming.

Difficulty

The obvious attempt at the goal is to pick, for each $x$, some minimizer $y$ of $f(x,\cdot)$ over the compact section $D_x$. The minimizer exists by compactness and lower semicontinuity, but the choice is made pointwise and gives no control on measurability: a minimizer chosen by the axiom of choice need not be Borel-measurable. The argmin sets $F^*(x)$ vary with $x$ only semicontinuously: they can jump from a single point to a large set, so a continuous selection generally does not exist, and continuity arguments cannot replace measurability. Lemma 7.18 isolates the hardest part: a choice of a point of each nonempty closed set that is measurable as a function of the set itself.

A second difficulty is bookkeeping at infinity. Values $\pm\infty$ are allowed throughout, so sublevel sets, minima, integrals and $\varepsilon$-bounds must all be handled in $R^*$; the integral in Proposition 7.31 uses the convention $\infty-\infty=+\infty$, which is not Mathlib's.

Formalization scope

• Extended reals. Values are in EReal. The only place where values of opposite infinite sign are combined is the integral, which is the published definition DupacovaWets.Consistency.expect (reused, not restated): $\int f^+-\int f^-$ with an explicit case returning $+\infty$ when $\int f^+=\infty$, exactly the book's convention (42). The $\varepsilon$-bound of Proposition 7.34 adds a real $\varepsilon$ to a value different from $-\infty$, which is safe in EReal.
• Semicontinuity is Mathlib's LowerSemicontinuous/UpperSemicontinuous, equivalent to Definition 7.13 for EReal-valued functions. Lemma 7.13 of the book (the sequential characterization) is Mathlib's lowerSemicontinuous_iff_le_liminf together with first countability of metrizable spaces, and is not restated here.
• Functions on $D$. Functions "on $D$" are functions on $X\times Y$ with LowerSemicontinuousOn f D (resp. UpperSemicontinuousOn); values off $D$ play no role. $\mathrm{proj}_X(D)$ is Prod.fst '' D, selectors are functions on that subtype, and its σ-algebra is the Borel σ-algebra of the subspace topology.
• Hyperspace. $2^Y$ is Closeds Y, and $2^Y-\{\emptyset\}$ for compact $Y$ is NonemptyCompacts Y, each with the Hausdorff extended metric and the Borel σ-algebra of its topology. This topology agrees with the book's (the exponential topology of Appendix C, independent of the metric).
• Boundedness. "Bounded below/above" is by a real constant. BddBelow in EReal would be vacuous and is not used.
• Edge cases. Proposition 7.32(a)'s attainment clause is stated for nonempty $Y$, since for $Y=\emptyset$ the infimum is $+\infty$ and nothing attains it.
• Argmin minimum. Lemma 7.20 assumes nonempty $Y$ because its defining formula uses a minimum; for empty $Y$ there is no minimizer.
• Ruling out trivial readings. The graph condition $(x,\varphi(x))\in D$ is part of every selection statement; without it the goal would follow from the unconstrained case. The selector must be Borel-measurable on $\mathrm{proj}_X(D)$ and must attain the minimum exactly, not up to $\varepsilon$.

A complete development needs the Borel structure of the hyperspace (measurability of maps into Closeds Y from upper semicontinuity in the sense of Kuratowski, Proposition C.4 of the book), the construction of a measurable choice function on NonemptyCompacts Y, and approximation of semicontinuous functions by monotone sequences in $C(X)$. Each of these is reusable on its own; proofs of individual milestones by any route are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996, Section 7.5 and Appendix C. https://web.mit.edu/dimitrib/www/soc.html
• L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965.
• K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors," Bull. Acad. Polon. Sci. 13 (1965), 397–403.
• F. Hausdorff, Set Theory, Chelsea, New York, 1957.