Dynamic Programming

Motivation

The Russian option of Shepp and Shiryaev pays its holder, at an exercise time of their choosing, the running maximum of the stock price, discounted, with no fixed maturity. It is the standard example of a perpetual lookback option, and its value is a model problem of optimal stopping for a two-dimensional Markov process (the price and its running maximum). Perpetual contracts are simple to analyse but economically unrealistic: every real contract ends. Canadization (Carr, Randomization and the American put, Rev. Financial Stud. 11, 1998, https://doi.org/10.1093/rfs/11.3.597) replaces a fixed maturity by an independent exponential time $\eta(\lambda)$. The holder must exercise before $\eta(\lambda)$; if they have not, they are paid the claim evaluated at $\eta(\lambda)$. Because the exponential law is memoryless, the problem stays time-homogeneous and its value can be computed in closed form, while it approximates a contract of finite expected life $1/\lambda$.

Avram, Kyprianou and Pistorius (AKP04) solved both the perpetual and the Canadized Russian problem when the log-price is a spectrally negative Lévy process: a process with stationary independent increments whose only jumps are downward. This covers Brownian motion with drift, the Black–Scholes model, and jump-diffusions with downward jumps (crashes). Their answer is written with the scale functions $W^{(q)}$, $Z^{(q)}$ of the process. This mission is the third of three drawn from that paper, and formalizes the Canadized problem (§7, Theorem 3).

Timeline. Shepp and Shiryaev (1993) solved the Russian option for geometric Brownian motion. Carr (1998) introduced Canadization for the American put. Kyprianou and Pistorius (Ann. Appl. Probab. 13, 2003) studied perpetual options through fluctuation theory; §7 of [AKP04] builds on their calculations. Avram, Kyprianou and Pistorius (2004) solved the perpetual and Canadized problems for general spectrally negative Lévy processes.

Setting

Let $(\Omega,\mathcal F,\mathbf F=\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a filtered probability space with $\mathbf F$ right-continuous, and let $X=\{X_t\}_{t\ge0}$ be a spectrally negative Lévy process adapted to $\mathbf F$: $X_0=0$, paths càdlàg with no upward jumps and not monotone, increments $X_{s+t}-X_s$ stationary and independent of $\mathcal F_s$. The standing assumption is that $X$ has unbounded variation, or bounded variation and a Lévy measure $\Lambda(dx)\ll dx$.

The Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$. Fix $r\ge0$ with $\psi(1)=r$, and let $\mathbb P^1$ be the Esscher measure, $d\mathbb P^1/d\mathbb P|_{\mathcal F_t}=e^{X_t-rt}$.

For $q\ge0$ the $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies $\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=(\psi(\theta)-q)^{-1}$ for $\theta>\Phi(q)$, where $\Phi(q)$ is the largest root of $\psi(\theta)=q$. Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(y)\,dy$. All scale functions in this mission are those of $(X,\mathbb P)$.

Starting from $Y_0=z\ge0$ (the paper's $\mathbb P^1_{-z}$), the reflected process is $Y_t=\overline X_t-X_t$, where $\overline X_t=\max\{0,\sup_{u\le t}(-z+X_u)\}$ and the position is $-z+X_t$. Its passage time above $k$ is $\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}$.

Let $\alpha>0$, and let $\eta(\lambda)$ be an exponential random variable of rate $\lambda>0$ which under $\mathbb P^1$ is independent of $\mathcal F_\infty$. The Canadized Russian problem (32) is

$$w^{CR}(z)=\sup_\tau\ \mathbb E^1_{-z}\Big[e^{-\alpha(\tau\wedge\eta(\lambda))+Y_{\tau\wedge\eta(\lambda)}}\Big],$$

over all $\mathbb P^1$-a.s. finite $\mathbf F$-stopping times $\tau$. Write $p=\alpha+\lambda+r$.

Formalization targets

Goal: Theorem 3

With

$$\kappa_*=\inf\{x\ge0:\ Z^{(p)}(x)-pW^{(p)}(x)\le-\lambda/(p-\lambda)\},\qquad h(z)=\frac{(p-\lambda)e^zZ^{(p)}(\kappa_*-z)}{p}+\frac{\lambda e^z}{p},$$

for every $z\ge0$:

$$w^{CR}(z)=h(z),$$

and $\tau_{\kappa_*}$ is a $\mathbb P^1$-a.s. finite $\mathbf F$-stopping time attaining the supremum. The statement covers every variation regime at once.

Milestones

In attack order:

1. Lemma 2 (i), which gives the monotonicity behind $\kappa_*$.
2. Corollary 1 (29), the value of stopping at $\tau_k$ at discount rate $\alpha+\lambda$.
3. The elimination of $\eta(\lambda)$ (display after (32)):

$$\mathbb E^1_{-z}\big[e^{-\alpha(\tau\wedge\eta)+Y_{\tau\wedge\eta}}\big]=\mathbb E^1_{-z}\Big[e^{-(\alpha+\lambda)\tau+Y_\tau}+\lambda\int_0^\tau e^{-(\alpha+\lambda)t+Y_t}dt\Big].$$

4. The Itô identity (34).
5. The expected $d\overline X$-integral up to $\tau_k$.
6. Lemma 3 (33), the value of $\tau_k\wedge\eta(\lambda)$.
7. Lemma 4, with two misprints corrected.
8. The supermartingale property of $U_t=e^{-(\alpha+\lambda)t}h(Y_t)+\lambda\int_0^te^{-(\alpha+\lambda)u+Y_u}du$.
9. The identity $h(z)=e^z+(p-\lambda)e^z\int_0^{\kappa_*-z}W^{(p)}\ge e^z$.

Significance

The result. Theorem 3 gives the price and the optimal exercise rule of a Russian option with random (exponential) maturity, for every spectrally negative Lévy model at once. It makes three things explicit. The optimal rule is a threshold rule for the reflected process $Y$. The threshold $\kappa_*$ is the crossing point of one explicit function of the scale functions. Whenever $W^{(p)}(0+)\ge(p-\lambda)^{-1}$ (possible only with bounded variation), immediate exercise is optimal. Because scale functions are known in closed form for many models, including Brownian motion with drift and hyper-exponential jump-diffusions (§8 of the paper), the theorem produces explicit prices.

Formalizing it. The result is proved on paper. It is not formalized in any proof assistant, and none of its infrastructure is available in Lean. This mission produces:

• a path-level definition of spectrally negative Lévy processes;
• scale functions defined as definite descriptions;
• the reflected process and its passage times;
• the Esscher change of measure as data;
• a continuous-time optimal stopping problem with an independent random horizon, valued in $[0,\infty]$.

A machine-checked proof would also check the verification argument, which the paper states in detail only for the unbounded-variation case.

Difficulty

The obvious route is to compute the value of every threshold rule (Lemma 3) and optimize over $k$. That identifies the right candidate, but it does not show that no other stopping time does better. The verification step needs two things for all regimes of $W^{(p)}(0+)$: that $U$ is a supermartingale, and that $U$ stopped at $\tau_{\kappa_*}$ is a martingale. For processes of bounded variation, $h$ is only continuous, not $C^1$, at $\kappa_*$, so a smooth Itô formula does not apply directly. Computing the expected $d\overline X$-integral up to $\tau_k$ uses excursion theory of $Y$ away from $0$, which Mathlib does not have. Eliminating $\eta(\lambda)$ is easy only if $\eta$ is independent of the whole filtration. If it is independent of $X$ alone, a stopping time could depend on $\eta$.

Formalization scope

• Conventions. Time is $[0,\infty)$ (ℝ≥0) and values are real. Random times take values in WithTop ℝ≥0, and the payoff is $0$ on $\{\tau=\infty\}$. Expectations of nonnegative payoffs are lower Lebesgue integrals in $[0,\infty]$, and $w^{CR}$ is an extended-real supremum, so no expectation defaults to $0$. Equalities with a real right-hand side also assert finiteness.
• Readings of informal words.
  • "The usual conditions" means right-continuity of $\mathbf F$, without completeness. Completing $\mathcal F_0$ with $\mathbb P$-null sets would contradict the Esscher relation, since $\mathbb P^1$ and $\mathbb P$ are typically singular on $\mathcal F_\infty$.
  • "Unbounded variation" means "not almost surely of bounded variation on compacts". (AC) is stated through jumps.
  • "ψ(v) < ∞" means integrability of $e^{vX_1}$.
  • "Decreases monotonically" means strictly decreasing, and "the unique root" means unique on $[0,\infty)$.
  • $W^{(p)}(0+)$ is the right limit.
  • "Almost surely finite" and the law and independence of $\eta(\lambda)$ are all under $\mathbb P^1$, where independence is from $\mathcal F_\infty$. "Parameter $\lambda$" is the rate.
  • $\mathbb P^1_{s,x}$ is encoded pathwise through the reflected process with $Y_0=s-x$.
  • The elimination of $\eta$ is stated τ by τ, which implies the page's equality of suprema.
  • The supermartingale claim, derived on the page in the unbounded-variation case, is stated for all cases.
  • Corollary 1's discount rate is renamed $a$.
  • (34) is stated as $pA+B=e^{s-x}+C$ with $A$, $B$, $C$ finite.
• Definition choices. Scale functions are defined by choice from their defining property, never as hypotheses on an arbitrary function. $W^{(q)}$ for $q<0$ is the series (5), not the tilting formula of Remark 4. $\mathbb P^1$ is a measure given with the Esscher relation. $d\overline X_t$ is the Lebesgue–Stieltjes measure of the running-maximum path.
• Corrected misprints. Lemma 4 is printed with $p^{-1}$ and $-\lambda/p$. The definition of $\kappa_*$ (p. 233) and the proof of Theorem 3 (p. 235) require $(p-\lambda)^{-1}$ and $-\lambda/(p-\lambda)$, and the printed version is false when $p^{-1}\le W^{(p)}(0+)<(p-\lambda)^{-1}$. The corrected statement is formalized.
• Ruled out. A supremum over stopping times of a filtration containing $\sigma(\eta)$, or a real-valued supremum or Bochner expectation that could be $0$ by default, would trivialize the goal or change it. The admissible class is every $\mathbb P^1$-a.s. finite stopping time of the given filtration, of which $\eta$ is independent. Replacing the goal by the $\eta$-free rewriting would state milestone 3 as if it were Theorem 3.
• Needed and reusable. A complete development needs Lévy process theory, scale functions, fluctuation identities for the reflected process, optional stopping in continuous time, and Itô or change-of-variable formulas for semimartingales with jumps. The Lévy-process, scale-function and reflected-process definitions are shared with the other two missions of the series and are reusable in ruin theory and queueing. Proofs of any milestone, and sorry-free facts about the definitions, are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• P. Carr, Randomization and the American put, Rev. Financial Stud. 11(3), 597–626, 1998. https://doi.org/10.1093/rfs/11.3.597
• L. A. Shepp, A. N. Shiryaev, The Russian option: reduced regret, Ann. Appl. Probab. 3, 603–631, 1993. https://doi.org/10.1214/aoap/1177005715
• A. E. Kyprianou, M. R. Pistorius, Perpetual options through fluctuation theory, Ann. Appl. Probab. 13, 1077–1098, 2003. https://doi.org/10.1214/aoap/1060202835
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996.

Motivation

Real investors do not merely accumulate wealth for a single terminal payoff; they consume along the way, and the market they invest in is rarely a single fixed statistical regime for years at a time — bull and bear markets, business cycles, and volatility regimes shift the distribution of returns. Bäuerle and Rieder's §4.3 extends the terminal-wealth theory of chunk 04a by adding a consumption choice at every stage (the Ramsey/Merton consumption-investment problem), and §4.4 extends it again by letting the return distribution itself depend on a hidden, Markov-modulated environment state. Both extensions are shown to be genuine instances of the same abstract finite-horizon Markov Decision Process machinery from Chapter 2 — the joint consumption-investment choice and the extra regime coordinate change the state and action spaces, but not the proof strategy, which is exactly the point.

Setting

The consumption-investment problem: state $E := \mathrm{dom}\,U_p$ (wealth), action $\mathbb{R}_{\ge0}\times\mathbb{R}^d$ (consumption $c$, amounts $a$ invested), transition $T_n(x,c,a,z) = (1+i_{n+1})(x-c+a\cdot z)$, reward $r_n(x,c,a) := U_c(c)$, terminal reward $g_N := U_p$. Value functions $V_n(x) := \sup_\pi \mathbb{E}^\pi_{n,x}[\sum_{k=n}^{N-1} U_c(c_k(X_k)) + U_p(X_N)]$. The one-period sub-problem: $D(x) := \{(c,a) : 0\le c\le x,\ (1+i)(x-c+a\cdot R)\in\mathrm{dom}\,U_p \text{ a.s.}\}$, $u(x,c,a) := U_c(c) + \mathbb{E}[U_p((1+i)(x-c+a\cdot R))]$, $v(x) := \sup_{(c,a)\in D(x)} u(x,c,a)$.

The regime-switching extension (§4.4): an environment process $(Y_n)$, a finite-state Markov chain with transition probabilities $p_{jk}$, modulates the risky-asset return law: given $Y_n=j$, the next relative risk $R_{n+1}$ has law $Q_j$, and $(R_{n+1},Y_{n+1})$ has joint law $Q_j(dz)p_{jk}$ given $Y_n=j$, $Y_{n+1}=k$. The augmented state is $(x,j) \in [0,\infty)\times E_Y$; value functions $J_n(x,j)$ are defined analogously, with the recursion incorporating a finite sum over the next regime.

Formalization targets

Goal — Theorem 4.3.3

$$V_N = U_p, \qquad V_n(x) = \sup_{(c,a)\in D_n(x)} \bigl[U_c(c) + \mathbb{E}\,V_{n+1}\bigl((1+ i_{n+1})(x-c+a\cdot R_{n+1})\bigr)\bigr],$$

with $V_n$ strictly increasing, strictly concave, continuous, and an optimal strategy realized by per-stage maximizers. This is chunk 04a's Theorem 4.2.2 with consumption added, and every closed-form corollary below specializes it.

Eight milestones: the one-period existence/regularity theorem (Theorem 4.3.1); the zero-mean special case (Theorem 4.3.5); power- and logarithmic-utility closed forms (Theorems 4.3.6, 4.3.7); the regime-switching generalization of the goal itself (Theorem 4.4.1), its power-utility closed form (Theorem 4.4.2), and two comparative-statics results on how the optimal policy moves across regimes under a stochastic order (Theorems 4.4.4, 4.4.5).

Significance

Theorem 4.3.3's consumption-investment structure theorem is the basis for every result about optimal spending and saving under uncertainty; its power/log closed forms (Theorems 4.3.6/4.3.7) recover the classical facts that a power-utility investor consumes and invests constant fractions of current wealth (myopic, wealth-independent policy fractions) while a log-utility investor's optimal consumption fraction, $1/(N-n+1)$, is the textbook "consume your remaining horizon's worth" rule. The regime-switching extension (§4.4) is the discrete-time analogue of Hamilton's regime-switching models, now standard in empirical finance; Theorems 4.4.4-4.4.5 give a rigorous comparative-statics answer to "does a riskier regime call for more or less stock exposure," using the increasing-concave stochastic order rather than a first- moment heuristic — the mathematically correct notion of "regime $k$'s returns dominate regime $j$'s for every risk-averse (concave, monotone) preference," not merely "regime $k$ has a higher mean."

No result of this chunk was found on the platform (searched "consumption investment", "regime switching", "stochastic order"). The proofs largely mirror chunk 04a's (the book itself says so explicitly for Theorems 4.3.1, 4.3.7, 4.4.2), so this mission's contribution is the precise joint-choice statement of each result and, for the comparative-statics theorems, the correct increasing-concave order (≤_icv, Definition B.3.9c) rather than the plain concave order (≤_cv) chunk 02c already needed for a different theorem — the two are genuinely different relations and must not be conflated.

Difficulty

The naive approach to the goal decouples the consumption and investment choices into two independent optimizations; the book's own proof shows they do separate at the level of the per-stage optimization (Theorem 4.3.6's proof: the transformed problem factors into a consumption fraction $\zeta$ and an investment fraction $\alpha$ optimized independently once the wealth scale is normalized out), but the admissible sets remain jointly constrained ($0\le c\le x$ interacts with the investable amount $x-c$), so treating them as literally independent unconstrained problems would silently solve an easier, different problem. For the regime-switching comparative statics (Theorem 4.4.5), the natural first attempt tries to prove monotonicity of $d_n(j)$ in $j$ directly from $Q_j\le_{\mathrm{icv}}Q_k$ alone; the book's own induction needs both hypotheses simultaneously (the environment chain's own stochastic monotonicity, governing how the regime itself evolves, and the return-distribution order, governing the one-period objective) — Theorem 4.4.4's monotonicity of $\alpha^*(j)$ handles the second factor of the induction's product (Eq. (4.22)) while the chain's stochastic monotonicity handles the first; dropping either hypothesis breaks the induction step.

Formalization scope

The consumption-investment vocabulary (ConsumptionInvestmentMarket, its value function, the one-period sub-problem) mirrors chunk 04a's pure-investment TerminalWealthMarket pattern exactly, extended to a joint $(c,a)$ action. The regime-switching model (RegimeSwitchingMarket) represents the finite regime set $E_Y$ abstractly (a Fintype with a row-stochastic transition matrix p : EY → EY → ℝ, not a PMF/product-measure construction on the joint disturbance): the book's own formula for $J_n^\pi$ is already a finite sum over the next regime of an integral against $Q_j$, so this is the direct, faithful representation and needs no additional measure-theoretic machinery — Jpi/J are built via an accumulator recursing through this finite-sum-of-integrals at each step (the natural generalization of chunk 04a's EFromToAcc pattern to a kernel that depends on an evolving state coordinate, rather than an exogenous process). Theorem 4.4.4/4.4.5 introduce LEIncreasingConcaveOrder (Definition B.3.9c) fresh, since chunk 02c's stochastic-order triple (≤_st/≤_cv/≤_cx) does not include the increasing-concave order this chunk's theorems actually use — reusing one of those three would silently substitute a different hypothesis, exactly the trap the chunk brief warns against. IsStochasticallyMonotoneChain (Definition B.3.13) is likewise restated fresh for a finite chain given by its transition matrix.

No trivializing formalization: D_n(x) is a genuine joint constraint on (c,a) (not two independent unconstrained choices); the six closed-form theorems (4.3.6, 4.3.7, 4.4.2, plus the comparative-statics pair) each state their own explicit recursion for $d_n$ — matching the brief's own note that the index-base convention is not uniform across them (Theorem 4.3.6 gives $d_N$ and recurses backward; Theorem 4.4.2 gives $d_0(j)$ and recurses forward) — encoded exactly as each theorem states it, not standardized to one direction.

Selected references

• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Universitext, Springer, 2011. https://doi.org/10.1007/978-3-642-18324-9
• J. D. Hamilton, "A new approach to the economic analysis of nonstationary time series and the business cycle", Econometrica, 1989 (the regime-switching framework §4.4 specializes to a portfolio-choice setting).

Motivation

Average-cost criteria are standard in inventory, queueing and maintenance models that run indefinitely. For a Markov decision process (MDP), the central object is the average-cost optimality equation (ACOE). It couples a constant $w$ (the optimal long-run cost per period) with a relative value function $\tilde u$. A stationary policy that attains the minimum in the ACOE is average-cost optimal. When the state space is uncountable, the one-step cost is unbounded and the transition probability is only weakly continuous, the ACOE is not automatically available.

Feinberg, Kasyanov and Zadoianchuk (2012) proved that under their Assumptions W* and B the weaker average-cost optimality inequality (ACOI) holds. For setwise continuous transition probabilities, Hernández-Lerma and Lasserre (1996, Theorem 5.5.4) gave conditions for the ACOE via equicontinuity. Feinberg and Lewis (2015) established the ACOI and optimality of $(s,S)$ policies for periodic-review inventory control with setup costs and general demand. Feinberg and Liang (2022, online 2017) extended the equicontinuity condition to weakly continuous transitions and used it to show that the inventory problem satisfies the full equation, not just the inequality.

Setting

An MDP has a state space $\mathbb X$ and an action space $\mathbb A$ (Borel subsets of Polish spaces). It has a one-step cost $c:\mathbb X\times\mathbb A\to\mathbb R\cup\{+\infty\}$, bounded below, and a transition probability $q(dy\mid x,a)$. A policy chooses actions from the observed history, possibly at random. A stationary policy is a measurable map $\phi:\mathbb X\to\mathbb A$. For a discount factor $\alpha\in[0,1)$:

• $v_\alpha(x)$ is the infimum over all policies of the expected total discounted cost from $x$;
• $m_\alpha=\inf_x v_\alpha(x)$;
• $u_\alpha=v_\alpha-m_\alpha$ is the discounted relative value function.

The average cost of a policy is $w^\pi(x)=\limsup_N \frac1N\mathbb E^\pi_x\sum_{t<N}c(x_t,a_t)$, and $w(x)=\inf_\pi w^\pi(x)$. Set $\underline w=\liminf_{\alpha\uparrow1}(1-\alpha)m_\alpha$. For a sequence $\alpha_n\uparrow1$, define

$$\tilde u(x)=\liminf_{n\to\infty,\ y\to x}u_{\alpha_n}(y).$$

Assumption EC for $\{\alpha_n\}$ has two parts:

1. the family $\{u_{\alpha_n}\}$ is equicontinuous;
2. some measurable $U\ge u_{\alpha_n}$ has $\int U\,dq(\cdot\mid x,a)<\infty$ for all $x,a$.

The inventory problem has inventory level $x\in\mathbb R$ (negative means backlog) and order quantity $a\ge0$. Inventory evolves by $x_{t+1}=x_t+a_t-D_{t+1}$, with i.i.d. nonnegative demands $D$. The cost is

$$c(x,a)=K\,I_{\{a>0\}}+\bar c\,a+\mathbb E[h(x+a-D)],$$

with setup cost $K\ge0$, unit cost $\bar c>0$, and convex $h$ with $h(x)\to\infty$ as $|x|\to\infty$. Let $\alpha^*=1+\lim_{x\to-\infty}h(x)/(\bar cx)$ and $H(x)=\bar cx+\mathbb E[h(x-D)]+\mathbb E[\tilde u(x-D)]$. A function $f$ is $K$-convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)+\lambda K$ for $x\le y$ and $\lambda\in(0,1)$. An $(s,S)$ policy orders up to $S$ whenever the inventory is below $s$.

Formalization targets

Goal: Theorem 4.5

For every sequence of nonnegative discount factors $\alpha_n\uparrow1$ with $\alpha_1>\alpha^*$, the inventory MDP satisfies Assumption EC. Along a subsequence, $u_{\alpha_{n_k}}\to\tilde u$, and some stationary $\phi$ satisfies

$$w+\tilde u(x)=K I_{\{\phi(x)>0\}}+H(x+\phi(x))-\bar cx=\min\Big\{\min_{a\ge0}[K+H(x+a)],\,H(x)\Big\}-\bar cx .$$

Moreover:

• $\tilde u$ and $H$ are $K$-convex, continuous and inf-compact;
• the $(s,S)$ policy built from a minimizer of $H$ satisfies the equation;
• so do the limits $(s^*,S^*)$ of discount-optimal thresholds.

Milestones

1. Lemma 3.3: for equicontinuous families, the pointwise and joint lower limits coincide.
2. Theorem 3.2: Assumptions W*, B and EC imply the ACOE for a general MDP.
3. The cited facts used in §4:
   • Assumptions W* and B hold for the inventory problem;
   • the sets $\mathbb X_\alpha$ of minimizers of $v_\alpha$ lie in a bounded interval (4.4);
   • discount-optimal $(s_\alpha,S_\alpha)$ policies (Theorem 4.3);
   • their average-cost limits (Theorem 4.4);
   • the renewal bounds (4.11)–(4.12).
4. Lemma 4.6: an explicit dominating function $U$.
5. Lemma 4.7: equicontinuity of $\{u_{\alpha_n}\}$ for the inventory problem.

Significance

The ACOE is stronger than the ACOI. It identifies the optimal actions of an average-cost problem as the minimizers of a one-step lookahead with $\tilde u$, and it makes $\tilde u$ a genuine relative value function: $\tilde u$ is the pointwise limit of the discounted relative values along a subsequence. For inventory control, Theorem 4.5 gives three further conclusions:

• the $K$-convexity and continuity of the average-cost relative value function;
• that an optimal $(s,S)$ policy can be computed from $H$ by the same argmin rule that works for discounted costs;
• that limits of discount-optimal thresholds solve the average-cost problem.

The results are proved in the paper, and in the cited works of Feinberg and coauthors for the cited milestones. None is formalized. There is no formal library of MDPs on Borel spaces with history-dependent randomized policies. This mission builds that layer (strategic measures via Ionescu Tulcea, discounted and average costs, Assumptions W*, B and EC) and states the general ACOE theorem on it. A proof of the goal would also require formal proofs of the cited inventory results of Feinberg–Lewis (2015) and Feinberg–Liang (2017a), which are milestones here.

Difficulty

One obvious route is to pass to the limit in the discounted optimality equation $v_\alpha=\min_a[c+\alpha\int v_\alpha\,dq]$. After subtracting $m_\alpha$, this needs two things: convergence of $u_{\alpha_n}$, and exchanging limit and integral. Pointwise lower limits give only the inequality (ACOI). The reverse inequality needs actual convergence of a subsequence and a dominating function. For weakly continuous $q$, convergence of $\int u_{\alpha_n}\,dq$ additionally requires uniform convergence on compacts, which is where equicontinuity enters.

For the inventory problem the hard step is equicontinuity itself. The functions $u_\alpha$ are not uniformly Lipschitz. It must be shown that costs from two nearby starting inventories stay close uniformly in $\alpha$. This comparison runs through the time until inventory falls below the reorder point, and it is controlled by renewal-theoretic bounds on the number of demand arrivals.

Formalization scope

The Lean development lives in the namespace FeinbergLiang.ACOE. It commits to the following conventions.

• Spaces. $\mathbb X,\mathbb A$ are separable metric spaces with standard Borel σ-algebras. This is the paper's "Borel subsets of Polish spaces", up to homeomorphism. The inventory case is $\mathbb X=\mathbb R$, $\mathbb A=\mathbb R_{\ge0}$. The integer case $\mathbb X=\mathbb Z$, $\mathbb A=\mathbb N_0$ is out of scope, as are Corollary 4.8 and Theorem 4.9.
• Costs and infinities. The cost is stored as a real lower bound plus a $[0,\infty]$-valued part. Every value function ($v_\alpha$, $m_\alpha$, $u_\alpha$, $w$, $\underline w$, $\tilde u$) is the $[0,\infty]$-valued part, with the explicit real shift described in the definitions. $u_\alpha$ equals $v_\alpha-m_\alpha$ whenever $m_\alpha<\infty$, which Assumption B guarantees. $\alpha^*$ is an extended real and may be $-\infty$. $G_\alpha$ and $H$ are extended-real valued, and each theorem using them concludes their finiteness. Likewise the ACOE conclusions include $\underline w<\infty$ and $\tilde u<\infty$, so an equation of the form $\infty=\infty$ can never satisfy them.
• Policies. $v_\alpha$ and $w$ are infima over all history-dependent randomized policies, with trajectory laws given by Mathlib's Ionescu Tulcea kernel Kernel.trajMeasure. They are never defined as solutions of an optimality equation.
• Readings of informal words.
  1. "$\alpha_n\uparrow1$" means values in $[0,1)$, nondecreasing, with limit $1$; "nonnegative discount factors" is the lower end of $[0,1)$.
  2. The paper's $\alpha_1$ is Lean's α 0.
  3. "Equicontinuous" is Mathlib's Equicontinuous, applied to the real values of $u_{\alpha_n}$ together with their finiteness.
  4. "$\liminf_{n\to\infty,y\to x}$" is the lower limit along the product filter atTop ×ˢ 𝓝 x.
  5. "Uniform on each compact subset" is TendstoUniformlyOn on every compact set.
  6. "$=\min$" in (3.3) and (4.10) means the middle term is attained and is a lower bound for all actions.
  7. "Assumption EC for the sequence" is a property of a given sequence.
  8. "Can be selected as an $(s^*,S^*)$ policy" is stated for every limit of discount-optimal thresholds along a further subsequence, with $\tilde u$ that of Theorem 3.2(i).
  9. "Can be selected as an $(s,S)$ policy" is stated for every minimizer $S$ of $H$.
  10. Theorem 4.4's "optimality inequality (4.8)" is read as the ACOI (3.1) for the $(s^*,S^*)$ policy.
• Standing assumptions. The paper's "without loss of generality $h\ge0$ and $h(0)=0$" is a pair of hypotheses of the inventory model. This is the paper's normalization, not an addition.
• Not trivializable. Defining $v_\alpha$ through its optimality equation, restricting policies to stationary ones, or dropping the finiteness conclusions would make the goal a different, weaker statement. The definitions rule each of these out.

Contributions welcome: proofs of the milestones, especially the general Theorem 3.2 and the renewal estimates behind Lemmas 4.6–4.7. The Borel-space MDP definitions are reusable by later average-cost and discounted MDP missions.

Selected references

• E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control, Annals of Operations Research 317 (2022) 569–586. https://doi.org/10.1007/s10479-017-2561-9
• E. A. Feinberg, P. O. Kasyanov and N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probability, Mathematics of Operations Research 37(4) (2012) 591–607. https://doi.org/10.1287/moor.1120.0555
• E. A. Feinberg and M. E. Lewis, On the convergence of optimal actions for Markov decision processes and the optimality of (s, S) policies for inventory control, preprint arXiv:1507.05125, 2015. https://arxiv.org/abs/1507.05125
• E. A. Feinberg and Y. Liang, Structure of optimal policies to periodic-review inventory models with convex costs and backorders for all values of discount factors, Annals of Operations Research (2017a). https://doi.org/10.1007/s10479-017-2548-6
• O. Hernández-Lerma and J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0

Motivation

Markowitz's mean-variance problem trades off the expected terminal wealth of a portfolio against its risk. Over several periods the scalarized form of this problem is time inconsistent: a strategy that is optimal today for a fixed risk-aversion parameter is generally no longer optimal tomorrow for the same parameter, so the investor would deviate from her own plan (Björk & Murgoci 2014; Björk, Murgoci & Zhou 2014). The literature has responded by redefining optimality (equilibrium strategies) or by searching for a time- and state-dependent risk aversion that restores consistency (Karnam, Ma & Zhang, Annals of Applied Probability 27, 2017). Dynamic convex risk measures and their time consistency are developed in Detlefsen & Scandolo 2005 and Riedel 2004.

Kováčová and Rudloff (arXiv:1806.10981, Operations Research 2021) take a different route. They keep both objectives, measure risk by a time consistent dynamic convex risk measure, and treat the dynamic mean-risk problem as a family of vector optimization problems. They show that this family is time consistent with respect to weak minimizers and that its value functions, the upper images, satisfy a set-valued Bellman principle. This mission formalizes that Bellman principle.

Setting

Fix a horizon $T$ and a finite probability space $(\Omega,\mathcal F,\mathbb P)$ with a filtration $(\mathcal F_t)_{t=0}^T$, $\mathcal F_0$ trivial, $\mathcal F_T=\mathcal F$, and $\mathbb P(A)>0$ for every nonempty event $A$. $L_t(D)$ denotes the $\mathcal F_t$-measurable random vectors with values in $D$; orders between random vectors are pointwise and componentwise.

A market has $d$ assets with adapted discounted prices $S_s\in L_s(\mathbb R^d)$. An investor holds positions $\psi_s\in L_s(\mathbb R^d)$ on $[s,s+1)$, subject to closed, conditionally convex constraint sets $\Phi_s\subseteq L_s(\mathbb R^d)$. With wealth $v_t\in L_t$ at time $t$, the feasible portfolios are

$$\Psi_t(v_t)=\{(\psi_s)_{s=t}^{T-1}\mid S_t^\top\psi_t=v_t,\ \psi_t\in\Phi_t,\ S_s^\top\psi_{s-1}=S_s^\top\psi_s,\ \psi_s\in\Phi_s,\ s=t+1,\dots,T-1\},$$

that is, self-financing strategies with initial value $v_t$ that respect the constraints. The terminal wealth is $v_T=S_T^\top\psi_{T-1}$ and $V_T(\psi)=(v_T,v_T)$.

Risk is measured by a dynamic convex risk measure $(\rho_t)_{t=0}^T$: each $\rho_t:L_T\to L_t$ is normalized, conditionally translation invariant, monotone (decreasing) and conditionally convex. It is time consistent: $\rho_{t+1}(X)=\rho_{t+1}(Y)$ implies $\rho_t(X)=\rho_t(Y)$. The mean-risk function is

$$\Gamma_t(X)=\big(-\mathbb E_t(X_1),\ \rho_t(X_2)\big),\qquad X\in L_T(\mathbb R^2),$$

and the mean-risk problem $D_t(v_t)$ minimizes $\Gamma_t(V_T(\psi))$ over $\psi\in\Psi_t(v_t)$ with respect to the cone $L_t(\mathbb R^2_+)$. Its upper image is

$$\mathcal P_t(v_t)=\operatorname{cl}\big(\Gamma_t(\Psi_t(v_t))+L_t(\mathbb R^2_+)\big),\qquad t<T,$$

and at the terminal time $\mathcal P_T(v_T)=\{(-v_T,-v_T)\}+L_T(\mathbb R^2_+)$ (5.2).

Formalization targets

Goal: Theorem 5.1 (set-valued Bellman equation)

For every $t=0,\dots,T-1$ and every $\mathcal F_t$-measurable $v_t$,

$$\mathcal P_t(v_t)=\operatorname{cl}\left\{\Gamma_t(-x)\ \middle|\ S_t^\top\psi_t=v_t,\ \psi_t\in\Phi_t,\ x\in\mathcal P_{t+1}\big(S_{t+1}^\top\psi_t\big)\right\}.$$

The right side has a closure and no ordering cone.

Milestones

1. Lemma 2.1 (second and third bullets): time consistency is equivalent to recursiveness $\rho_t(X)=\rho_t(-\rho_{t+1}(X))$; a convex risk measure on a finite space is continuous.
2. Lemma 3.1: $\psi\in\Psi_t(v_t)$ iff $S_t^\top\psi_t=v_t$, $\psi_t\in\Phi_t$ and $(\psi_s)_{s\ge t+1}\in\Psi_{t+1}(S_{t+1}^\top\psi_t)$.
3. Lemma B.1: $\Gamma_t$ is conditionally translation invariant, monotone, conditionally convex, recursive ($\Gamma_t(X)=\Gamma_t(-\Gamma_{t+1}(X))$), local and continuous; upper images are monotone with respect to their cone.
4. Lemma B.2: $\Gamma_t(\Psi_t(v_t))$ equals the image of the auxiliary problem $\bar D_t(v_t)$, in which $x$ ranges over $\Gamma_{t+1}(\Psi_{t+1}(S_{t+1}^\top\psi_t))$.
5. Lemma 5.2: the upper image $\tilde{\mathcal P}_t(v_t)$ of the one-time-step problem $\tilde D_t(v_t)$, in which $x$ ranges over $\mathcal P_{t+1}(S_{t+1}^\top\psi_t)$, equals $\mathcal P_t(v_t)$.

Significance

The upper image is the infimum of $D_t(v_t)$ in the complete lattice of closed upper sets, so it is the natural value function of a vector optimization problem. Theorem 5.1 expresses the value function at time $t$ through the value functions at time $t+1$ by a one-period problem, exactly as a scalar Bellman equation does. Computationally this is what makes the problem tractable: one solves a convex one-period vector optimization problem per node, backwards in time, and recovers the whole efficient frontier at every node and an efficient strategy forward along the realized path (Sections 6 and 7 of the paper do this for 2,500 periods). Conceptually, it shows that the mean-risk problem is time consistent in the set-valued sense without computing the moving scalarization in advance.

The paper proves Theorem 5.1; no machine-checked version exists. Formalizing it produces a Lean development of dynamic convex risk measures on finite filtrations, of conditional vector optimization in $L_t(\mathbb R^2)$, and of upper images, none of which is currently on the platform beyond the static conditional convex risk measure reused here.

Difficulty

The equality has two halves of different character. Replacing the image $\Gamma_{t+1}(\Psi_{t+1})$ by the upper image $\mathcal P_{t+1}$ enlarges the feasible set of the one-period problem, and the new points must be shown to be limits of points already attained: this needs monotonicity of $\Gamma_t$ together with its continuity, which holds only because $\Omega$ is finite. Removing the cone from the right-hand side needs translation invariance of $\Gamma_t$ with an $\mathcal F_t$-measurable shift and the monotonicity of $\mathcal P_{t+1}$ with respect to the larger cone $L_{t+1}(\mathbb R^2_+)$. Both closures matter: without them the identity fails in general, since the image of a closed set under $\Gamma_t$ need not be closed. The natural first idea, to define $\mathcal P_t$ recursively, proves nothing: the content of the theorem is that the upper image built from whole multi-period strategies agrees with the recursion.

Formalization scope

• $\Omega$ is a Fintype with an ambient σ-algebra $\mathcal F$; the filtration is a Mathlib Filtration ℕ with $\mathcal F_T=\mathcal F$ and $\mathcal F_0=\bot$; $\mathbb P$ is a probability measure with $\mathbb P(A)>0$ for every nonempty measurable $A$.
• Each $\rho_t$, $t\le T$, satisfies the published CondConvexRisk.Representation.IsCondConvexRiskMeasure with respect to $\mathcal F_t$ (axioms a.s. on $L^\infty$); time consistency is stated pointwise for measurable arguments. On a finite space with positive probabilities, a.s. equality of measurable functions is equality, so all of the mission's own statements are pointwise.
• Random vectors in $\mathbb R^2$ are functions $\Omega\to\mathbb R\times\mathbb R$; the cone $L_t(\mathbb R^2_+)$ is the set of nonnegative $\mathcal F_t$-measurable ones; closures are in the product topology. $\mathbb E_t$ is Mathlib's condExp.
• Strategies are sequences indexed by $\mathbb N$; only the indices $t,\dots,T-1$ are constrained or read.
• Assumption 2.2 item 3 ($\Psi_0(v_0)\neq\emptyset$) is not assumed by any statement; Theorem 5.1 holds for empty feasible sets as well.
• $\mathcal P_t$ for $t<T$ is the closure of the image of whole strategies plus the cone; only $\mathcal P_T$ is given by (5.2). A recursive definition of $\mathcal P_t$, or a cone on the right of (5.1), would make the goal trivial or turn it into Lemma 5.2, and is ruled out.
• Not formalized here: Theorem 3.2 (time consistency w.r.t. weak minimizers), the scalarization results of §4, the coherent case of §6, and the node-wise algorithms of Appendix A.

A complete development needs: conditional expectation on finite filtrations (tower property, pull-out of $\mathcal F_t$-measurable factors), continuity of convex functions on finite-dimensional spaces, and elementary closure arguments in $\Omega\to\mathbb R\times\mathbb R$. The results on dynamic risk measures (Lemma 2.1) and on $\Gamma_t$ (Lemma B.1) are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• G. Kováčová, B. Rudloff, Time consistency of the mean-risk problem, Operations Research, 2021. Preprint arXiv:1806.10981v2. https://arxiv.org/abs/1806.10981
• A. H. Hamel, F. Heyde, A. Löhne, B. Rudloff, C. Schrage, Set optimization — a rather short introduction, in Set Optimization and Applications, Springer, 2015. https://doi.org/10.1007/978-3-662-48670-2_3
• A. Löhne, Vector Optimization with Infimum and Supremum, Springer, 2011. https://doi.org/10.1007/978-3-642-18351-5
• K. Detlefsen, G. Scandolo, Conditional and dynamic convex risk measures, Finance and Stochastics 9(4), 2005. https://doi.org/10.1007/s00780-005-0159-6
• F. Riedel, Dynamic coherent risk measures, Stochastic Processes and their Applications 112(2), 2004. https://doi.org/10.1016/j.spa.2004.03.004
• T. Björk, A. Murgoci, A theory of Markovian time-inconsistent stochastic control in discrete time, Finance and Stochastics 18(3), 2014. https://doi.org/10.1007/s00780-013-0227-1
• T. Björk, A. Murgoci, X. Y. Zhou, Mean-variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• C. Karnam, J. Ma, J. Zhang, Dynamic approaches for some time-inconsistent optimization problems, Annals of Applied Probability 27, 3435–3477, 2017.

Motivation

Firms that develop technology in generations face a recurring choice: sell the product they already have, or hold it back while the next generation is developed. Selling it earns revenue now, but once the advanced product arrives, the earlier product cannibalizes part of its market. An established firm makes this choice by weighing development risk against cannibalization. A cash-constrained start-up faces a third pressure: it can only keep developing while it can pay for development, and selling the on-hand product is also a way to finance the next period.

Bhaskaran, Erzurumlu and Ramachandran (SSRN 3255345; Manufacturing & Service Operations Management, doi:10.1287/msom.2020.0895) model both firms as infinite-horizon dynamic programs and compare their optimal strategies. For the established firm, the answer is governed by two thresholds on the per-period probability of development success. For the start-up, the paper relates its strategy to the same thresholds and to its cash. This mission formalizes the start-up's strategy in the low and intermediate success-probability regimes, together with the established-firm benchmark it is built on.

Setting

A firm holds an on-hand product that pays $v_o$ per period once launched, and develops an advanced product that pays $v_a \ge v_o$ per period once developed. Each period of development costs $c > v_o$ and succeeds with probability $p$. Payoffs are discounted by $\delta \in (0,1)$, so the lifetime values are $V_o = v_o/(1-\delta)$ and $V_a = v_a/(1-\delta)$. If the advanced product is launched after the on-hand product, it earns only $(1-\alpha)v_a$ per period, where $\alpha \in [0,1]$ is the cannibalization factor.

In each period the firm chooses among three actions: launch the on-hand product and stop development (LS), launch it and continue development (LC), or defer its launch and continue development (DC). Once the on-hand product is launched, only LS and LC remain.

Established firm. Its values $\Pi_0$ (on-hand product not yet launched) and $\Pi_1$ (launched) satisfy equations (1)–(2):

$$\Pi_0 = \max\{\Pi_{LS},\Pi_{LC},\Pi_{DC}\},\qquad \Pi_1 = \max\{\Pi_{LS},\Pi_{LC}\},$$

with $\Pi_{LS} = V_o$, $\Pi_{LC} = v_o - c + p(1-\alpha)\delta V_a + (1-p)\delta\Pi_1$ and $\Pi_{DC} = -c + p\,\delta V_a + (1-p)\delta\Pi_0$.

Start-up. It holds cash $E$, and unused cash earns interest at rate $(1-\delta)/\delta$. After a period of development, its cash is $E_D = (E-c)/\delta$ if it deferred the launch and $E_L = (E+v_o-c)/\delta$ if it launched. Its value functions $R_0, R_1$ of the cash level satisfy equations (3)–(5):

$$R_0(E) = \max\{R_{LS}(E), R_{DC}(E), R_{LC}(E)\},\qquad R_1(E) = \max\{R_{LS}(E), R_{LC}(E)\},$$ $$R_{LS}(E) = E + V_o,\qquad R_{LC}(E) = p\bigl(E + v_o - c + \delta(1-\alpha)V_a\bigr) + (1-p)\delta R_1(E_L),$$

and $R_{DC}(E) = p(E - c + \delta V_a) + (1-p)\delta R_0(E_D)$ when $E \ge c$, and $R_{DC}(E) = E$ when $E < c$.

The established firm's thresholds $p_1 \le p_2$ (Proposition 1) are defined by its strategy: launch and stop for $p \le p_1$, launch and continue for $p_1 < p \le p_2$, and defer and continue for $p > p_2$.

Formalization targets

Goal: Proposition 2 (i)–(ii)

For every cash level $E \ge 0$:

1. if $p < p_1$ or $c > E + v_o$, then launching and stopping is strictly optimal:

$$R_0(E) = R_{LS}(E) > \max\{R_{DC}(E),\,R_{LC}(E)\};$$

2. if $p_1 \le p < p_2$ and $c < E + v_o$, then launching and continuing is optimal, and continuing stays optimal after the launch at every funded cash level:

$$R_0(E) = R_{LC}(E),\qquad R_1(E') = R_{LC}(E')\ \text{ whenever } c \le E' + v_o .$$

Milestones

• the value functions $\Pi_I$ and $R_I$ exist and are unique;
• Proposition 1 (i)–(iii): thresholds $p_1 \le p_2$ exist;
• Lemma 1(i): if $p < p_1$, then $R_{LS}(E) > \max[R_{DC}(E), R_{LC}(E)]$ for all $E > 0$;
• Lemma 1(ii), corrected: if $p_1 < p_2$, $p > p_1$ and $c \le E + v_o$, then $R_{LC}(E) > R_{LS}(E)$;
• the corrected limit claim of the proof of Proposition 2(ii): $R_1(E) = E + \Pi_1$ for $E \ge (c-v_o)/(1-\delta)$ and $R_0(E) = E + \Pi_0$ for $E \ge c/(1-\delta)$.

Significance

Proposition 2 answers the managerial question the paper poses: a cash-constrained start-up should behave like the established firm when development is unlikely to succeed, and must stop when it cannot fund the current period. In the intermediate regime it, too, should launch the on-hand product and keep developing. The established firm's thresholds of Proposition 1 therefore also organize the start-up's decision, and the start-up's cash enters only through whether development can be funded.

The paper also states a third part: above $p_2$, a cash threshold $\bar E_L$ below which the start-up launches. This part is false: with $v_o = 6/5$, $v_a = 6$, $c = 24/5$, $\delta = 15/16$, $\alpha = 27/100$ and $p = 8/25 > p_2 = 1/12$, deferring is strictly optimal at $E = 6$ and $E = 9$ and launching at $E = 7$. Lemma 2, the route the paper takes to (iii), fails for the same instance. Lemma 1(ii) as printed also fails: when $p_1 = p_2$, launching and continuing need not beat launching and stopping. The mission states the corrected forms, so a machine-checked proof here settles exactly which parts of the characterization hold. No part of this paper has a machine-checked proof.

Difficulty

The start-up's equations are a functional fixed-point problem in which the action sets depend on the state: the defer option changes form at $E = c$ and launching-and-continuing requires $c \le E + v_o$, so $R_0$ and $R_1$ have jumps. Comparisons between actions therefore cannot be read off a single closed form. They must hold uniformly along the cash trajectories $E \mapsto E_D$ and $E \mapsto E_L$, which shrink below the interest break-even and grow above it.

The paper's own argument for (ii) goes through Lemma 2, a single-crossing property of $R_{DC} - R_{LC}$ in the cash level, and that property is false. A proof of (ii) must instead show directly that deferral never beats launch-and-continue below $p_2$, at every cash level, including those where the start-up can afford only a few periods of development. The threshold $p_1$ itself is defined by the established firm, so one must also relate the start-up's finite-horizon comparisons to the established firm's infinite-horizon ones.

Formalization scope

Everything is real-valued. The expectations in (1)–(5) are explicit two-outcome sums, and no probability or MDP library is used. The parameters form a structure with the standing assumptions $0 < v_o \le v_a$, $v_o < c$, $0 < \delta < 1$ and $0 \le \alpha \le 1$, and $p \in [0,1]$. The paper allows $\delta = 1$, but $V_o$ needs $\delta < 1$; $v_o > 0$ is also assumed.

• Value functions are hypothesized solutions. Every theorem quantifies over all solutions $(\Pi_0,\Pi_1)$ of (1)–(2) and all solutions $(R_0,R_1)$ of (3)–(5). A milestone states that each system has exactly one solution, so these statements are neither vacuous nor about different objects.
• The start-up's equations hold at every real $E$. Launching and continuing is available only when $c \le E + v_o$; otherwise $R_1(E) = R_{LS}(E)$. Printed (4) says "when $E_t > c$"; the funded reading is the one Lemma 1(iii) and Proposition 2(i) use. Lemma 1(iii) holds by definition under this reading and is not a milestone.
• Bounded selection. Above the interest break-even the recursion never terminates and (3)–(5) admit spurious unbounded solutions. The value function is selected by requiring $R_0(E) - E$ and $R_1(E) - E$ to be bounded.
• Thresholds by behaviour. $p_1, p_2$ are any pair inducing Proposition 1's strategy on $q \in [0,1]$, normalized so that $p_1 \le 1$ and $p_2 = 1$ when $p_1 = 1$. They are never defined by the proof's closed forms, whose printed $p_C$ is wrong. The strategies are "attains the maximum in every solution", which is correct at the tie points $q = p_1$, $q = p_2$.

Trivializing formalizations are ruled out: $R_0$ and $R_1$ are not given by closed forms, launch-and-continue is not available without funding, (i) asserts strict optimality, and (ii) asserts continuation at every later funded cash level, not only at the current one.

Not formalized: Proposition 1(iv) (comparative statics of $p_1, p_2$), Proposition 2(iii) and Lemma 2 (false), Propositions 3–6 (built on the threshold $\bar E_L$ or on approximations), and the extensions of §5. Contributions welcome: proofs of the milestones. The well-posedness milestone concerns a generic two-state discounted recursion with a state-dependent action set, and its proof is reusable beyond this paper.

Selected references

• S. Bhaskaran, S. S. Erzurumlu, K. Ramachandran, Sequential product development and introduction by cash-constrained start-ups, Manufacturing & Service Operations Management, 2020 (manuscript of February 2020). https://ssrn.com/abstract=3255345, https://doi.org/10.1287/msom.2020.0895

Inventory control when stock is seen only at zero

In many retail settings, recorded inventory is not reliable. Shrinkage, misplacement and recording errors mean the shelf count is unknown, but a stock-out is visible. Bai, Chen and Stolyar (SSRN 3865728; Operations Research Technical Note, 2022, doi:10.1287/opre.2022.2305) study the extreme version of this: a single-item lost-sales system whose inventory level is observed only when it is zero.

For the discounted cost criterion, Bensoussan, Çakanyıldırım and Sethi (2007) showed that optimal feedback policies exist for this model. Whether a stationary policy minimizes the long-run average cost was left open. Average-cost problems for partially observable systems are harder because of the vanishing-discount argument they rely on. It needs a uniform bound on relative value functions, and on a space of beliefs such bounds are not automatic. The paper settles the question for this model.

Setting

In each period $t$ the inventory level is $x_t\in\mathbb R_+$. The decision maker orders $a_t\in\mathbb A=[0,K]$, with $K>0$. The order arrives at once and ordering costs nothing. Then an i.i.d. demand $D_t\sim D$ is realized, and unmet demand is lost:

$$x_{t+1}=(x_t+a_t-D_t)^+ .$$

The period cost is the holding and lost-sales cost $h^+(x_t+a_t-D_t)^+ + h^-(x_t+a_t-D_t)^-$, with $h^+,h^->0$. Its expectation given $(x,a)$ is $c(x,a)$. The demand $D$ is nonnegative, has a density $f$ with distribution function $F$, a finite positive mean and a positive variance.

Only the signal $y_t=\mathbf 1\{x_t>0\}$ is observed. The decision maker therefore acts on a belief $z$, the conditional distribution of the current inventory level. After ordering $a$ from belief $z$, the next belief is $\delta_0$ if $y=0$. If $y=1$ it is the posterior $H(z,a,1)$, the law of $(x+a-D)^+$ (with $x\sim z$) conditioned on being positive. The probability of $y=1$ is $R(1\mid z,a)$.

This yields a completely observable MDP (COMDP). Its states are beliefs with finite second moment, $\int x^2\,z(dx)<\infty$ (Assumption 1), taken with the topology of weak convergence. Its cost is $\bar c(z,a)=\int c(x,a)\,z(dx)$ and its transition kernel is

$$q(\cdot\mid z,a)=R(0\mid z,a)\,\delta_{\delta_0}+R(1\mid z,a)\,\delta_{H(z,a,1)}.$$

For a policy $\pi$, $v^\pi_\alpha$ is its $\alpha$-discounted cost and $w^\pi$ its average cost per period (a $\limsup$). The optima are $v_\alpha=\inf_\pi v^\pi_\alpha$ and $w=\inf_\pi w^\pi$ over all history-dependent randomized policies. Write $m_\alpha=\inf_z v_\alpha(z)$, $u_\alpha=v_\alpha-m_\alpha$ and $w^*=\inf_z w(z)$.

Formalization targets

Goal: Theorem 1 (p. 9)

There are a sequence $\alpha_n\uparrow 1$ and a measurable stationary policy $\varphi$ that is average-cost optimal among all policies. With $w^*$ finite and

$$u(z)=\liminf_{n\to\infty,\ s\to z}u_{\alpha_n}(s)$$

finite, $\varphi$ satisfies the average cost optimality inequality (ACOI)

$$w^*+u(z)\ \ge\ \bar c(z,\varphi(z))+\int u(s)\,q(ds\mid z,\varphi(z))\qquad\text{for every belief }z .$$

Milestones, in attack order

1. §3.1, p. 10. $q$ is a measurable stochastic kernel, so the COMDP exists.
2. Lemma 3, p. 12. Assumption B(i): $w^*<\infty$.
3. §3.2, p. 12. Assumption (W*): $\bar c$ is $\mathbb K$-inf-compact and $q$ is weakly continuous.
4. Lemma 2, p. 12 (Feinberg 2016, for a general MDP on Borel spaces). Under (W*) and (B), $w^*=\lim_{\alpha\uparrow1}(1-\alpha)v_\alpha$, and a stationary average-cost optimal policy satisfies the ACOI.
5. Lemma 4, p. 14. For two inventory paths started at $x'\ge x\ge 0$, sharing demands and an arbitrary control rule $\zeta$: $V^\zeta_\alpha(x)-V^\zeta_\alpha(x')\le h^-(x'-x)-\mathbf 1\{x'-x\ge C\}h'(x'-x)\le h^-C$, with $C,\alpha_*,h'>h^-$ uniform.
6. Display (12), corrected, pp. 13–14. $v_\alpha(\delta_0)-v^\pi_\alpha(z')\le\bar C$, uniformly in $\alpha\in[\alpha_*,1)$, in beliefs $z'$ and in stationary $\pi$. The paper prints $v^\pi_\alpha(\delta_0)$ as the first term. Its proof bounds the cost of a different policy (the "pursuing" policy) started at $\delta_0$, and the derivation of (11) uses the optimal value. The printed form, with the same $\pi$ at $\delta_0$, is not what the proof establishes.
7. Display (11), p. 13. $\sup_{\alpha\in[\alpha_*,1)}u_\alpha(\delta_0)<\infty$.
8. Theorem 2, p. 13. Assumption B(ii): $\sup_{\alpha\in[\alpha_*,1)}u_\alpha(z)<\infty$ for every belief $z$.

Significance

Theorem 1 gives existence of a stationary average-cost optimal policy for a partially observed inventory system with lost sales. In that setting the belief space is infinite-dimensional and the state is never fully revealed except at zero. The ACOI also supplies the structure needed to study such a policy. The paper leaves open whether the ACOE (the equality form) holds.

The reduction is reusable. Feinberg's general conditions, (W*) and (B), apply to many belief MDPs. The problem-specific work is the uniform bound B(ii), obtained here through a coupling estimate (Lemma 4) for lost-sales paths under arbitrary, even anticipating, controls.

The paper proves Theorem 1, Theorem 2, Lemma 3 and Lemma 4. Lemma 2 and the (W*) claim are cited from Feinberg (2016) and Feinberg, Kasyanov and Zgurovsky (2016) and are not proved in the paper. As far as is known, none of these results has a machine-checked proof; the general vanishing-discount theory for MDPs on Borel spaces is itself not yet formalized.

Difficulty

The obvious route to B(ii) compares $v_\alpha(z)$ with $v_\alpha(\delta_0)$ by running from $z$ the policy that is optimal from $\delta_0$. This fails: a policy is a function of the belief, and the beliefs generated from $z$ and from $\delta_0$ differ, so the same policy produces different orders. The paper goes the other way and bounds $v_\alpha(\delta_0)$ above by $v^\pi_\alpha(z')+\bar C$. This needs a policy started from $\delta_0$ that mimics $\pi$'s orders while the two systems have not yet merged. The constant must be uniform in $\alpha$ close to $1$, so per-period estimates that grow like $1/(1-\alpha)$ are useless.

The (W*) claim has its own difficulty. The observation kernel $\mathbf 1\{x>0\}$ is discontinuous at $0$, so the known criterion for weak continuity of belief kernels, which needs observations continuous in total variation, does not apply. Continuity has to come from the density of $D$.

Formalization scope

The Lean development lives in the namespace PartialLostSales.ACOI. It reuses the published FeinbergLiang.ACOE layer: MDP, history-dependent randomized Policy, vDisc, vOpt, avgCost, wOpt, IsAvgOptimal, uRel, uTilde, IsDiscountSeq, KInfCompact and AssumptionWStar. All costs and values lie in $[0,\infty]$. Its conventions are:

• Spaces. Inventory lives in ℝ≥0 with the Euclidean topology, and actions in the subtype $[0,K]$.
• Beliefs. Beliefs form the subtype of ProbabilityMeasure ℝ≥0 with finite second moment. They carry the weak topology and Mathlib's (Giry) σ-algebra, which is the Borel σ-algebra here.
• COMDP. "The COMDP" is any MDP satisfying IsCOMDP, which pins the lower bound $0$, the cost $\bar c$ and the kernel $q$ pointwise; milestone 1 shows one exists.
• Assumption (B). It is the paper's version, with $\sup$ over $[\alpha_*,1)$.
• Policies. "Stationary" means a measurable map from beliefs to actions.

The paper states that COMDP and POMDP policies correspond with equal values (Feinberg, Kasyanov and Zgurovsky 2016). The goal is stated in the COMDP, and that equivalence is not formalized.

Added hypotheses. Demand is nonnegative. Lemma 4's control rule is measurable, but adaptedness is not required.

Totality devices. The posterior when $R(1\mid z,a)=0$, and the map of a posterior back into the belief subtype, have else branches that are never used.

Indexing. Lemma 4 indexes periods from $0$ with weight $\alpha^t$. Its costs are realized costs, since controls may anticipate.

Trivializing formalizations. Several encodings would make statements trivial, and none is used. The kernel and cost of the MDP are never left free. The ACOI carries explicit finiteness of $w^*$ and $u$, so it is not an $[0,\infty]$ inequality that holds when $u=\infty$. Optimality is over all policies, not only stationary ones. The ACOI uses $w^*$, not $\limsup(1-\alpha)m_\alpha$ or a free constant.

Not formalized.

• Lemma 1, already open on the platform as FKZAvg.WStar.theorem_2 (v).
• Theorem 3, p. 20, and the pursuing-policy construction of §4.1.
• The POMDP–COMDP equivalence.
• The extensions of §5.

Contributions of general value include Feinberg's average-cost theory on Borel spaces (Lemma 2) and weak continuity of belief kernels with discontinuous observations.

Selected references

• X. Bai, X. Chen, A. L. Stolyar, Average Cost Optimality in Partially Observed Lost-Sales Inventory Systems, SSRN preprint 3865728; Operations Research Technical Note, 2022. https://ssrn.com/abstract=3865728, https://doi.org/10.1287/opre.2022.2305
• E. A. Feinberg, Optimality conditions for inventory control, in Optimization Challenges in Complex, Networked and Risky Systems (INFORMS TutORials in Operations Research), 14–45, 2016. https://doi.org/10.1287/educ.2016.0145
• E. A. Feinberg, P. O. Kasyanov, M. Z. Zgurovsky, Partially observable total-cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 41(2), 2016. https://doi.org/10.1287/moor.2015.0746
• E. A. Feinberg, P. O. Kasyanov, N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probabilities, Mathematics of Operations Research 37(4), 2012. https://doi.org/10.1287/moor.1120.0555
• A. Bensoussan, M. Çakanyıldırım, S. P. Sethi, Partially observed inventory systems: the case of zero-balance walk, SIAM Journal on Control and Optimization 46(1), 2007. https://doi.org/10.1137/040620321