All missions

Motivation

In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.

Setting

Write $\mathcal I$ for the set of all subsegments $I=[a,b]$ of $[0,1]$ with $0\le a\le b\le1$. An interval may be degenerate, meaning $a=b$. A real-valued function $f$ on $\mathcal I$ is continuous when its value varies continuously with the two endpoints. The required boundary condition is $f([a,a])=0$ for every $a\in[0,1]$. No sign, monotonicity, or additivity condition is imposed. A partition into $m$ parts is a sequence $0=x_0\le x_1\le\cdots\le x_m=1$, so its parts $[x_{j-1},x_j]$ may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.

The intermediate setting is a nice multivalued function. Its graph is a compact subset $Z$ of $\mathcal I\times(-1,1)$. The graph separates the bottom $\mathcal I\times\{-1\}$ from the top $\mathcal I\times\{1\}$ inside the cylinder $C=\mathcal I\times[-1,1]$: those two sides lie in different connected components of $C\setminus Z$. A representation of a nice graph is a continuous real function $\varphi$ on $C$ that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.

For a prime $p$, a segment $I=[a,b]$, and a value $y$, a zero partition is a sequence $a=x_0\le\cdots\le x_p=b$ such that $\varphi([x_{j-1},x_j],y)=0$ for each $j=1,\ldots,p$. The set $Z_p(\varphi)$ contains exactly those pairs $(I,y)$ that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set $S$ for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.

Formalization targets

The goal is Theorem 1.1: for every positive integer $m$ and every continuous $f$ satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:

$$0=x_0\le x_1\le\cdots\le x_m=1,\qquad f([x_0,x_1])=\cdots=f([x_{m-1},x_m]).$$

The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when $\varphi([a,a],y)=y$, there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for $\varphi$. The milestone list includes the fixed-segment and continuous-family statements used to characterize $Z_p(\varphi)$, and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.

Significance

The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.

Difficulty

For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod-$p$ statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy $\psi([a,a],y)=y$, not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.

Formalization scope

Lean represents $I=[a,b]$ by the endpoint pair $(a,b)$ with $0\le a\le b\le1$. The cylinder uses the closed value range $[-1,1]$; a nice graph lies in its open interior $(-1,1)$. Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.

Every prime-step claim assumes $p$ prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly $p$ consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes $m\ge1$. The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.

Selected references

• Sergey Avvakumov and Roman Karasev, Equipartition of a Segment, Mathematics of Operations Research, 2023. arXiv:2009.09862v4.
• Anna Bogomolnaia and Hervé Moulin, Guarantees in Fair Division: General or Monotone Preferences, 2019. arXiv:1911.10009v3.
• Sergey Avvakumov and Roman Karasev, Envy-Free Division Using Mapping Degree, Mathematika 67, 2021. arXiv:1907.11183.
• Frédéric Meunier and Shira Zerbib, Envy-Free Cake Division Without Assuming the Players Prefer Nonempty Pieces, Israel Journal of Mathematics 234, 2019. arXiv:1804.00449.

Motivation

Financial networks, supply chains and contact networks share a failure mode: a node fails when enough of its counterparties have failed, and its failure in turn weakens its own counterparties. Threshold contagion on random graphs is the standard mathematical model of this. Amini, Cont and Minca (Resilience to contagion in financial networks, Mathematical Finance 2016) proved that on a configuration-model network the final fraction of failed nodes concentrates, as the network grows, around an explicit value determined by the smallest fixed point of a one-dimensional map.

In that model thresholds are fixed. In practice institutions recover while a crisis unfolds: capital is raised, earnings accrue, and a node that survives long enough can absorb more losses than at the start. Amini, Minca and Sulem (A Dynamic Contagion Risk Model with Recovery Features, Mathematics of Operations Research 2022; the mission follows the authors' preprint of February 2021) add this recovery feature: every surviving node's threshold grows linearly in calendar time, at a rate proportional to its connectivity. The main result, Theorem 5, identifies the scaling limit of the cascade with growth. It is the basis of the paper's analysis of equilibrium connectivity choice (§3), where agents trade off the rewards of links against contagion risk.

Setting

A network has $n$ nodes. Node $i$ has a connectivity $\lambda_i\in\mathbb N$ (in-degree and out-degree both equal $\lambda_i$) and an integer initial threshold $\theta_i\in\mathbb N$. The empirical type distribution is $\mu^{(n)}_{\lambda,\theta}=\#\{i:\theta_i=\theta,\lambda_i=\lambda\}/n$ and the mean connectivity is $\bar\lambda^{(n)}=\sum_{\lambda,\theta}\lambda\mu^{(n)}_{\lambda,\theta}$. Two regularity conditions are assumed: (C1) $\mu^{(n)}_{\lambda,\theta}\to\mu_{\lambda,\theta}$ for a probability distribution $\mu$ on $\mathbb N^2$; (C2) $\bar\lambda^{(n)}\to\bar\lambda=\sum\lambda\mu_{\lambda,\theta}\in(0,\infty)$.

Each node owns $\lambda_i$ out-going and $\lambda_i$ in-coming half-edges. The directed configuration model matches out-half-edges to in-half-edges by a uniformly random bijection; self-loops and multiple links are allowed.

The cascade: at time $0$ the nodes with $\theta_i=0$ fail. Interactions happen at times $T^{(n)}_k$ whose gaps are i.i.d. exponential with rate $n$. At each interaction one unrevealed out-link of a failed node, chosen uniformly, is revealed; its counterparty $j$ gains one failed link and fails if its count of failed links reaches its current threshold $\theta_j+\alpha\lambda_jT^{(n)}_k/\bar\lambda^{(n)}$, where $0<\alpha<1$ is the growth rate. Only surviving nodes grow. The cascade stops at $k^{(n)}_{\rm stop}$, when no unrevealed failed link remains; $|\mathcal D^{(n)}_f|$ is the number of failed nodes and $S^{(n)}_{\lambda,\theta}(k^{(n)}_{\rm stop})$ the number of survivors of type $(\lambda,\theta)$.

The limit objects: $P_{\lambda,\theta,\ell}(\pi)$ is the probability that the order statistics of $\ell$ i.i.d. uniform variables on $[0,\pi]$ satisfy $U_{(u)}>(u-\theta)/(\alpha\lambda)$ for $u=\theta+1,\dots,\ell$; $B^\alpha_{\lambda,0}=1$ and, for $\theta\ge1$,

$$B^\alpha_{\lambda,\theta}(\pi)=1-\sum_{\ell=0}^{\min\{\lceil\theta+\alpha\lambda\pi\rceil-1,\lambda\}}\binom{\lambda}{\ell}\pi^\ell(1-\pi)^{\lambda-\ell}P_{\lambda,\theta,\ell}(\pi);$$

$J^\alpha(\pi)=\sum_{\lambda,\theta}\lambda\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(\pi)/\bar\lambda$; and the relaxed fixed point $\pi^*=\min\{\pi\in[0,1]:J^\alpha(\pi)\le\pi\}$.

Formalization targets

Goal: Theorem 5 (corrected)

With $L=\sum_{\lambda,\theta}\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(\pi^*)$: for every $\varepsilon>0$, with high probability $|\mathcal D^{(n)}_f|/n\ge L-\varepsilon$. (i) If $\pi^*=1$ and $\mu_{0,\theta}=0$ for $\theta\ge1$, then $|\mathcal D^{(n)}_f|/n\to1$ in probability. (ii) If $\pi^*<1$ is a stable fixed point ($J^\alpha(\pi)<\pi$ just to the right of $\pi^*$), then

$$\frac{|\mathcal D^{(n)}_f|}{n}\xrightarrow{p}L,\qquad\frac{S^{(n)}_{\lambda,\theta}(k^{(n)}_{\rm stop})}{n}\xrightarrow{p}\mu_{\lambda,\theta}\big(1-B^\alpha_{\lambda,\theta}(\pi^*)\big).$$

Milestones

1. Lemma 16: a recursion in $\ell$ for $P_{\lambda,\theta,\ell}(t)$, for $0<\alpha<1$ and $\theta<\ell\le\lambda$, valid for $t\ge\hat t_{\lambda,\theta,\ell}=(\ell-\theta)\bar\lambda/(\alpha\lambda)$.
2. Lemma 15: for $0<\alpha<1$ and $0<\theta\le\lambda$, the piecewise linear system (DE) for the rescaled numbers of surviving nodes with $\ell$ failed links has a unique continuous solution on $[0,\bar\lambda)$, in closed form.
3. (24)–(25): the limiting failed fraction of a class is $\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(t/\bar\lambda)$, and the limiting number of unrevealed failed links is $\bar\lambda(J^\alpha(t/\bar\lambda)-t/\bar\lambda)$.
4. (27)–(28): for $k=\gamma\bar\lambda^{(n)}n+o(n)$, $T^{(n)}_k\to\gamma\bar\lambda$ in probability.
5. Remark 6: the minimum defining $\pi^*$ is attained.

Significance

Theorem 5 gives the final size of a cascade with recovery as an explicit function of the type distribution and the growth rate. The paper uses it to define each agent's expected reward as a function of its connectivity and to study the equilibrium of the resulting connectivity game (§3). Without the theorem, the equilibrium analysis would rest on the heuristic of §2.3 alone.

On the formal side, the platform has no random graph model of configuration type, no network contagion process and no fluid limit of a random cascade. This mission introduces all three. The result is proved on paper (by Wormald's differential-equation method); none of it is machine-checked. The work is to formalize the proof, and the milestones are self-contained pieces of it: an order-statistic identity, an explicit ODE solution, an algebraic identification of the limit, a concentration bound for sums of exponentials, and a fixed-point existence result.

Difficulty

The obvious approach is to view the cascade as a Markov chain in the counts of surviving nodes by type and number of failed links, and to apply Wormald's theorem directly. Two things break. First, with growth a node's survival depends on the whole history of its failed-link count, not on its current value, so the state space grows with time: new states become relevant at each growth time $\hat t_{\lambda,\theta,\ell}$, and the fluid limit has to be established inductively on successive time intervals. Second, the cascade stops at a random time, near the first zero of the limiting number of unrevealed failed links. Showing that the stopping time concentrates requires the stability condition on $\pi^*$ and a truncation of the type distribution in the degree, since $\mu$ may have infinite support. The fixed point need not be a crossing point of a smooth map, so the identification of the stopping time is delicate even when the drift is known.

Formalization scope

• Network. Half-edges of node $i$ are pairs $(i,a)$ with $a<\lambda_i$; the matching is a uniformly random permutation of the half-edges. Each $n$ has its own probability space: the matching, $m=n\bar\lambda^{(n)}$ i.i.d. $\mathrm{Exp}(n)$ gaps, and $m$ i.i.d. uniform variables on $[0,1)$ that choose the revealed link (uniform among the available ones given the past). The probability of an event averages over permutations the product law of gaps and choices. "With high probability" and "in probability" are stated with explicit $\varepsilon$ and limits of these probabilities.
• Cascade. Computed step by step from the randomness and run for $m$ steps; $|\mathcal D^{(n)}_f|$ and $S^{(n)}_{\lambda,\theta}(k_{\rm stop})$ are read off the final state. A node fails when its failed links reach (not exceed) its threshold, as in every formula of the paper. Initially failed nodes are those with $\theta_i=0$.
• Limit objects. Order statistics are encoded by counting ($U_{(u)}>s$ iff fewer than $u$ variables are $\le s$), and probabilities as Lebesgue measures of subsets of $[0,\pi]^\ell$. Sums over types are tsums with summability hypotheses; $\mu$ is nonnegative with total mass $1$.
• Corrections, all labelled. (a) $B^\alpha_{\lambda,0}:=1$; the printed formula gives a value below $1$ for $\pi>0$, contradicting the paper's p. 9, and makes the theorem false. (b) Part (i) assumes no isolated nodes with a positive threshold. (c) Lemma 16 assumes $t\ge\hat t_{\lambda,\theta,\ell}$. (d) Lemma 15 is stated for $0<\theta\le\lambda$, with uniqueness among continuous solutions, and reads the printed $\bar\lambda-u$ as $\bar\lambda-t$. (e) (24) ends in $\mu_{\lambda,\theta}B^\alpha_{\lambda,\theta}(t/\bar\lambda)$, not $\mu_{\lambda,\theta}(1-B^\alpha_{\lambda,\theta}(t/\bar\lambda))$. "Stable fixed point" means $J^\alpha(\pi)<\pi$ on some interval $(\pi^*,\pi^*+\eta)$.
• No trivialization. $|\mathcal D^{(n)}_f|$ and $S^{(n)}_{\lambda,\theta}$ are computed from the random matching, the gaps and the revelation order, never from $B^\alpha$ or $J^\alpha$; $\pi^*$ is defined from $\mu$ and $\alpha$, not taken as a parameter.
• Not included. Theorem 3 (the case $\alpha=0$, cited from earlier work), the equilibrium results of §3, Wormald's theorem (Lemma 17, an external result), the in/out-degree extension (Theorem 18) and the displays (32)–(41) of the inductive argument.
• Infrastructure. A complete proof needs Wormald's differential-equation method for Markov chains with bounded increments, concentration of the configuration model, and the elementary facts in the milestones. A general Wormald theorem and the configuration model are reusable well beyond this mission; contributions of either, as separate theorems, are welcome.

Selected references

• H. Amini, A. Minca, A. Sulem, A dynamic contagion risk model with recovery features, Mathematics of Operations Research, 2022 (preprint February 2021). https://doi.org/10.1287/moor.2021.1174
• H. Amini, R. Cont, A. Minca, Resilience to contagion in financial networks, Mathematical Finance, 2016. https://doi.org/10.1111/mafi.12051
• N. C. Wormald, Differential equations for random processes and random graphs, Annals of Applied Probability, 1995. https://doi.org/10.1214/aoap/1177004612
• L. Warnke, On Wormald's differential equation method, arXiv:1905.08928, 2019. https://arxiv.org/abs/1905.08928
• B. Bollobás, A probabilistic proof of an asymptotic formula for the number of labelled regular graphs, European Journal of Combinatorics, 1980. https://doi.org/10.1016/S0195-6698(80)80030-8

Motivation

In prediction from experts (PFE), an online learner chooses one of $n$ actions in each of $T$ rounds, and an adversary assigns each action a loss in $[0,1]$. Performance is measured by regret, the learner's total loss minus that of the best single action in hindsight. In many applications changing the action is itself costly: re-routing traffic, re-balancing a portfolio, re-deploying a model. The number of switches, rounds in which the action changes, is then a second resource to keep small.

It has long been known that both quantities can be kept at $O(\sqrt{T\log n})$ in expectation. Kalai and Vempala's multiplicative Follow the Perturbed Leader (Kalai–Vempala 2005) and Devroye, Lugosi and Neu's random-walk perturbation (Devroye et al. 2015) both achieve this. Devroye et al. asked for guarantees that hold with high probability. A bound in expectation says little about a single run: the switch count of these algorithms can have heavy upper tails. Altschuler and Talwar (arXiv:1803.01548, COLT 2018; Mathematics of Operations Research 2021) gave the first algorithms whose regret and switches are both $O(\sqrt{T\log n\log(1/\delta)})$ with probability $1-\delta$. They used this to characterise the optimal regret under a hard switching budget, both for PFE and for multi-armed bandits.

Setting

A loss sequence is $(\ell_t)_{t\ge1}$ with $\ell_t:[n]\to[0,1]$. The adversary is oblivious: it fixes the whole sequence before the game, independently of the learner's randomness. A randomized online algorithm $\mathcal A$ draws internal randomness $\omega$ from a probability space $(\Omega,\mu)$. At round $t$ it plays an action $i_t\in[n]$ that is a function of $\omega$ and of the past losses $\ell_1,\dots,\ell_{t-1}$ only. This is full-information feedback: after round $t$ the whole vector $\ell_t$ is revealed. Then

$$\mathrm{Regret}_T=\sum_{t=1}^T\ell_t(i_t)-\min_{i\in[n]}\sum_{t=1}^T\ell_t(i),\qquad \mathrm{Switches}_T=\#\{t\in\{2,\dots,T\}:i_t\ne i_{t-1}\}.$$

Follow the Perturbed Leader (FPL) with perturbations $P_t(i)$ plays at round $t$ the minimiser of $\sum_{s=0}^{t-1}(\ell_s(i)+P_{s+1}(i))$, with $\ell_0:=0$. FPL$^*_\varepsilon$ perturbs only once, with $P_1(i)=-R(i)/\varepsilon$, where $R(1),\dots,R(n)$ are i.i.d. standard exponential.

Framework 1 turns an algorithm $\mathcal A$ into a batched algorithm $\mathcal B$. $\mathcal B$ runs a copy of $\mathcal A$ with fresh randomness. The copy sees only the losses since its epoch began. The epoch ends just before the copy would exceed $S'$ switches, and a new copy starts there. $E$ is the number of epochs used in $T$ rounds. BFPL$^*_\delta$ is Framework 1 applied to FPL$^*_\varepsilon$ with

$$N=\lceil\log(2/\delta)\rceil,\qquad \varepsilon=\tfrac12\sqrt{N\log n/T},\qquad S'=135\sqrt{T\log n/N}.$$

Formalization targets

Goal: Theorem 1 (p. 8)

There is an absolute constant $C>0$ such that for all $T,n\ge1$ and $\delta\in(0,\tfrac12)$ some randomized online algorithm $\mathcal A$ satisfies, for every oblivious loss sequence,

$$\mathbb P\Big(\mathrm{Regret}_T(\mathcal A)\le C\sqrt{T\log n\log(1/\delta)}\ \wedge\ \mathrm{Switches}_T(\mathcal A)\le C\sqrt{T\log n\log(1/\delta)}\Big)\ge1-\delta.$$

The algorithm may depend on $T$, $n$ and $\delta$, as on the page, but not on the losses. The constant is left unspecified, so a sharper constant would not change the goal.

Milestones

1. Lemma 7 (p. 13): $\mathbb E[\mathrm{Switches}_\tau(\mathrm{FPL}^*_\varepsilon)]\le(\varepsilon\tau+2\log n)/(1-\varepsilon)$.
2. Lemma 3 (p. 10): if $\mathbb E[\mathrm{Switches}_{\tau_0}(\mathcal A)]\le c_{\mathcal A}\sqrt{\tau_0}$ with $\tau_0=\min(T,\lceil8T/N\rceil)$, then Framework 1 with $S'=23c_{\mathcal A}\sqrt{T/N}$ has $\mathbb P(E>N)\le e^{-N}$ and $\mathbb P(\mathrm{Switches}_T>N(S'+1))\le e^{-N}$.
3. Lemma 17 (p. 27), Be-The-Leader: $\sum_{t=0}^T\ell_t(i_{t+1})\le\sum_{t=0}^T\ell_t(i)$.
4. Lemma 5 (p. 13): $\mathrm{Regret}_T(\mathrm{FPL})\le M(\mathrm{Switches}_T+1)+\max_i\sum_{t=1}^{T+1}P_t(i)-\sum_{t=1}^{T+1}P_t(i_t)$.
5. Corollary 6 for BFPL$^*$ (p. 14): $\mathrm{Regret}_T\le\mathrm{Switches}_T+E+\sum_{e<E}\max_iR_e(i)/\varepsilon$.
6. Lemma 18 (p. 28): $\mathbb E[e^{tX}]\le n^t/(1-t)$ for the maximum $X$ of $n$ standard exponentials.
7. Lemma 9 (p. 14): $\mathbb P(\sum_{e=1}^N\max_iR_e(i)>6N\log n)\le e^{-N}$ for $N,n\ge2$.
8. Theorem 8 (p. 13): BFPL$^*_\delta$ itself satisfies the bound of Theorem 1 for $n\ge2$.

Significance

The result separates two notions of "optimal". Expected-value bounds on switching do not control a single run, and the paper shows (Appendix B) that naive restarting does not concentrate. Theorem 1 is the black box behind the paper's later results: the $\tilde\Theta$ characterisation of minimax regret under a switching budget $S$, with a phase transition at $S\approx\sqrt{T\log n}$, and the switching-cost corollary obtained by mini-batching. Framework 1 is generic: any algorithm with an expected switching bound of order $\sqrt\tau$ gains a high-probability one.

The paper result is proved, but none of it has been machine-checked. A formalization yields a verified online-learning protocol with oblivious adversaries, a restart framework with fresh randomness, and verified tail bounds for maxima of exponentials. Formalizing it also repairs four printed slips, listed under Formalization scope.

Difficulty

The obvious approach runs $\mathcal A$ about $\log(1/\delta)$ times in fixed-length blocks and applies Markov's inequality in each. It fails: a single block can use far too many switches with probability that is not small enough. Framework 1 therefore uses epochs of random length, ended by the switch budget. The epoch lengths are then dependent, and the final epoch is truncated at $T$. The concentration argument has to handle both. On the regret side, Lemma 5 is pointwise, but summing it over random epochs and then controlling the sum of perturbation maxima needs a sub-exponential tail bound for maxima of exponentials.

Formalization scope

Rounds are 1-based, and losses are $\ell:\mathbb N\to\mathrm{Fin}\,n\to\mathbb R$ with values in $[0,1]$. An online algorithm has type $\Omega\to(t:\mathbb N)\to(\mathrm{Fin}(t-1)\to\mathrm{Fin}\,n\to\mathbb R)\to\mathrm{Fin}\,n$: at round $t$ it sees only $\omega$ and $\ell_1,\dots,\ell_{t-1}$. The adversary is a deterministic loss sequence, quantified after the algorithm, which is the page's own reduction (p. 5). High-probability statements bound the outer measure of the failure event by $\delta$. Expectations are lower Lebesgue integrals of natural-valued switch counts. The $O(\cdot)$ of Theorems 1 and 8 is an absolute constant $C>0$ chosen before $T$, $n$ and $\delta$. Argmins break ties towards the lowest index. Framework 1 takes randomness $\omega:\mathbb N\to\Omega$ under the infinite product measure, one coordinate per epoch.

Three formalizations of the goal would be trivial, and all are excluded. An algorithm that could see $\ell_t$ or the future would simply play the best action in hindsight. A constant $C$ chosen after $T$ could be $C=T$. A loss sequence chosen before the algorithm would let the algorithm depend on it.

The printed slips and how they are handled:

• FPL* sign. The paper perturbs by $+R/\varepsilon$. With one-sided exponentials that variant violates Lemma 7, so the perturbation is $-R/\varepsilon$.
• Lemma 5 and Corollary 6. These need $M(\mathrm{Switches}_T+1)$ and $+E$; the printed forms fail at $T=1$.
• Lemma 3. It takes an integer $N\ge2$ with $\delta/2=e^{-N}$, it assumes the switching hypothesis only at the horizon the proof uses, and it counts one boundary switch per epoch.
• BFPL$^*_\delta$. It uses $N=\lceil\log(2/\delta)\rceil$.
• Measurability. Lemma 3 assumes that $\mathcal A$'s actions are measurable in $\omega$.

The development needs:

• product and infinite-product measures of exponential laws (in Mathlib);
• Markov's inequality and Azuma–Hoeffding for submartingales with bounded differences;
• the memoryless property of the exponential law;
• Chernoff bounds.

The online-learning layer (protocol, regret, switches, FPL, the restart framework) is reusable for other switching-cost results in the paper and elsewhere. Proofs of any milestone are welcome, as are alternative routes to Theorem 1, such as the random-walk perturbation of §2.5.

Selected references

• J. M. Altschuler and K. Talwar, Online learning over a finite action set with limited switching, COLT 2018; Mathematics of Operations Research 46(1), 2021. arXiv:1803.01548v2
• A. Kalai and S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3), 2005. doi:10.1016/j.jcss.2004.10.016
• L. Devroye, G. Lugosi and G. Neu, Random-walk perturbations for online combinatorial optimization, IEEE Transactions on Information Theory 61(7):4099–4106, 2015. doi:10.1109/TIT.2015.2428253
• N. Cesa-Bianchi and G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. doi:10.1017/CBO9780511546921

Motivation

Many systems studied in operations research and reinforcement learning are modelled as finite Markov chains with a large number of states $p$: the stops of a taxi in a city, a random walk on a network, the conformations of a molecule. Estimating the $p\times p$ transition matrix from one observed trajectory needs, in general, a trajectory long compared with the $p^2$ unknown entries. In many such systems the transition matrix has, at least approximately, a small rank $r\ll p$: the observed chain is driven by a low-dimensional latent process, as in state aggregation, where $\mathbb P(s_{t+1}\mid s_t)=\sum_z\mathbb P(z_t=z\mid s_t)\,\mathbb P(s_{t+1}\mid z_t=z)$ (Zhu, Li, Wang & Zhang, arXiv:1907.00113, §1.1). Zhu, Li, Wang and Zhang show that a low-rank transition matrix can be estimated from a trajectory whose length is proportional to $p$ (up to logarithmic factors), and they give two maximum-likelihood estimators with explicit rates. This mission formalizes the rate of the second, rank-constrained, estimator in Kullback–Leibler divergence.

Setting

Let $X_0,X_1,\dots,X_n$ be a Markov chain on the states $[p]=\{s_1,\dots,s_p\}$ with transition matrix $P$ ($P_{ij}\ge0$, $\sum_jP_{ij}=1$, $P_{ij}=\mathbb P(X_1=s_j\mid X_0=s_i)$) and stationary distribution $\pi$ ($\pi^\top P=\pi^\top$). The chain is primitive (some power of $P$ has all entries positive), and $X_0$ is drawn from $\pi$. Write $\pi_{\min}=\min_j\pi_j$ and $\pi_{\max}=\max_j\pi_j$.

The right spectral gap is $1-\rho_+$, where, with $\langle h_1,h_2\rangle_\pi=\sum_jh_{1j}h_{2j}\pi_j$ and the adjoint $P^*=\mathrm{Diag}(\pi)^{-1}P^\top\mathrm{Diag}(\pi)$,

$$\rho_+=\sup_{\langle h,1\rangle_\pi=0,\ \langle h,h\rangle_\pi=1}\tfrac12\langle(P+P^*)h,h\rangle_\pi .$$

The KL divergence of a transition matrix $Q$ from $P$ is $D_{\mathrm{KL}}(P,Q)=\sum_{i,j}\pi_iP_{ij}\log(P_{ij}/Q_{ij})1_{\{P_{ij}\ne0\}}$. From the trajectory, $n_{ij}$ counts the transitions $s_i\to s_j$, and the averaged negative log-likelihood is $\ell_n(Q)=-\frac1n\sum_{i,j}n_{ij}\log Q_{ij}$. The empirical KL divergence is $\widetilde D_{\mathrm{KL}}(P,Q)=\ell_n(Q)-\ell_n(P)$.

Assumption 1 of the paper: $\operatorname{rank}(P)=r$, and $P_{jk}\in\{0\}\cup[\alpha/p,\beta/p]$ for constants $\alpha,\beta>0$. The $(\alpha/p)$-minoration (Remark 2) removes the $0$: $\alpha/p\le P_{jk}\le\beta/p$ for all $j,k$. The rank-constrained MLE (5) is any

$$\widehat P^r\in\arg\min\big\{\ell_n(Q):\ Q1_p=1_p,\ \alpha/p\le Q_{ij}\le\beta/p,\ \operatorname{rank}(Q)\le r\big\}.$$

In Lean these objects are IsStochastic, IsStationary, IsPrimitive, piMin, piMax, trajProb, rhoPlus, klDiv, negLogLik, empKL, Assumption1, Minorated, RankFeasible and IsRankMLE in the namespace LowRankMarkov.RankMLE.

Formalization targets

Goal: Theorem 2, KL display (p. 10)

There are universal constants $C_1,C_2>0$ such that, for $p\ge2$, under minoration with $\operatorname{rank}P=r$ and $n\pi_{\max}(1-\rho_+)>\max(20\log p,\log n)$, every rank-constrained MLE satisfies, for all $\xi>0$,

$$\mathbb P\Big\{D_{\mathrm{KL}}(P,\widehat P^r)\ge\max\Big(\frac{C_1r\pi_{\max}\beta^2p\log p}{\pi_{\min}\alpha^3n},\ \frac{\xi\pi_{\min}}{rp\pi_{\max}\log p}\Big)\Big\}\le C_2e^{-\xi}.$$

The constants are not fixed numerically, so a sharper analysis does not invalidate the goal.

Milestones

1. Lemma EC.1, both forms: $D_{\mathrm{KL}}(u,v)\ge\frac{p\alpha}{2\beta^2}\|u-v\|_2^2$ for distributions with $u_j\in\{0\}\cup[\alpha/p,\beta/p]$, $v_j\in[\alpha/p,\beta/p]$, and its matrix form $\|P-Q\|_F^2\le\frac{2\beta^2}{\alpha\pi_{\min}p}D_{\mathrm{KL}}(P,Q)$.
2. The rank remark (p. 14): $\operatorname{rank}(\widehat P^r-P)\le2r$ and $\|\widehat P^r-P\|_*\le(2r)^{1/2}\|\widehat P^r-P\|_F$.
3. (EC.14): on the shell $Q\in\mathcal C(\eta)$, $l\ge1$ and $2^{l-1}\eta\le D_{\mathrm{KL}}(P,Q)\le2^l\eta$, $\|Q-P\|_*\le2\beta(2^l\eta r/(p\alpha\pi_{\min}))^{1/2}$.
4. (EC.15), (EC.17): Bernstein-type tails $p^{-(\xi-1)}$ for $W^{(1)}_n=\max_j\sum_{i\le n}P_{X_{i-1},j}$ and $W^{(2)}_n=\max_j\sum_{i\le n}1_{\{X_{i-1}=s_j\}}$.
5. Lemma 3: with probability at least $1-C_2\exp(-\eta\pi_{\max}rp\log p/\pi_{\min})$, $|\widetilde D_{\mathrm{KL}}(P,Q)-D_{\mathrm{KL}}(P,Q)|\le\frac12D_{\mathrm{KL}}(P,Q)+C_1\pi_{\max}\beta^2rp\log p/(\pi_{\min}\alpha^3n)$ for every $Q\in\mathcal C$ with $D_{\mathrm{KL}}(P,Q)\ge\eta$.
6. (EC.3): $\widetilde D_{\mathrm{KL}}(P,\widehat P^r)\le0$. Together with $D_{\mathrm{KL}}(P,\widehat P^r)=\mathcal L(\widehat P^r)-\mathcal L(P)$ it gives (EC.4), $D_{\mathrm{KL}}(P,\widehat P^r)\le D_{\mathrm{KL}}(P,\widehat P^r)-\widetilde D_{\mathrm{KL}}(P,\widehat P^r)$.

Significance

The bound says that, with high probability, the KL error of $\widehat P^r$ is of order $rp\log p/n$ up to the factors $\pi_{\max}/\pi_{\min}$ and $\beta^2/\alpha^3$, plus a term independent of $n$ controlled by $\xi$. A trajectory of length of order $rp\log p$, rather than $p^2$, therefore suffices: the low rank is what makes the estimation problem sample-efficient. Lemma EC.1 converts the KL bound into a Frobenius-norm bound, and Lemma 3 is a uniform law for the empirical KL process of a dependent sequence over the paper’s cone class.

The result is proved in the paper; nothing in it has been machine-checked. The mission asks for a formal proof of the KL display. Two points need care beyond transcription: the printed hypotheses do not suffice (see Formalization scope), and the paper's proof of Lemma 3 symmetrizes the dependent summands as if they were independent (EC.8), so a formal proof must supply a valid argument for that step.

Difficulty

Comparing $\ell_n(\widehat P^r)$ with $\ell_n(P)$ is immediate; the difficulty is to control $\widetilde D_{\mathrm{KL}}-D_{\mathrm{KL}}$ uniformly over a non-convex set of matrices, from one dependent trajectory. A union bound over a net of the feasible set loses polynomial factors in $p$, and i.i.d. empirical-process tools do not apply directly to a Markov chain. The printed Lemma 3 covers the cone class $\mathcal C$, while the appendix proof restricts its shells to rank-$r$ matrices. This leaves a gap for matrices in $\mathcal C$ of higher rank and for the claimed application to $\widehat P^r$ when $r>16$. The paper combines a tail inequality for suprema of empirical processes of Markov chains (Adamczak 2008), a contraction step, the matrix Freedman inequality (Tropp 2011) for a matrix martingale, and a Bernstein inequality for Markov chains with a spectral gap (Jiang, Fan & Sun 2018) for the quadratic variations $W^{(1)}_n,W^{(2)}_n$. None of these is in Mathlib.

Formalization scope

States are Fin p, matrices Matrix (Fin p) (Fin p) ℝ, logarithms natural. A trajectory $x=(X_0,\dots,X_n)$ makes $n$ transitions, and its probability is $\pi(x_0)\prod_{k<n}P_{x_kx_{k+1}}$; probabilities of events are finite sums, so no measure theory is needed. $\rho_+$ is a real sSup; "$\rho_+<1$" is not built into its definition. The nuclear and Frobenius norms come from the published definition CaiCandesShen.Convergence.Basic.

Hypotheses fixed relative to the page:

• Minoration instead of Assumption 1(ii), in the goal and (EC.3). The printed Theorem 2 allows $P_{jk}=0$, and it is false then. For even $p$, let rows $1,\dots,p/2$ of $P$ equal $2/p$ on columns $p/2+1,\dots,p$ and $0$ elsewhere, and rows $p/2+1,\dots,p$ equal $1/p$. Then $\operatorname{rank}P=2$, $\alpha=1$, $\beta=2$, $\rho_+=0$, $\pi$ puts mass $1/3$ on the first half and $\pi_{\max}/\pi_{\min}=2$. Every feasible $Q$ has $Q_{ij}\ge1/p$, so on each of the first $p/2$ rows $Q$ puts mass at most $1/2$ on the support of $P$, and $D_{\mathrm{KL}}(P,Q)\ge\frac13\log2$. With $\xi=0.9\,p\log p$ the threshold is below $\frac13\log2$ for all large $n$, so the probability is $1$, while $C_2e^{-\xi}<1$ for large $p$. The broken step is (EC.3), which needs $P$ feasible for (5); minoration with $\operatorname{rank}P=r$ makes it feasible. Lemma EC.1, (EC.14), (EC.15), (EC.17) and Lemma 3 keep the printed Assumption 1.
• $X_0\sim\pi$, stated in Theorem 1 and used by the proof of Theorem 2 through Lemma 3.
• Ergodic is read as primitive; $\pi_i>0$ is stated (it is implied); $p\ge2$ keeps $\log p>0$ in denominators.
• Lemma 3's set is the printed $\mathcal C(\eta)$, whose cone is $\|Q-P\|_*\le4\times2^{1/2}\|Q-P\|_F$ and which has no rank constraint. The appendix proof uses rank-restricted shells; for $r>16$ the rank remark alone does not place $\widehat P^r$ in $\mathcal C$. This is a proof gap, while the formal statement retains the page's quantification.
• Lemma EC.1's matrix form and (EC.14) include the printed cone condition. (EC.14) is stated pointwise for members of $\mathcal C_l$.

The statements rule out trivializing readings: $C_1,C_2$ are quantified before all data; the goal holds for every selection of minimizers, not for one fixed estimator; $p\ge2$ and $\pi>0$ exclude the junk values $x/0=0$ and $\log1=0$ that would collapse the thresholds; a sorry-free check shows the goal's hypotheses are jointly satisfiable ($p=2$, uniform $P$, $n=28$).

Not posed: Theorem 1 (nuclear-norm MLE), the Frobenius display of Theorem 2 (Lemma EC.1 turns the KL threshold into twice the printed Frobenius threshold, so the paper's one-line derivation gives $C_2e^{-\xi/2}$), Theorem 3 (lower bound), and the DC-programming results of §4. Useful reusable contributions: a Bernstein inequality for finite Markov chains with a spectral gap, the matrix Freedman inequality, and the reverse-Pinsker bound of Lemma EC.1.

Selected references

• Z. Zhu, X. Li, M. Wang, A. R. Zhang, Learning Markov models via low-rank optimization, Operations Research, 2022; preprint arXiv:1907.00113v2, 2020. https://arxiv.org/abs/1907.00113
• B. Jiang, J. Fan, Q. Sun, Bernstein's inequality for general Markov chains, arXiv:1805.10721, 2018. https://arxiv.org/abs/1805.10721
• J. A. Tropp, Freedman's inequality for matrix martingales, Electronic Communications in Probability 16:262–270, 2011. https://arxiv.org/abs/1101.3039
• R. Adamczak, A tail inequality for suprema of unbounded empirical processes with applications to Markov chains, Electronic Journal of Probability 13(34):1000–1034, 2008. https://arxiv.org/abs/0709.3110
• J. A. Fill, Eigenvalue bounds on convergence to stationarity for nonreversible Markov chains, with an application to the exclusion process, The Annals of Applied Probability 1(1):62–87, 1991. https://doi.org/10.1214/aoap/1177005981

Motivation

Asset managers increasingly buy alternative data: satellite images, credit-card panels, web traffic. Raw data of this kind is worthless until someone has the skills to process it, and those skills are costly and uncertain to acquire. A fund can hire data scientists and still find that its models extract little. Huang, Xiong and Yang (Management Science, 2022) build an equilibrium model of a data seller who sells to investors who must first acquire such skills. They ask how the cost of acquiring skills feeds through the data market into the financial market: into how much the price reveals, the cost of capital and return volatility.

The model joins two lines of work. One is the classical noisy rational-expectations market of Grossman and Stiglitz (1980), in which prices partly reveal private information. The other is the literature on selling information started by Admati and Pfleiderer (1986, 1990), in which a monopolist seller degrades the information it sells to limit what the price leaks. The new feature is the "gold rush" of skill acquisition: an investor who pays the cost learns only afterwards whether her skill is high or low.

Setting

A risky asset pays $\tilde\theta\sim N(0,\tau_\theta^{-1})$ and there is noise demand $\tilde u\sim N(0,\tau_u^{-1})$. A data seller observes $\tilde\theta+\tilde\eta$ with $\tilde\eta\sim N(0,\tau_\eta^{-1})$; the precision $\tau_\eta$ is the data accuracy. The seller chooses a clarity $x\in(0,\infty]$ and passes the data with personalized noise, so that a buyer of skill $z$ receives a signal of precision $xz$ about $\tilde\theta+\tilde\eta$. The value $x=\infty$ means the data are sold "as is".

A continuum of CARA investors with risk aversion $\gamma$ is indexed by $i\in[0,1]$. Investor $i$ can acquire data-processing skills at cost $C(c,i)$, where $c>0$ is a cost parameter. The cost is continuous and strictly increasing in $i$, with $C(c,0)=0$ and $C(c,i)\to\infty$ as $i\to1$, and it is strictly increasing in $c$. A skilled investor turns out high-skilled ($Z_H$) or low-skilled ($Z_L$) with probability $\tfrac12$ each, with $0<Z_L<Z_H$. A mass $\lambda$ of investors becomes skilled.

In the asset market, the price reveals $\tilde\theta+\tilde\eta$ with precision $\alpha^2\tau_u$, and $\alpha$ is pinned down by the market-clearing equation (14). Skilled investors buy the data at a Nash-bargained price $q=\beta G$, where $G(x,\alpha)$ is the certainty-equivalent trading gain (15) and $\beta\in(0,1)$ is the seller's bargaining power. Investors acquire skills until the marginal investor is indifferent, $(1-\beta)G(x,\alpha)=C(c,\lambda)$ (19). The seller chooses $x$ to maximize the profit $\lambda q$. An equilibrium is a clarity $x^*$ with its $(\lambda^*,\alpha^*)$ such that no other feasible clarity gives more profit.

The market outcomes are:

• the data price $q^*$;
• price informativeness $1/\operatorname{Var}(\tilde\theta\mid\tilde p)$;
• the cost of capital $E(\tilde\theta-\tilde p)$;
• return volatility $\sigma(\tilde\theta-\tilde p)$;
• skilled investors' performance, the average certainty-equivalent advantage (21) of a skilled over an unskilled investor.

Formalization targets

Goal: Proposition 5

Fix $0<c_1<c_2$. There is a threshold $T$ such that, for every data accuracy $\tau_\eta\ge T$ and every pair of equilibria at $c_1$ and $c_2$, both clarities are finite and

$$\lambda^*_2<\lambda^*_1,\quad x^*_1<x^*_2,\quad q^*_1<q^*_2,\quad \frac{1}{\operatorname{Var}_1(\tilde\theta\mid\tilde p)}<\frac{1}{\operatorname{Var}_2(\tilde\theta\mid\tilde p)},$$ $$E_2(\tilde\theta-\tilde p)<E_1(\tilde\theta-\tilde p),\quad \sigma_2(\tilde\theta-\tilde p)<\sigma_1(\tilde\theta-\tilde p),\quad \mathrm{Performance}_1<\mathrm{Performance}_2 .$$

The paper writes these as signs of derivatives in $c$. The goal states them as comparisons between two cost levels, which is what the prose of the proposition asserts.

Milestones

1. Proposition 1: for given $(\lambda,x)$, equation (14) has a unique positive root $\alpha$.
2. Proof of Proposition 2: for each finite clarity $x$, a unique $(\lambda,\alpha)$ solves (14) and (19).
3. Proposition 2 (1): an equilibrium exists.
4. (C5): on feasible tuples the profit equals $\beta\lambda C(c,\lambda)/(1-\beta)$.
5. Proposition 3: in equilibrium, $x^*<\infty$ if $\lambda^*\tau_\eta>\alpha^*\gamma$ and $x^*=\infty$ otherwise.
6. The clarity limit: as $\tau_\eta\to\infty$, every solution $x$ of (14) tends to $2\alpha\gamma/(\lambda(Z_H+Z_L))$.
7. The α limit: the equilibrium $\alpha^*$ tends to $\sqrt{\tau_\theta/\tau_u}$.
8. (C18): the equilibrium $\lambda^*$ tends to a root of (C18).

Significance

The result. Proposition 5 is the paper's headline. When skills are uncertain, a rise in skill-acquisition costs makes prices more informative and lowers the cost of capital and return volatility. When skills are certain, these outcomes stay unchanged (Proposition 4). The mechanism is that the seller cannot tailor one clarity to buyers of unknown skill. To keep buyers interested as costs rise, she provides clearer data, and more information leaks into the price. The result separates the data market from a pure cost shock to information production. It gives empirical predictions for markets where skill acquisition is costlier, such as private or international equities.

Formalizing it. The proposition is proved in the paper by expansion in $w=1/\tau_\eta$ around $w=0$. A machine-checked version must make "sufficiently high $\tau_\eta$" precise, with a threshold that holds uniformly over all equilibria. It must also control the exact finite-$\tau_\eta$ equilibrium rather than its limit. The mission also contributes the first noisy rational-expectations model with a strategic data seller on the platform: posterior variances, the equilibrium equation (14), the certainty-equivalent gain, and the seller's choice between finite clarity and selling "as is". No part of the paper has been formalized before.

Difficulty

Several comparisons follow at leading order in $1/\tau_\eta$. As $\tau_\eta\to\infty$ the equilibrium mass converges to the root of (C18), which is decreasing in $c$, and the clarity, the data price and performance are, to first order, functions of that mass. The price-informativeness, cost-of-capital and volatility comparisons do not follow at leading order. At $\tau_\eta=\infty$ the ratio $\alpha^*$ tends to $\sqrt{\tau_\theta/\tau_u}$ whatever the cost, so these three outcomes are flat in $c$ to leading order. Their signs come from the $O(1/\tau_\eta)$ correction to $\alpha^*$, and the correction must be controlled jointly with the seller's optimal clarity. A newcomer's first idea is to set $\tau_\eta=\infty$ in the equilibrium conditions and differentiate. That loses exactly the term that carries the result. A further difficulty is that the seller's optimum is defined by comparison with every feasible clarity, including selling "as is", not by a first-order condition.

Formalization scope

All quantities are real numbers. The parameters satisfy $\tau_\theta,\tau_u,\gamma>0$, $0<\beta<1$, $0<Z_L<Z_H$ and $\tau_\eta>0$. Two of these go beyond the paper's §2 domains, and both are needed:

• $\beta>0$: with $\beta=0$ the profit is identically zero and every clarity is optimal;
• $Z_L>0$: this is the paper's own condition on p. 23.

The cost family is any admissible $C(c,i)$: continuous and strictly increasing in $i$ on $[0,1)$, $C(c,0)=0$, $C(c,i)\to\infty$ as $i\to1^-$, and strictly increasing in $c$ on $(0,1)$. "Increasing" in the paper is read as strictly increasing. Clarity is either a finite $x>0$ or "as is". At "as is", (14) becomes $\gamma\alpha=\lambda\tau_\eta$ and both conditional variances given a signal equal $1/(\tau_\theta+\tau_\eta)$. These are the $x\to\infty$ limits of the finite-clarity formulas. The value $x=0$ is excluded from the choice set because it gives no positive root of (14).

The posterior variances (8), (10), (12), the gain (15), the price coefficients (C1)–(C4), the cost of capital (C12), volatility (C13) and performance (21) are taken as closed-form definitions. Their CARA-normal derivation (Bayes' rule, market clearing, certainty equivalents) is not formalized. Equilibria are defined relationally: a feasible tuple whose profit is at least that of every feasible tuple, with no choice functions.

The goal concludes, rather than assumes, that the equilibrium clarities are finite. It quantifies over every equilibrium at each cost level. It does not define the equilibrium through the $\tau_\eta=\infty$ economy or through the paper's expansions, which would replace the theorem by its heuristic.

A complete development needs real analysis only: the intermediate value theorem, monotonicity, compactness on $(0,\infty]$, and asymptotics in $1/\tau_\eta$. Contributions are welcome on any milestone, on an independent proof of Proposition 4's $\Delta=0$ counterpart, and on a formal derivation of the closed forms from Gaussian conditioning and CARA utility, which would be reusable for other rational-expectations models.

Selected references

• S. Huang, Y. Xiong, L. Yang, Skill Acquisition and Data Sales, Management Science 68(8), 2022; working paper version of July 2019. https://doi.org/10.1287/mnsc.2021.4117
• S. J. Grossman, J. E. Stiglitz, On the Impossibility of Informationally Efficient Markets, American Economic Review 70(3), 1980. https://www.jstor.org/stable/1805228
• A. R. Admati, P. Pfleiderer, A Monopolistic Market for Information, Journal of Economic Theory 39(2), 1986. https://doi.org/10.1016/0022-0531(86)90049-3
• A. R. Admati, P. Pfleiderer, Direct and Indirect Sale of Information, Econometrica 58(4), 1990. https://doi.org/10.2307/2938330
• N. Gârleanu, L. H. Pedersen, Efficiently Inefficient Markets for Assets and Asset Management, Journal of Finance 73(4), 2018. https://doi.org/10.1111/jofi.12696

Why self-replicating goods

Some goods can only be made by copies of themselves. RepRap and Prusa 3D printers print the parts of new printers, seed stock is grown from seed, and livestock herds breed. For such a good the inventory is also the production capacity: a unit sold today is a unit that will not replicate tomorrow. A firm launching such a good has to decide, at every instant, how much of its stock to use for replication and how much demand to serve. Demand for an innovative good is not exogenous either. It diffuses through the market by word-of-mouth, so sales held back today also slow future demand.

B. Hu and Z. Sun (Management Science) model this as a deterministic optimal control problem. Their demand side is the Bass diffusion model (Bass, 1969) in the supply-constrained form of Ho, Savin and Terwiesch (2002) and Kumar and Swaminathan (2003), where cumulative sales rather than cumulative demand drive imitation. Hu and Sun add diminishing word-of-mouth. Their main structural result, Theorem 1, says that under a condition they call Strong Replicability the optimal policy switches only once and can be found by a one-dimensional search.

The model

Time runs over $[0,T]$, where $T$ is the life cycle. The firm controls a production rate $p(t)$ and a sales rate $s(t)$. The state consists of the cumulative demand $D(t)$, the adjusted cumulative sales $S(t)$ and the inventory $I(t)$. The demand rate is

$$d(t)=\Big[\alpha+\frac{\beta S(t)}{m}\Big]\big[m-D(t)\big],$$

where $m$ is the market size, $\alpha$ the coefficient of innovation and $\beta$ the coefficient of imitation. Problem (1) of the paper is

$$\max_{p,s}\int_0^T\big[\pi s(t)-cp(t)-hI(t)\big]e^{-\rho t}\,dt$$

subject to

$$D'=d,\quad S'=s-wS,\quad I'=p-s,\qquad 0\le p\le rI,\quad 0\le s\le d,\quad I(T)\ge0,$$ $$D(0)=S(0)=0,\qquad I(0)=I_L>0.$$

Here $\pi$ is the price, $c$ the unit replication cost, $h$ the holding cost rate, $r$ the replication rate, $\rho\ge0$ the discount rate and $w\ge0$ the rate at which word-of-mouth decays. Unmet demand is lost. The paper assumes $\pi>c$ and $r>\rho$. Production is on when $p=rI$ and off when $p=0$. Sales are on when $s=d$ and off when $s=0$.

Strong Replicability is condition (2),

$$(r-\rho)\pi>cr+h.$$

It says that letting a unit replicate for a short time and selling the offspring later is worth more than selling the unit now.

Two levels of the launch inventory organise the answer. $\underline I$ is the level at which keeping production and sales always on depletes the inventory exactly at $T$. $\overline I$ is the level at which keeping production off and sales on depletes it exactly at $T$.

Formalization targets

Goal: Theorem 1

Assume Strong Replicability. Then:

• (a) if $I_L<\underline I$, the policy that keeps production always on and switches sales on once, at the time that depletes the inventory exactly at $T$, is optimal;
• (b) if $\underline I<I_L<\overline I$, the policy that keeps sales always on and switches production on once, at the time that depletes the inventory exactly at $T$, is optimal;
• (c) if $I_L>\overline I$, the policy that keeps sales always on and production off is optimal, and it leaves inventory at $T$.

In each case, optimal means that the profit is at least

$$\int_0^T\big[\pi\tilde s-c\tilde p-h\tilde I\big]e^{-\rho t}\,dt$$

for every admissible trajectory $(\tilde D,\tilde S,\tilde I,\tilde p,\tilde s)$, not only for policies of the stated shape. The switching times are not given in closed form, and the theorem asserts only that they exist.

Milestones

1. The thresholds are ordered, $\underline I<\overline I$ (preamble of Theorem 1).
2. Proposition 1. Once production is switched on, an optimal policy keeps it on until $T$ or inventory depletion.
3. Proposition 2, first half. Under Strong Replicability, every optimal trajectory has $I(t)>0$ for all $t<T$, whatever $T$ is.

Significance

Theorem 1 turns an infinite-dimensional control problem into a choice of one switching time. Its managerial content is that a firm with a replicating good should, when stock is scarce, run replication at full capacity and hold back sales, losing some early customers, as long as the stock built up will eventually be sold. Proposition 2 says that under Strong Replicability the firm never sells out before the end of the life cycle. The paper's numerical study (§4) and its extensions (§5: backlogged demand, liquidity, stochastic diffusion) are built on this characterization.

The result has a published informal proof (pp. 36–37 of the manuscript), which applies necessary conditions from Pontryagin's maximum principle and then a perturbation and exchange argument. None of it is machine-checked. A complete formal proof would establish global optimality, against all integrable controls, for a nonlinear controlled ODE with mixed state–control constraints. That is a sufficiency statement, which the necessary conditions alone do not give.

Difficulty

The maximum principle gives necessary conditions only, and Problem (1) is not concave: the dynamics of $D$ are bilinear in $S$ and $D$, and the constraint $p\le rI$ couples control and state. So the obvious route, solving the Pontryagin system and reading off the optimum, does not prove optimality. The paper's own argument is an exchange argument. It postpones sales or shifts production forward and claims each change improves profit, and it applies the change recursively ("by making the same argument recursively"). Making it rigorous requires comparison results for the Bass system under perturbed sales, which are delicate. Postponing sales lowers the adjusted sales $S$, and with it all future demand. The existence of the switching times also needs a continuity argument on the depletion time as a function of the switch.

Formalization scope

The Lean development lives in the namespace SelfReplic.Strong and uses real numbers throughout.

• Parameters form a structure Params with fields m, price, c, h, r, alpha, beta, rho, w, T, IL. The predicate Params.Standing collects the page's assumptions $I_L>0$, $\pi>c$, $r>\rho\ge0$, $w\ge0$. It adds the sign conditions $m>0$, $T>0$, $\alpha>0$, $\beta\ge0$, $c\ge0$, $h\ge0$, which the paper uses but never states. Params.StrongRepl is condition (2).
• Admissible trajectories (IsAdmissible) have integrable controls $p,s$ and continuous states $D,S,I$ on $[0,T]$. The three ODEs hold in integral form at every $t\in[0,T]$, the constraints $0\le p\le rI$, $0\le s\le d$ hold at every $t\in[0,T]$, and $I(T)\ge0$. The integral form is used because bang-bang controls are discontinuous. Continuity and integrability prevent any integral from silently taking Lean's default value $0$. Nonnegativity of $I$ follows from $0\le p\le rI$, as on p. 8.
• Optimality (IsOptimal) compares the discounted profit with every admissible trajectory of the same parameters.
• Policy shapes are pointwise statements on $[0,T]$, and a switch instant counts as "on". The thresholds $\underline I,\overline I$ enter as real numbers with their defining property (IsLowLevel, IsHighLevel), evaluated at the same parameters with $I_L$ replaced.
• Proposition 1 is read up to null sets ("production has run before $t_0$", conclusion almost everywhere). It carries the added hypothesis $\rho c+h>0$, which the paper's proof uses. Without it ($\rho=h=0$), pausing production is costless and the statement fails.

A formalization that states Theorem 1 inside its own policy class (the best policy of shape (a) is the best of shape (a)) would be empty. Here the competitor in every case ranges over all admissible trajectories.

Not formalized: Theorem 2 (Weak Replicability), whose closed form (3) for the production interval is inexact when $\rho>0$; Corollaries 1–2; the second half of Proposition 2, which fails when $I_L\ge m$; the unnumbered bang-bang claim of p. 9; Propositions 3–4 (§5).

Contributions that would be reusable beyond this mission include existence and uniqueness for the controlled Bass system in integral form, a comparison lemma for $D$ and $S$ under pointwise-ordered sales, and a sufficiency (verification) theorem for bang-bang controls of problems that are linear in the control.

Selected references

• B. Hu, Z. Sun, Managing self-replicating innovative goods, Management Science (doi:10.1287/mnsc.2020.3936); authors' manuscript of 2020-10-18. https://doi.org/10.1287/mnsc.2020.3936
• F. M. Bass, A new product growth for model consumer durables, Management Science 15(5), 215–227, 1969. https://doi.org/10.1287/mnsc.15.5.215
• T.-H. Ho, S. Savin, C. Terwiesch, Managing demand and sales dynamics in new product diffusion under supply constraint, Management Science 48(2), 187–206, 2002. https://doi.org/10.1287/mnsc.48.2.187.255
• S. Kumar, J. M. Swaminathan, Diffusion of innovations under supply constraints, Operations Research 51(6), 866–879, 2003. https://doi.org/10.1287/opre.51.6.866.24918
• S. P. Sethi, Optimal Control Theory: Applications to Management Science and Economics, 3rd ed., Springer, 2019. https://doi.org/10.1007/978-3-319-98237-3