Dynamic Programming

Markov policies in continuous-time decision processes

In a Markov decision process a controller chooses actions over time to influence a random system. A basic question for every such model is whether the controller loses anything by ignoring the past: whether, for every policy that uses the full history, some Markov policy (one that looks only at the current state and time) performs equally well. For discrete-time models the answer goes back to Derman and Strauch (1966): the Markov policy that randomizes according to the conditional distribution of the action given the current state has the same state-action marginals as the original policy, and therefore the same expected costs for any criterion that depends on these marginals.

In continuous-time jump Markov decision processes (CTJMDPs) with unbounded transition rates the question is harder, because the process may explode: infinitely many jumps can accumulate in finite time, after which the process leaves the state space. Earlier sufficiency results assumed bounded rates or nonexplosive processes (Kitaev 1985; Kitaev and Rykov 1995; Guo and Song 2011; Piunovskiy and Zhang 2014). Feinberg, Mandava and Shiryaev (arXiv:2003.01342) proved the continuous-time analogue of Derman and Strauch's result with no such assumption: the induced Markov policy has state-action marginals no larger than those of the original policy, and equal ones as long as it does not explode.

Setting

A CTJMDP is given by a state space $X$ and an action space $A$, both standard Borel spaces; nonempty sets $A(x)\subseteq A$ of actions available at each state $x$, whose graph $\mathrm{Gr}(A)$ is measurable and contains the graph of a measurable selector; and transition rates $\tilde q(x,a,\cdot)$, where $Z\mapsto\tilde q(x,a,Z\setminus\{x\})$ is a finite measure, measurable in $(x,a)$. The jump intensity is $\tilde q(x,a)=\tilde q(x,a,X\setminus\{x\})$, and Assumption 2.1 requires $\bar q(x)=\sup_{a\in A(x)}\tilde q(x,a)<\infty$ for every $x$. A probability measure $p$ on $A$ acts through $\tilde q(x,p)=\int\tilde q(x,a)\,p(da)$ and $\tilde q(x,p,Z)=\int\tilde q(x,a,Z)\,p(da)$.

A trajectory is $\omega=(x_0,t_1,x_1,t_2,x_2,\dots)$, with jump epochs $0=t_0<t_1<t_2<\cdots\le\infty$ and post-jump states $x_n$; the process is $\xi_t=x_n$ for $t_n\le t<t_{n+1}$ and leaves $X$ at $t_\infty=\lim_nt_n$. A policy $\pi$ chooses, between the $n$th and $(n+1)$st jump, the action distribution $\pi_n(\cdot\mid x_0,t_1,\dots,t_n,x_n,t-t_n)$, concentrated on $A(x_n)$. A Markov policy is a transition probability $\phi(\cdot\mid z,t)$ from $X\times(0,\infty)$ to $A$ with $\phi(A(z)\mid z,t)=1$. An initial distribution $\gamma$ and a policy $\pi$ define the law $\mathbb P^\pi_\gamma$ of the process: from $x_n$ the next jump occurs at hazard rate $\tilde q(x_n,\pi_s)$ and lands in $dy$ with intensity $\tilde q(x_n,\pi_s,dy\setminus\{x_n\})$.

The state marginal and the state-action marginal are

$$P^\pi_\gamma(t,Z)=\mathbb P^\pi_\gamma(\xi_t\in Z),\qquad P^\pi_\gamma(t,Z,B)=\mathbb E^\pi_\gamma\big[I\{\xi_{t-}\in Z\}\,\pi(B\mid\omega,t)\big],$$

for $t>0$, $Z\subseteq X$, $B\subseteq A$. A Markov policy $\phi$ satisfies (16) for $(\gamma,\pi)$ if

$$P^\pi_\gamma(t,Z,B)=\int_Z\phi(B\mid z,t)\,P^\pi_\gamma(t,dz)\qquad\text{for all }t>0,\ Z,\ B,$$

that is, $\phi(\cdot\mid z,t)$ is the conditional distribution of the action given $\xi_{t-}=z$ under $\pi$. The process under $\phi$ is nonexplosive when $P^\phi_\gamma(t,X)=1$ for all $t>0$.

Formalization targets

Goal: Theorem 1

If $\phi$ is a Markov policy satisfying (16) for $(\gamma,\pi)$, then

$$P^\phi_\gamma(t,Z,B)\le P^\pi_\gamma(t,Z,B)\qquad\text{for all }t>0,\ Z,\ B,$$

with equality for $t\in\,]0,s]$ whenever $P^\phi_\gamma(s,X)=1$, and equality for all $t>0$ when the process under $\phi$ is nonexplosive.

Milestones

The milestones follow the paper's proof: existence and uniqueness of $\mathbb P^\pi_\gamma$ (§2); the compensator identities (8) and Lemma 3; the forward identity (37) for $(x,\pi)$-bounded sets (Lemma 4); Feller's minimal solution of Kolmogorov's forward equation (Theorem 3), its identification with the marginal of a Markov policy ((31), Corollary 5); the occupation identities (49)–(50); the state-marginal comparison (Lemma 2) and Theorem 1 for one initial state (Lemma 5); the characterization (19) of (16) (Corollary 1); the scaling identity (58)–(59) and the claim (19) for the extended model (p. 16); and the existence of $\phi$ (Lemma 1).

Significance

Theorem 1 with Lemma 1 shows that Markov policies are sufficient in CTJMDPs with unbounded rates. Every cost criterion that is a monotone functional of state-action marginals with nonnegative costs (expected total discounted costs, finite-horizon costs, average costs per unit time, and the corresponding constrained problems) is no larger under the Markov policy, which is the content of §6 of the paper. Equality holds whenever the Markov policy does not explode, for example when the rates are bounded (Corollary 2), and two Markov policies satisfying (16) have the same law (Corollary 3). The intermediate results, in particular Lemma 4 (the forward identity for possibly explosive processes) and Feller's minimal-solution theorem, are tools in their own right for continuous-time Markov chains on general state spaces.

The result is proved in the paper; nothing here is open mathematically. No part of it is formalized: Mathlib has no jump processes, compensators of point processes, Kolmogorov forward equations on general state spaces, or Feller's construction of minimal transition functions. The mission produces a machine-checked account of these foundations and of the sufficiency theorem built on them, with every measure-theoretic step (the law of the process, the disintegration, the minimality argument) made explicit.

Difficulty

The direct argument for discrete time compares the two marginals step by step through the one-step transition law. In continuous time there is no first step, and the natural replacement, comparing the forward equations satisfied by the two marginals, breaks down twice. First, with unbounded rates the integrals in the forward equation (37) can be infinite, so the equation is not even well defined for all sets, and the standard derivations assume nonexplosiveness. Second, forward equations need not have unique solutions when the process can explode, so showing that both marginals solve the same equation does not make them equal. The paper handles the first point with the class of $(x,\pi)$-bounded sets and the second with Feller's minimal solution, which yields only an inequality in general; equality needs the probability-one condition. Passing from an initial state to an initial distribution is a further step: the forward equation is stated for a point initial condition, and the reduction goes through an extended model with an added state.

Formalization scope

All quantities take values in $[0,\infty]$. Rates are given by off-diagonal finite jump measures, with $\tilde q:=0$ off $\mathrm{Gr}(A)$. A trajectory is an element of X × (ℕ → ℝ≥0∞ × X); the cemetery point is not a separate state, and $x_n$ is ignored once $t_n=\infty$. A policy is a family $\pi_n(\cdot\mid\omega,s)$ that depends only on the history up to the $n$th jump. Marginals read the process at $\xi_{t-}$, which equals $\xi_t$ almost surely at each fixed $t$.

The law $\mathbb P^\pi_\gamma$ is a hypothesis of each statement: any probability measure on trajectories with initial law $\gamma$ whose one-step conditional laws are the explicit sojourn/jump kernel (the Ionescu-Tulcea construction (75)–(76) of the paper) is admitted, and a milestone states that exactly one such measure exists. The paper characterizes the same measure through Jacod's compensator theorem. The compensator properties (8) and Lemma 3 are stated as (8) for every stopping time of the natural filtration $\sigma(\xi_s: 0\le s\le t)$. Kolmogorov's forward equations are written additively, with the subtracted integral finite, which is equivalent to the real equation. In the extended model of the proof the added state and actions are Sum.inr points of X ⊕ Unit and A ⊕ Bool; the policy (55) is evaluated on the observed part of the path and chooses the absorbing action off the set $\Omega'(u)$, which is a null set.

A formalization in which the law is never shown to exist, or in which (16) cannot be satisfied, would make Theorem 1 vacuous; the existence-and-uniqueness milestone and Lemma 1 rule this out.

A complete development needs the Ionescu-Tulcea construction of the law, compensators of multivariate point processes, the forward equation and Feller's series on a standard Borel space, and disintegration of measures. The first three are reusable for any continuous-time Markov chain or CTJMDP on a general state space, and contributions to them are welcome on their own.

Selected references

• E. A. Feinberg, M. Mandava, A. N. Shiryaev, Sufficiency of Markov policies for continuous-time jump Markov decision processes, Mathematics of Operations Research, 2022; arXiv:2003.01342v3. https://arxiv.org/abs/2003.01342
• E. A. Feinberg, M. Mandava, A. N. Shiryaev, Kolmogorov's equations for jump Markov processes with unbounded jump rates, Annals of Operations Research, 2017. https://doi.org/10.1007/s10479-017-2538-8
• E. A. Feinberg, M. Mandava, A. N. Shiryaev, On solutions of Kolmogorov's equations for nonhomogeneous jump Markov processes, Journal of Mathematical Analysis and Applications 411(1):261–270, 2014.
• J. Jacod, Multivariate point processes: predictable projection, Radon–Nikodym derivatives, representation of martingales, Probability Theory and Related Fields 31:235–253, 1975.
• M. Kitaev, V. Rykov, Controlled Queueing Systems, CRC Press, 1995.
• X. Guo, X. Song, Discounted continuous-time constrained Markov decision processes in Polish spaces, Annals of Applied Probability 21(5):2016–2049, 2011.
• A. Piunovskiy, Y. Zhang, Discounted continuous-time Markov decision processes with unbounded rates and randomized history-dependent policies: the dynamic programming approach, 4OR 12:49–75, 2014.
• C. Derman, R. Strauch, A note on memoryless rules for controlling sequential control processes, Annals of Mathematical Statistics 37:276–278, 1966.
• W. Feller, On the integro-differential equations of purely-discontinuous Markoff processes, Transactions of the AMS 48:488–515, 1940.

Learning while doing, and the frontier of continuation values

Many sequential decisions trade off immediate reward against information: a firm prices without knowing which demand regime it faces, a clinician treats without knowing a patient's type, a bandit player pulls a risky arm to learn its mean. Formally these are partially observed Markov decision problems (POMDPs) with a hidden but fixed state. Their value function is the upper envelope of a set of linear functions of the belief, one continuation-value vector per policy. The efficient frontier of these vectors describes the optimal policy for every prior at once. Except for special cases, the frontier of a POMDP has to be computed numerically.

Hao Zhang (Management Science, 2021; accepted version SSRN 3847049) treats the case of two states, two actions and two signals. Under a commensurability condition on the signals, the extreme points of the frontier satisfy linear difference equations with constant coefficients (Theorems 2 and 4 of the paper). The paper solves these equations in closed form. Theorem 3 covers the case where the second action reveals nothing, so that it acts as a stopping action. Theorem 6 covers the case where both actions are informative. This mission formalizes the solution of the difference equations, including the explicit determinant of the coupling matrix that Appendix B states as Theorem 6 (Complete).

Setting

The hidden state is $\theta \in \{1, 2\}$, the actions are $A$ and $B$, and the signals are $\gamma$ and $\bar\gamma$. In each period, action $a$ in state $\theta$ produces signal $\gamma$ with probability $p_\theta(a, \gamma)$ and an expected reward $r_\theta(a)$, and rewards are discounted by $\delta \in (0, 1)$. The anchor points $\hat u^a_\theta = (1-\delta)^{-1} r_\theta(a)$ are the values of always playing $a$. Write $p^A_\theta = p_\theta(A,\gamma)$ and $p^B_\theta = p_\theta(B,\gamma)$.

The signal quality indices are integers $n(A,\gamma) = n^A > 0$, $n(A,\bar\gamma) = -\bar n^A < 0$, $n(B,\gamma) = n^B > 0$ and $n(B,\bar\gamma) = -\bar n^B < 0$. Their absolute values are relatively prime, and for some $\mu > 1$ each log-likelihood ratio $\ln(p_1(a,s)/p_2(a,s))$ equals $n(a,s) \ln\mu$ (Definition 3).

For each $\theta$ the paper's boundary-value problem (28)–(31) asks for real sequences $v^A, v^B$ on $k = 0, 1, 2, \dots$ satisfying four conditions:

$$v^A(k+n^A) - \delta^{-1}(p^A_\theta)^{-1} v^A(k) + (p^A_\theta)^{-1}(1-p^A_\theta)\, v^A(k-\bar n^A) = 0 \quad (k \ge \bar n^A),$$ $$v^B(k+\bar n^B) - \delta^{-1}(1-p^B_\theta)^{-1} v^B(k) + (1-p^B_\theta)^{-1} p^B_\theta\, v^B(k-n^B) = 0 \quad (k \ge n^B),$$

the coupling condition $v^A(k) + \hat u^A_\theta = v^B(\bar n^A + n^B - 1 - k) + \hat u^B_\theta$ for $k = 0, \dots, \bar n^A + n^B - 1$, and decay, $v^A(k), v^B(k) \to 0$.

The characteristic polynomials are

$$f^A_\theta(z) = z^{n^A+\bar n^A} - \delta^{-1}(p^A_\theta)^{-1} z^{\bar n^A} + (p^A_\theta)^{-1}(1-p^A_\theta), \qquad f^B_\theta(z) = z^{n^B+\bar n^B} - \delta^{-1}(1-p^B_\theta)^{-1} z^{n^B} + (1-p^B_\theta)^{-1}p^B_\theta.$$

$Z^a_{unit}$ is the set of their roots with $|z| < 1$, and $m^a_z$ is the multiplicity of the root $z$. From these roots the paper builds a square matrix $Y = (Y^A, Y^B)$. Its A-columns are $\binom{k}{\tau}z^{k-\tau}$ and its B-columns are $\binom{\bar n^A+n^B-1-k}{\tau}z^{\bar n^A+n^B-1-k-\tau}$, in a fixed column order.

Formalization targets

Goal: Theorem 6 (Complete), EC p. 11

For each $\theta$, under the standing assumptions of §5, the goal asserts four things:

1. $\sum_{z\in Z^A_{unit}} m^A_z = \bar n^A$ and $\sum_{z\in Z^B_{unit}} m^B_z = n^B$.
2. For every enumeration of the roots,

$$\det Y = \prod_{i<l}(z^A_l - z^A_i)^{m^A_i m^A_l}\prod_{i,l}(1 - z^A_i z^B_l)^{m^A_i m^B_l}\prod_{i<l}(z^B_i - z^B_l)^{m^B_i m^B_l}.$$

3. $\det Y \ne 0$.
4. The problem (28)–(31) has exactly one real solution. That solution is the root expansion $v^a_\theta(k) = \sum_{z \in Z^a_{unit}}\sum_{\tau<m^a_z}\alpha^a_{z,\tau}\binom{k}{\tau}z^{k-\tau}$, whose coefficients are given by $(\boldsymbol\alpha^A; -\boldsymbol\alpha^B) = (\hat u^B_\theta - \hat u^A_\theta)Y^{-1}\mathbf 1$.

Milestones

• Eq. (18): the general solution of a constant-coefficient linear recurrence with repeated characteristic roots.
• Eq. (19): the determinant of the generalized (confluent) Vandermonde matrix.
• From the proof of Theorem 3: $z^{n+\bar n} - \delta^{-1}p^{-1}z^{\bar n} + p^{-1}(1-p)$ has exactly $\bar n$ roots in the open unit disk, counted with multiplicity.
• From the proof of Theorem 3: decay of an exponential polynomial forces zero coefficients on every root with $|z| \ge 1$.
• Theorem 3: the one-sided problem (13)–(15), when action $B$ is uninformative.
• The base case and the inductive step of the determinant computation in the proof of Theorem 6 (Complete).

Significance

The result turns the efficient frontier of this class of POMDPs into explicit algebra. Each extreme point is a finite sum over the roots of two trinomials in the unit disk, and the coefficients come from one linear solve. The paper uses this to explain the shape of the frontier: how many extreme points the two actions contribute, and how quickly they accumulate at the anchor points. It also shows that the coupled two-sided problem is always well posed, because $Y$ is nonsingular.

The paper proves the results in prose; none of them is machine-checked. The mission contributes a checked proof of the solution formula and of the determinant identity. The identity is a confluent Vandermonde-type evaluation with a reflected second block. Several pieces are general mathematics that Mathlib lacks: the solution space of a linear recurrence with repeated roots in binomial form, the confluent Vandermonde determinant, root counting in the unit disk, and the decay lemma for exponential polynomials.

Difficulty

The obvious argument is to write down the general solution, discard the growing modes and match the boundary data. It runs into three problems. First, the count of roots in the disk is what makes $Y$ square. It comes from Rouché's theorem, which Mathlib does not have, so it must be proved or replaced by a polynomial argument. Second, roots on the unit circle are not excluded a priori, so the decay argument has to handle polynomially weighted unimodular terms. Third, and hardest, is $\det Y \ne 0$. $Y$ is not a confluent Vandermonde matrix: its B-block is reflected ($N-1-k$ in place of $k$). The paper reduces the simple-root case to a Vandermonde matrix in the inverted points $1/z^B_j$, and then handles each repeated B-root by differentiating with respect to a "nominal root". Making that induction precise requires care with column orders and signs.

Formalization scope

The Lean development lives in the namespace LearnDoFrontier.TwoAction. A Model carries $\delta$, $p^A_\theta$, $p^B_\theta$, the rewards $r_\theta(a,s)$ and the four indices, with the negative indices stored as the positive naturals $\bar n^A, \bar n^B$. States, actions and signals are Fin 2, and index 0 stands for $\theta = 1$, $A$ and $\gamma$. Model.Standing collects the assumptions of §5: $0<\delta<1$, General Position, Informative Actions A and B, and Definition 3, with "relatively prime" read as a joint gcd of $1$. Sequences are real and indexed by $\mathbb N$, while the roots, coefficients and $Y$ are complex. The solution formula is an equality in $\mathbb C$. Root enumerations are arbitrary bijections onto $Z^a_{unit}$, universally quantified, and the columns of $Y$ follow the paper's order: A-columns first, roots first, then $\tau$ ascending for A and descending for B. Exponents use natural-number subtraction, which is harmless because the binomial factor vanishes whenever $k<\tau$. The determinant milestones are stated for arbitrary distinct points rather than roots, as the paper's induction uses them.

No formalization may make the targets hold by definition. $Z_{unit}$ and $m_z$ are the actual roots and multiplicities, never "the first $\bar n^A$ roots". Uniqueness ranges over all real sequences satisfying (28)–(31), not only over root expansions. The coefficients are given by $Y^{-1}$, not chosen to fit the boundary.

The link from the POMDP's efficient frontier to (13)–(15) and (28)–(31) (Theorems 2 and 4) is not formalized. Its proofs are geometric sketches, and Theorem 4 assumes a two-segment frontier structure that the paper itself calls a conjecture. The mission is about the difference equations exactly as the paper poses them. Proofs of any milestone are welcome, and the recurrence, Vandermonde and root-count lemmas are reusable well beyond this mission.

Selected references

• Hao Zhang, Analytical Solution to a Discrete-Time Model for Dynamic Learning and Decision Making, Management Science, 2021. https://doi.org/10.1287/mnsc.2021.4194 ; accepted version with E-Companion: https://ssrn.com/abstract=3847049
• Saber Elaydi, An Introduction to Difference Equations, 3rd ed., Springer, 2005. https://doi.org/10.1007/0-387-27602-5
• Richard D. Smallwood and Edward J. Sondik, The Optimal Control of Partially Observable Markov Processes over a Finite Horizon, Operations Research 21(5), 1973. https://doi.org/10.1287/opre.21.5.1071

Motivation

Online marketplaces such as Zalando, Amazon or Farfetch let brands sell through the platform's storefront in addition to their own stores. One common arrangement is inventory sharing: the brand keeps ownership of its stock, but makes it visible to the platform's customers, and pays the platform a commission on every unit the platform sells. For a supplier with a fixed stock and a finite selling season, this creates a timing question. Sharing brings more customers, but each platform sale earns less than a direct one. Early in the season there is plenty of time to sell the stock at full margin; late in the season unsold units are worth nothing.

Martínez-de-Albéniz, Pinto and Amorim (SSRN 3643261, 2020; published in Manufacturing & Service Operations Management, 2022) model this problem as a continuous-time optimal control problem with Poisson demand, solve the supplier's problem, and use the solution to study how the platform should set its commission. The supplier's problem is a binary-control relative of the dynamic pricing problem of Gallego and van Ryzin (Management Science 1994): sharing switches the effective price and the demand rate between two values. Its solution is the building block for the paper's platform-pricing results.

Setting

A supplier sells a single item during a season. Time is measured as the time-to-go $t \ge 0$ until the end of the season ($t = 0$ at the end). The item sells at the price $\pi > 0$. Customers of the supplier's own (direct) channel arrive as a Poisson process of rate $\lambda_D > 0$; customers of the platform arrive at rate $\lambda_P > 0$. On a direct sale the supplier earns $\pi$; on a platform sale it keeps $(1-\theta)\pi$, where $\theta \in [0,1]$ is the commission. Revenue is discounted at rate $r \ge 0$, and leftover units are worth nothing.

At every moment the supplier chooses $z \in \{0,1\}$: $z = 1$ shares the inventory with the platform, $z = 0$ does not. Write $V_n(t)$ for the revenue-to-go with $n$ units left and time-to-go $t$, and $\Delta V_n(t) = V_n(t) - V_{n-1}(t)$ for the marginal revenue-to-go of the $n$-th unit. The revenue-to-go solves the Hamilton–Jacobi–Bellman equation (3)

$$\frac{dV_n}{dt} = \sup_{z\in\{0,1\}}\Bigl[\bigl(\pi\lambda_D + z(1-\theta)\pi\lambda_P\bigr) - (\lambda_D + z\lambda_P)\,\Delta V_n(t) - rV_n(t)\Bigr], \qquad n \ge 1,$$

with $V_0 \equiv 0$ and $V_n(0) = 0$. A decision is optimal for unit $n$ at time $t$ if it attains this supremum. The threshold of unit $n$ is

$$t_n = \sup\{t \ge 0 : \Delta V_n(t) \le (1-\theta)\pi\} \in [0, \infty], \qquad t_0 = 0,$$

which is $\infty$ when $\Delta V_n$ never exceeds the platform margin $(1-\theta)\pi$. In Lean these objects are Params, hamiltonian, hjbRHS, IsRevenueToGo, marginal, IsOptimalDecision and threshold in the namespace MarketplaceSharing.Threshold.

Formalization targets

Goal: Theorem 1 (p. 9)

For every revenue-to-go $V$ and every $n \ge 1$:

$$\Delta V_n \text{ is strictly increasing on } [0,\infty), \qquad \Delta V_n(t) = (1-\theta)\pi \iff t = t_n,$$ $$z = 1 \text{ is optimal at } (t, n) \iff t \le t_n, \qquad t > t_n \implies z = 0 \text{ is optimal and } z = 1 \text{ is not},$$

and on each interval $I_{nj} = [t_{j-1}, t_j]$, $1 \le j \le n$, and on $I_{n,n+1} = [t_n, \infty)$, there are constants with

$$V_n(t) = C_{nj} + \sum_{i=0}^{n-j} A_{nji}\,t^i e^{-(\lambda_D+\lambda_P+r)t} + \sum_{i=0}^{j-2} B_{nji}\,t^i e^{-(\lambda_D+r)t}. \tag{4}$$

The coefficients are existential, as on the page; their recursions are not part of the goal.

Milestones

In attack order: well-posedness of (3) (a solution exists and is unique on $[0,\infty)$); the sharing condition of p. 8, $z = 1$ optimal $\iff \Delta V_n(t) \le (1-\theta)\pi$; Lemma 1, $V_{n+1} \ge V_n$; Lemma 2, $\Delta V_{n+1} \le \Delta V_n$; Lemma 3, $V_n$ nondecreasing in $t$; Lemma 4, $\Delta V_n$ nondecreasing in $t$; the explicit $t_1$ of footnote 4 (at $r = 0$); the first bullet of Theorem 1; and Corollary 1, $t_{n+1} \ge t_n$.

Significance

Theorem 1 reduces the supplier's policy, a function of time and stock, to one number per unit: share the $n$-th remaining unit exactly when the time-to-go is at most $t_n$. Corollary 1 orders these numbers, so the season splits into an early period of direct-only sales and a late period of sharing, which begins earlier the more stock is left. The closed form (4) makes $V_n$ and the thresholds computable. The paper's analysis of the platform's commission (Theorems 2 and 3) takes this policy as the supplier's best response.

The results are proved in the paper, by an induction on $n$ that runs through Lemmas 1–4. None of it has a machine-checked proof. A formalization produces a checked proof of a threshold structure for a two-mode Poisson control problem, a checked statement of where the printed text needs correcting (see below), and reusable pieces: well-posedness of a recursive system of Lipschitz ODEs and comparison arguments for HJB equations of this type.

Difficulty

The HJB system (3) is a recursive family of ODEs whose right-hand side switches between two affine laws according to the sign of $(1-\theta)\pi - \Delta V_n(t)$. The monotonicity statements are comparison results for such switched systems: the obvious argument (differentiate $\Delta V_n$ and read off the sign) gives an equation for $\Delta V_n'$ that involves $\Delta V_{n-1}'$ and the switching times of both units, so monotonicity in $t$ and in $n$ have to be established together, unit by unit. The closed form (4) then needs the switching times of all lower units to be ordered (Corollary 1) before the ODE on each interval has constant decisions, and the polynomial factors $t^i$ come from repeated resonance of the exponential $e^{-(\lambda_D+\lambda_P+r)t}$ across units.

Formalization scope

The paper defines $V_n$ by a stochastic control problem (2) over Poisson sales processes and derives (3) informally. The mission works with (3) only: the revenue-to-go is any family $V : \mathbb{N} \to \mathbb{R} \to \mathbb{R}$ satisfying IsRevenueToGo ($V_0 = 0$ on $[0,\infty)$, $V_n(0) = 0$, and the HJB equation for $n \ge 1$ as a derivative within $[0,\infty)$, one-sided at $0$), and every theorem takes this as a hypothesis. The well-posedness milestone shows such a family exists and is unique on $[0,\infty)$, so no theorem is vacuous. Values at $t < 0$ are unconstrained. Decisions are Booleans (true = share).

Conventions and added hypotheses: $\pi > 0$, $\lambda_D > 0$, $\lambda_P > 0$ and $r \ge 0$ are standing hypotheses (with $\lambda_P = 0$ or $\pi = 0$ the two decisions tie everywhere and the threshold statement fails); $\theta \in [0,1]$ is printed. The paper's range $n \in \{1,\dots,N\}$ is read as $n \ge 1$, since $V_n$ does not depend on $N$. The threshold lives in the extended reals with $t_n = \infty$ when $\Delta V_n = (1-\theta)\pi$ has no solution (p. 10); the literal "there is an unique $t_n$" fails for instance at $\theta = 0$. Three printed formulas are corrected and disclosed: the exponents of (4) carry $r$, as the proof on p. 30 does (the printed form is exact only at $r = 0$); Lemma 4 is stated in the direction of its words and proof, $\Delta V_n(t_1) \le \Delta V_n(t_2)$ for $t_2 \ge t_1 > 0$ (the printed display is reversed); and the $t_1$ formula of footnote 4 is stated at $r = 0$ (with $\theta > 0$), the only case in which it is exact.

The encoding rules out the trivializing readings: "optimal" is attainment of the supremum in (3), not membership in $[0, t_n]$; $t_n$ is the supremum of a sublevel set that always contains $0$, not a solution of $\Delta V_n = (1-\theta)\pi$ that could make uniqueness definitional; monotonicity of $\Delta V_n$ is a conclusion of the goal, never a hypothesis; and the hypothesis IsRevenueToGo is satisfiable by the well-posedness milestone.

Not formalized: the stochastic formulation (2) and its identification with (3); the recursions for $A_{nji}$, $B_{nji}$, $C_{nj}$ (pp. 31–32); the numerical study of §3.3; and the platform-pricing results (Theorems 2 and 3, §4) and §5. A complete development needs one-dimensional ODE existence and uniqueness (Picard–Lindelöf and Grönwall, available in Mathlib), comparison of solutions of scalar ODEs, and calculus with $t^i e^{-ct}$. Proofs of any milestone, and reusable comparison lemmas for switched affine ODEs, are welcome.

Selected references

• V. Martínez-de-Albéniz, C. Pinto, P. Amorim, Driving Supply to Marketplaces: Optimal Platform Pricing When Suppliers Share Inventory, SSRN 3643261, version of June 30, 2020; Manufacturing & Service Operations Management, 2022. https://ssrn.com/abstract=3643261
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8), 999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• V. Martínez-de-Albéniz, K. Talluri, Dynamic Price Competition with Fixed Capacities, Management Science 57(6), 1078–1093, 2011. https://doi.org/10.1287/mnsc.1110.1337

Motivation

A firm that sells several products must decide, before demand is known, how much capacity to build. It can build dedicated capacity, one resource per product, or a single flexible resource that can serve any product but costs more per unit. The classical argument for flexibility is risk pooling: one pooled resource absorbs the fluctuations of several demands, as studied by Fine and Freund (1990) and Van Mieghem (1998).

Chod, Markakis and Trichakis (SSRN 3212177, published in Management Science, 2021) identify a second, independent benefit. A firm usually observes its sales, not its demand: when a product stocks out, the firm learns only that demand exceeded capacity. This is demand censoring. Because flexible capacity can be shifted to whichever product is in demand, it stocks out less often for each product, and so the firm learns more about demand from a flexible system than from a dedicated one. When demand is correlated over time, that information is worth money in later periods. The paper calls this the learning benefits of flexibility and asks when they are positive.

To separate learning from pooling, the paper compares the two systems at the break-even cost of flexibility, the unit cost of flexible capacity at which both systems earn the same profit in a single period. Any difference that remains in a two-period model is then due to learning alone (Eq. (14) of the paper).

Setting

There are two products with a common unit price $p$. Dedicated capacity costs $c$ per unit and flexible capacity costs $c_F$ per unit, with $0 \le c < p$. The first-period demands $D^1_1, D^1_2$ are independent and each uniform on $[x, x+U]$, with $x \ge 0$ and $U > 0$. The profit margin is $(p-c)/p$.

Static model. With dedicated capacities $\mathbf Q = (Q_1, Q_2)$, product $i$ sells $\min\{D_i, Q_i\}$, and the expected profit is $\pi_N(\mathbf Q) = p\,\mathbb E[\min\{D_1,Q_1\} + \min\{D_2,Q_2\}] - c(Q_1+Q_2)$. With flexible capacity $Q_F$, product 1 is served first: it sells $S_{F,1} = \min\{D_1, Q_F\}$ and product 2 sells $S_{F,2} = \min\{D_2, Q_F - S_{F,1}\}$; the expected profit is $\pi_F(c_F)(Q_F) = p\,\mathbb E[S_{F,1} + S_{F,2}] - c_F Q_F$. The optimal static profits are

$$\bar\pi_N = \sup_{\mathbf Q \in \mathbb R^2_+} \pi_N(\mathbf Q), \qquad \bar\pi_F(c_F) = \sup_{Q_F \ge 0} \pi_F(c_F)(Q_F),$$

and $c_F$ is a break-even cost when $\bar\pi_F(c_F) = \bar\pi_N$.

Learning. A product that had $q$ units available and demand $d$ reveals $d$ exactly if $d < q$; otherwise the firm learns only that $D \ge q$ and conditions its prior on that event. The firm's belief after period 1 is the product of the two products' posteriors. In period 2 demand repeats ($D^2_i = D^1_i$), and both systems build dedicated capacity against the posterior belief $\mathbb G$, earning

$$V^2(\mathbb G) = \sup_{\mathbf Q \in \mathbb R^2_+} \mathbb E_{\mathbb G}\big[p\min\{D_1,Q_1\} + p\min\{D_2,Q_2\} - c(Q_1+Q_2)\big].$$

The two-period optimal profits are

$$V_N = \sup_{\mathbf Q \in \mathbb R^2_+} \Big(\pi_N(\mathbf Q) + \mathbb E\big[V^2(\mathbb P(\cdot \mid \mathbf S^1_N))\big]\Big), \qquad V_F(c_F) = \sup_{Q_F \ge 0} \Big(\pi_F(c_F)(Q_F) + \mathbb E\big[V^2(\mathbb P(\cdot \mid \mathbf S^1_F))\big]\Big).$$

Formalization targets

Goal: Proposition 1

Take $x = 0$. There is a threshold $\zeta \in (0,1)$ such that for all $p, c, U, c_F$ with $0 \le c < p$, $U > 0$, $c \le c_F < p$ and $\bar\pi_F(c_F) = \bar\pi_N$,

$$\frac{p-c}{p} \le \zeta \implies V_F(c_F) \ge V_N, \qquad \frac{p-c}{p} > \zeta \implies V_F(c_F) \le V_N.$$

The goal fixes no numerical value of $\zeta$; the paper reports $\zeta \approx 0.5904$.

Milestones

1. Lemma 3: the uniform newsvendor optimum $\bar Q = x + U(p-c)/p$ with profit $(p-c)x + \tfrac U2 (p-c)^2/p$.
2. The static non-flexible optimum $\bar\pi_N = 2(p-c)x + U(p-c)^2/p$.
3. The static flexible optimum $\bar Q_F(c_F)$, $\bar\pi_F(c_F)$ in the two branches $p \ge 2c_F$ and $p < 2c_F$.
4. Eq. (8): the pooling benefits $\bar\pi_F(c_F) - \bar\pi_N$ are strictly decreasing in $c_F$, and the break-even cost exists and is unique in $[c, p)$.
5. The two-period non-flexible optimum: $V_N = 4x(p-c) + U(p-c)^2(3c+2p)/\Delta$ with $\Delta = (p-c)(p+c) + cp$.
6. The flexible case $Q_F \ge 2x + U$: concavity, the right derivative $(-c^2 + cp + p(p-2c_F))/(2p)$ at $2x+U$, and the price threshold $\tilde p$.

Significance

Proposition 1 says that learning favours flexibility when margins are low or moderate and favours dedicated capacity when margins are high. Combined with the risk-pooling analysis, it shows that the value of flexibility in a dynamic setting is not captured by static pooling models: a firm choosing a technology by comparing single-period profits misjudges it in both directions, depending on the margin. The comparison at the break-even cost is the cleanest available measurement of the information value of a capacity structure under censored demand.

The paper proves Proposition 1 by computing closed forms of all the value functions and then certifying a polynomial inequality over a semialgebraic parameter set with sum-of-squares methods (p. A8). No machine-checked proof exists. A formalization would replace a computer-algebra certificate whose details are not printed with a checked argument, and would fix the value-function closed forms (milestones 2–6), which the paper derives in a few lines each. The milestones are of independent use: Lemma 3 and the censored-sales posterior are standard in inventory learning models.

Difficulty

The value functions $V_N$ and $V_F(c_F)$ are suprema of first-period profit plus the expectation of a second-period value under a posterior that depends on whether each product stocked out. In the flexible system the capacity left for product 2 depends on product 1's realized demand, so the posterior of product 2 depends on product 1's demand, and the objective $v_F$ splits into regimes with different formulas; it is not concave in general (the paper notes "optimization of non-concave functions", p. 12). The break-even cost is defined implicitly by an equation involving square roots, so the final comparison is between two functions of $(p, c)$ along an implicit curve; the obvious approach of comparing closed forms branch by branch needs a sign certificate for a polynomial system rather than a one-line inequality.

Formalization scope

Everything is real-valued. The uniform prior is $U^{-1}$ times Lebesgue measure on $[x, x+U]$; the joint prior is the product measure. The stock-out posterior is Mathlib's conditional measure cond of the prior on $\{D \ge q\}$, an exact observation is a Dirac measure, and a demand is observed exactly iff it is strictly below the available capacity (p. 9). The joint posterior is the product of the per-product posteriors, which is exact because the observation is a product event given product 1's demand. All optima are real suprema of images over nonnegative capacities, never closed forms. The symmetric case of §3 is built in ($p_1 = p_2 = p$, common $c$, i.i.d. uniform demands), as is $\xi = 0$ (second-period demand equals first-period demand); at $x = 0$ the paper's noise $U[-\xi x, \xi x]$ is zero for every $\xi$, so the goal loses nothing. Added hypotheses, disclosed in each statement: $U > 0$, $0 \le c < p$, $c \le c_F < p$, and in the goal $0 < \zeta < 1$.

The values must not be defined by their closed forms or by the paper's case split $j = 1, 2, 3$; that would make the goal a statement about polynomials rather than about the Bellman problems.

A complete development needs: integrals of piecewise-linear functions against uniform laws and their products, conditional uniform laws, measurability of the posterior-dependent second-period value, and a sign certificate for the final polynomial comparison. The newsvendor and censored-posterior lemmas are reusable in other inventory-learning models. Contributions are welcome on any milestone, on alternative proofs of the final comparison, and on the regime $j = 3$ of the flexible objective, which the milestones do not cover.

Selected references

• J. Chod, M. G. Markakis, N. Trichakis, On the Learning Benefits of Resource Flexibility, SSRN preprint 3212177 (December 6, 2019); published in Management Science, 2021. https://ssrn.com/abstract=3212177, https://doi.org/10.1287/mnsc.2020.3795
• C. H. Fine, R. M. Freund, Optimal Investment in Product-Flexible Manufacturing Capacity, Management Science 36(4), 1990. https://doi.org/10.1287/mnsc.36.4.449
• J. A. Van Mieghem, Investment Strategies for Flexible Resources, Management Science 44(8), 1998. https://doi.org/10.1287/mnsc.44.8.1071
• P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming 96, 2003. https://doi.org/10.1007/s10107-003-0387-5

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