Probability

Motivation

In 1965 Erdős asked how large a family of $k$-element subsets of an $n$-element set can be if it contains no $s+1$ pairwise disjoint members. The question, now called the Erdős Matching Conjecture (EMC), contains the Erdős–Ko–Rado theorem (the case $s=1$) and is one of the central open problems of extremal set theory. Beyond combinatorics it is tied to tail bounds for sums of random variables (generalizations of Markov's inequality, see Alon, Frankl, Huang, Rödl, Ruciński and Sudakov, JCTA 2012, as cited on p. 2 of the paper) and to Dirac-type thresholds for perfect matchings in hypergraphs.

Timeline.

• 1965: Erdős proves the conjecture for $n\ge n_0(k,s)$.
• 1959/1968: Erdős–Gallai settle $k=2$; Kleitman settles the case $n=k(s+1)$ implicitly.
• 1976: Bollobás, Daykin and Erdős prove it for $n\ge2k^3s$.
• 2012: Huang, Loh and Sudakov prove it for $n\ge3k^2s$.
• 2013: Frankl proves it for $n\ge(2s+1)k-s$ (JCTA 120).
• 2017: Frankl settles $k=3$ completely.
• 2018–2022: Frankl and Kupavskii prove it for $n\ge\frac53sk-\frac23s$ and all $s\ge s_0$ (arXiv:1806.08855), the result of this mission.

Setting

Write $[n]=\{1,\dots,n\}$ and $\binom{[n]}{k}$ for the set of its $k$-element subsets. For a family $\mathcal F\subseteq\binom{[n]}k$, a matching is a subfamily of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The Erdős matching function is

$$m(n,k,s)=\max\Big\{|\mathcal F| : \mathcal F\subseteq\tbinom{[n]}{k},\ \nu(\mathcal F)\le s\Big\}.$$

Two families show the conjectured value. The family of all $k$-sets meeting $[s]$ has $\binom nk-\binom{n-s}k$ members; the family of all $k$-subsets of $[k(s+1)-1]$ has $\binom{k(s+1)-1}k$ members. Both have $\nu\le s$, and the EMC asserts $m(n,k,s)$ is the larger of the two numbers. For $n\ge(k+1)s$ the first is larger.

The proof uses the shifting order: for $A=\{a_1<\dots<a_k\}$ and $B=\{b_1<\dots<b_k\}$, $A\prec B$ if $a_i\le b_i$ for all $i$ and $A\ne B$. A family is initial if it is closed downward under $\prec$. For $S\subseteq[s+1]$, $\mathcal F(S)=\{F\setminus S: F\in\mathcal F,\ F\cap[s+1]=S\}$, and $\partial$ denotes the shadow. Families $\mathcal F_1,\dots,\mathcal F_{s+1}$ are cross-dependent if no choice $F_i\in\mathcal F_i$ is pairwise disjoint, and nested if $\mathcal F_1\supseteq\dots\supseteq\mathcal F_{s+1}$. A random $t$-matching is a uniformly random ordered $t$-tuple of pairwise disjoint $l$-subsets of $[m]$, and $\eta=|\mathcal G\cap\mathcal B|$ counts how many of its sets lie in a fixed family $\mathcal G$ of density $\alpha=|\mathcal G|/\binom ml$.

Formalization targets

Goal: Theorem 1

There is an absolute constant $s_0$ such that for all $k\ge1$, $s\ge s_0$ and

$$n\ge\tfrac53sk-\tfrac23s\qquad\text{we have}\qquad m(n,k,s)=\binom nk-\binom{n-s}k .$$

The constant $s_0$ is existential and uniform in $n$ and $k$; no value is fixed, so any improvement of the proof keeps the statement valid.

Stronger form: Theorem 14

For every $\varepsilon>0$ there is $s_0(\varepsilon)$ such that the same equality holds for all $s\ge s_0$, $k\ge1$ and $n\ge s+(1.666+\varepsilon)s(k-1)$. Theorem 1 follows by taking $\varepsilon<\frac53-1.666$.

Milestones

Following the paper's proof: Lemma 3 (shifting), Proposition 4, Lemma 5, Proposition 6, Corollary 7 and Lemma 8 (structure of initial families and their shadows); Proposition 11, Theorem 12 and Proposition 13 (concentration of $\eta$ for random matchings); Lemma 18 and Lemma 15 (the weighted bound for cross-dependent nested families); Lemmas 16 and 17 (the induction step at $n=s+(1.666+\varepsilon)s(k-1)$); Theorem 14.

Significance

The theorem extends the range in which the EMC is known from $n\ge(2s+1)k-s$ to $n\ge\frac53sk-\frac23s$ for large $s$, settling roughly a third of the remaining range. The paper uses it as a black box to derive a universal upper bound on $m(n,k,s)$ below that range (its Theorem 2) and consequences for Dirac thresholds. The concentration inequality of Theorem 12, a Gaussian tail for the number of members of a fixed family hit by a random matching, is a tool of independent use and has since been applied to rainbow versions of the problem (Kupavskii, arXiv:2104.08083).

The result is proved on paper; this mission formalizes it. No part of the argument has a machine-checked proof: Mathlib has shadows and the Erdős–Ko–Rado theorem, and the platform has Erdős–Ko–Rado for $s=1$, but there is no formal theory of the matching number, shifted families, Kneser graph spectra, or martingale concentration for random matchings. A complete formalization would make the EMC in this range, and the concentration theorem, available for reuse.

Difficulty

Averaging over a random full partition of $[n]$ into $k$-sets gives only $m(n,k,s)\le s\binom{n-1}{k-1}$, far from the truth: the expected number of partition classes in $\mathcal F$ says nothing about how that number is distributed. The paper's step is to show the count is concentrated (Theorem 12) and to exploit the deterministic bound of Lemma 18, which penalizes matchings with many classes in $\mathcal F_{s+1}$. Controlling the regime where the density $\alpha$ is small needs the separate comparison of Proposition 13.

The second difficulty is Lemma 17, whose proof in the appendix is a delicate estimate on sums and products of binomial coefficients over all $k\ge4$, supported by numerical computations done in Mathematica. A formal proof needs certified numerics for these finite checks and a separate stability argument for $k>2\cdot10^4$. The case $k=3$ is an external base case (Frankl 2017), so the induction on $k$ also needs that result or another route.

Formalization scope

Sets are finite sets of natural numbers; $[n]$ is Finset.Icc 1 n, so the paper's indices such as $[i(s+1)-1]$ and $s+1,2(s+1),\dots$ appear unshifted. $\nu$ is a maximum over subfamilies (members are distinct), and $m(n,k,s)$ is a finite maximum, always attained. Initial families are closed downward among $k$-subsets of $[m]$ only. Random matchings are ordered tuples, and probabilities, expectations and covariances are uniform averages over the finite sample space. The constant $1.666$ is the exact decimal, not $5/3$. The paper omits integer parts at $n=s+(c+\varepsilon)s(k-1)$; the formalization rounds $n$ up. Where the paper leaves hypotheses implicit, they are binders: $k\ge2$ in Corollary 7, Lemma 8 and Lemma 16, $k\ge4$ and the induction hypothesis in Lemma 17, $t\ge1$ in Theorem 12, and $q>0$ (the division $sx/q$) in Lemma 15.

The goal is the equality $m(n,k,s)=\binom nk-\binom{n-s}k$; exhibiting the family of $k$-sets meeting $[s]$ proves only the lower bound and does not close it.

Useful infrastructure, reusable beyond this mission: shifting and the compression argument (Lemma 3), the shadow bounds of Section 2, the expander mixing lemma and the second eigenvalue of Kneser graphs, and the Azuma–Hoeffding inequality for the exposure martingale of a random matching. Contributions of any of these, and of alternative proofs of the milestones, are welcome.

Selected references

• P. Frankl, A. Kupavskii, The Erdős Matching Conjecture and concentration inequalities, J. Combin. Theory Ser. B (2022); arXiv:1806.08855v3. https://arxiv.org/abs/1806.08855, https://doi.org/10.1016/j.jctb.2022.08.002
• P. Erdős, A problem on independent r-tuples, Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 8 (1965), 93–95.
• P. Frankl, Improved bounds for Erdős' Matching Conjecture, J. Combin. Theory Ser. A 120 (2013), 1068–1072. https://doi.org/10.1016/j.jcta.2013.01.008
• P. Frankl, On the maximum number of edges in a hypergraph with given matching number, Discrete Appl. Math. 216 (2017), 562–581.
• H. Huang, P.-S. Loh, B. Sudakov, The size of a hypergraph and its matching number, Combin. Probab. Comput. 21 (2012), 442–450.
• N. Alon, F. Chung, Explicit construction of linear sized tolerant networks, Discrete Math. 72 (1988), 15–19. https://doi.org/10.1016/0012-365X(88)90189-6
• L. Lovász, On the Shannon capacity of a graph, IEEE Trans. Inform. Theory 25 (1979), 1–7. https://doi.org/10.1109/TIT.1979.1055985

Motivation

A convex risk measure assigns to a bounded financial position $X$ (a random net payoff) a number $\rho(X)$, interpreted as the capital that must be added to $X$ to make it acceptable. The axiomatic theory began with coherent risk measures (Artzner, Delbaen, Eber and Heath, 1999) and was extended to convex ones by Föllmer and Schied (2002) and Frittelli and Rosazza Gianin (2002). Its central structural result is a robust representation: a convex risk measure that is continuous from above equals a worst case of expected losses over a family of probabilistic models, each penalized by how implausible it is.

Regulators and risk managers do not assess positions once and for all; they reassess them as information arrives. Detlefsen and Scandolo (2005) extend the representation to conditional risk measures, whose value $\rho(X)$ is itself a random variable measurable with respect to the information available to the agent. This is the building block of dynamic (time-consistent) risk measurement, studied in later work on dynamic risk measures and backward stochastic differential equations.

Timeline. Artzner et al. (1999): coherent risk measures on finite $\Omega$. Delbaen (2002): coherent risk measures on general probability spaces, Fatou property. Föllmer–Schied (2002) and Frittelli–Rosazza Gianin (2002): convex risk measures and their robust representation; Föllmer–Schied, Stochastic Finance, Theorem 4.26 (2002 edition) for $L^\infty$ with continuity from above. Detlefsen–Scandolo (2005): the conditional version, Theorem 3.2 of the paper formalized here.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$ describing the available information. $L^\infty$ is the space of essentially bounded random variables and $L^\infty_{\mathcal G}$ its $\mathcal G$-measurable part; every (in)equality between random variables holds $P$-almost surely.

A map $\rho:L^\infty\to L^\infty_{\mathcal G}$ is a conditional convex risk measure if $\rho(0)=0$ and, for $X,Y\in L^\infty$:

• (conditional translation invariance) $\rho(X+Z)=\rho(X)-Z$ for every $Z\in L^\infty_{\mathcal G}$;
• (monotonicity) $X\le Y$ implies $\rho(X)\ge\rho(Y)$;
• (conditional convexity) $\rho(\Lambda X+(1-\Lambda)Y)\le\Lambda\rho(X)+(1-\Lambda)\rho(Y)$ for every $\Lambda\in L^\infty_{\mathcal G}$ with $0\le\Lambda\le1$.

The admissible models are

$$\mathcal P_{\mathcal G}=\{Q \text{ probability on }(\Omega,\mathcal F): Q\ll P,\ Q(A)=P(A)\text{ for all }A\in\mathcal G\}.$$

For a family $\mathcal X$ of $[-\infty,+\infty]$-valued random variables, the essential supremum $\operatorname{ess.sup}\mathcal X$ is the $P$-a.s. smallest random variable that dominates every member $P$-a.s.; it replaces the pointwise supremum, which is not meaningful for uncountable families of equivalence classes.

A map $\rho$ is representable if there is a penalty $\alpha:\mathcal P_{\mathcal G}\to L^0_{\mathcal G}([0,+\infty])$ with

$$\rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha(Q)\},\qquad X\in L^\infty .$$

The minimal penalty is $\alpha^*(Q)=\operatorname{ess.sup}_{X\in L^\infty}\{-E_Q(X\mid\mathcal G)-\rho(X)\}$. $\rho$ is continuous from above if $X_n\searrow X$ $P$-a.s. implies $\rho(X_n)\nearrow\rho(X)$ $P$-a.s.

Formalization targets

Goal: Theorem 3.2

For a conditional convex risk measure $\rho$, the following are equivalent:

$$\text{(a) } \rho \text{ continuous from above}\iff\text{(b) } \rho\text{ representable}\iff\text{(c) } \rho(X)=\operatorname*{ess.sup}_{Q\in\mathcal P_{\mathcal G}}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}.$$

Milestones

• Theorem A.1: existence and a.s. uniqueness of the essential supremum; an increasing sequence converging to it for upward directed families.
• Lemma A.2: $E_P(\operatorname{ess.sup}\mathcal X)=\sup_{X\in\mathcal X}E_PX$ for upward directed $\mathcal X$.
• The easy inequality $\rho(X)\ge\operatorname{ess.sup}_{Q}\{-E_Q(X\mid\mathcal G)-\alpha^*(Q)\}$.
• The unconditional representation (Föllmer–Schied, Theorem 4.26) of a convex risk measure $\rho_0:L^\infty\to\mathbb R$ continuous from above: $\rho_0(X)=\sup_{Q\ll P}\{-E_QX-\alpha^*_0(Q)\}$.
• For $\rho_0=E_P[\rho(\cdot)]$: $\alpha^*_0(Q)<\infty$ forces $Q\in\mathcal P_{\mathcal G}$.
• The family $B_Q=\{-E_Q(X\mid\mathcal G)-\rho(X):X\in L^\infty\}$ is upward directed.
• $E_P[\alpha^*(Q)]=\alpha^*_0(Q)$ for $Q\in\mathcal P_{\mathcal G}$.
• Representable implies continuous from above.
• Remark 3.3: $\alpha^*\le\alpha$ for every penalty $\alpha$, and $\alpha^*(Q)=\operatorname{ess.sup}_{X\in\mathcal A_\rho}\{-E_Q(X\mid\mathcal G)\}$.

Significance

The result. Theorem 3.2 shows that a conditional convex risk measure is determined by a random penalty on the models consistent with the available information, exactly when it satisfies a sequential continuity condition. The representation is the input for the paper's later sections: the conditional entropic risk measure, whose minimal penalty is the conditional relative entropy, and the consistency of dynamic risk measures via Lemma 3.4, which is expressed through the minimal penalty. The restriction to $\mathcal P_{\mathcal G}$ has an interpretation: the more information, the fewer models can enter the worst case.

Formalizing it. The theorem has been proved in the literature since 2005; to our knowledge neither it nor its unconditional counterpart has a machine-checked proof. The mission produces an essential supremum of arbitrary families of extended random variables with its existence theorem, the exchange of expectation and essential supremum for directed families, and the unconditional Föllmer–Schied representation on $L^\infty$. The last of these is the standard representation theorem of the theory of convex risk measures and is useful well beyond this paper.

Difficulty

The obvious route, applying the unconditional representation pathwise or $\omega$ by $\omega$, fails: $\rho(X)(\omega)$ is not a risk measure of anything, and conditional expectations are only defined up to null sets that depend on $Q$, of which there are uncountably many. The essential supremum is what turns an uncountable supremum of classes into a well-defined class, and passing expectations through it requires directedness. The unconditional step itself (continuity from above implies the dual representation) rests on a Krein–Šmulian / weak* closedness argument on $L^\infty$, which is not available off the shelf.

Formalization scope

• Payoffs are real functions $\Omega\to\mathbb R$ with MemLp X ⊤ P; $\rho$ is a map $(\Omega\to\mathbb R)\to(\Omega\to\mathbb R)$ constrained only on $L^\infty$. Because it acts on functions, $\rho$ is required to respect $P$-a.s. equality, and $\rho(X)$ is required to be $\mathcal G$-strongly measurable and essentially bounded; the paper's $\rho$ acts on classes, so this adds nothing in substance. $\mathcal G$ is a MeasurableSpace m with m ≤ mΩ.
• Translation invariance and convexity quantify over $\mathcal G$-measurable $Z$ and $\Lambda$ (not constants). $\mathcal P_{\mathcal G}$ is the subtype of probability measures $Q\ll P$ with $Q(A)=P(A)$ for all $A\in\mathcal G$ — equality on $\mathcal G$, not mutual absolute continuity.
• $E_Q(X\mid\mathcal G)$ is Mathlib's Q[X | m]; it is $\mathcal G$-measurable, hence determined $P$-a.s. for $Q\in\mathcal P_{\mathcal G}$.
• Extended values live in EReal; penalties are ENNReal-valued and coerced, so only (real) $-(+\infty)=-\infty$ occurs, never $+\infty-(+\infty)$.
• The essential supremum is a predicate IsEssSup P F Z (a.e. upper bound of every member, a.e. below every a.e.-measurable a.e. upper bound). The minimal penalty is a predicate IsMinimalPenalty on a candidate; statement (c) of the goal asserts that a $\mathcal G$-measurable $[0,+\infty]$-valued essential supremum of $B_Q$ is a penalty for $\rho$.
• Continuity from above: $X_n,X\in L^\infty$, $(X_n)$ a.s. non-increasing and a.s. convergent to $X$ implies $(\rho(X_n))$ a.s. non-decreasing and a.s. convergent to $\rho(X)$. It is not norm or weak* continuity.
• Lemma A.2's "provided the expectations exist" is pinned as: each member has an expectation in $[-\infty,+\infty]$ and some member has integrable negative part (without the latter the lemma is false). Theorem A.1's directed part assumes a nonempty family. The acceptance set of Remark 3.3 is $\{X\in L^\infty:\rho(X)\le0\}$ (the paper's $L^\infty_{\mathcal G}$ on p. 4 is a misprint).
• Ruled out: an essential supremum defined as a pointwise ⨆ over the family, or via Mathlib's essSup of a single function, and an index set equal to all $Q\ll P$ or to the $Q$ equivalent to $P$; each of these changes statement (b) or makes it vacuous.
• Needed infrastructure: essential suprema of families, extended expectations with monotone convergence, conditional expectation under a change of measure agreeing on $\mathcal G$, and the $L^\infty$–$L^1$ duality behind Föllmer–Schied 4.26. The essential-supremum layer and the unconditional representation are reusable in any mission on risk measures or robust optimization; contributions to either are welcome.

Selected references

• K. Detlefsen, G. Scandolo, Conditional and Dynamic Convex Risk Measures, SFB 649 Discussion Paper 2005-006, Humboldt-Universität zu Berlin, 2005 (the version formalized here; journal version: Finance and Stochastics 9(4), 539–561, 2005, https://doi.org/10.1007/s00780-005-0159-6)
• H. Föllmer, A. Schied, Stochastic Finance — An Introduction in Discrete Time, de Gruyter Studies in Mathematics 27, 2002. https://doi.org/10.1515/9783110198065
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4), 429–447, 2002. https://doi.org/10.1007/s007800200072
• M. Frittelli, E. Rosazza Gianin, Putting order in risk measures, Journal of Banking and Finance 26, 1473–1486, 2002. https://doi.org/10.1016/S0378-4266(02)00270-4
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3), 203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002. https://doi.org/10.1007/978-3-662-04790-3_1

Motivation

A spectrally negative Lévy process is a process with stationary independent increments whose jumps are all downward: Brownian motion with drift plus a compound Poisson or infinite-activity stream of negative jumps. It is the standard model for a risk reserve that earns premiums continuously and pays claims in lumps, for a storage level or a queue workload seen in reverse, and, in mathematical finance, for a log-price that can crash but not jump up. Exit problems (when and where such a process first leaves an interval) are the basic quantities in ruin theory, in dividend and barrier problems, and in the pricing of path-dependent options.

The reflected process $Y=\overline X-X$, the distance of $X$ below its running maximum, is the drawdown of $X$. Its first passage above a level $k$ is the time at which a drawdown of size $k$ first occurs. Avram, Kyprianou and Pistorius (AKP 2004) computed the joint Laplace transform of this passage time and of the overshoot $Y_{\tau_k}$ in closed form, in terms of the scale functions of $X$. This is the first of three missions on that paper. The two others use this identity for the perpetual Russian option and its Canadized version.

Timeline. Bertoin gave the upward two-sided exit identity for spectrally negative Lévy processes in terms of scale functions (Bertoin 1996, Theorem VII.8) and the downward one (Bertoin 1997, Corollary 1). Avram, Kyprianou and Pistorius (2004) obtained the joint transform of $(\tau_k,Y_{\tau_k})$ for every spectrally negative Lévy process of unbounded variation, or of bounded variation with absolutely continuous Lévy measure.

Setting

Let $X=\{X_t,t\ge0\}$ be a spectrally negative Lévy process on $(\Omega,\mathcal F,\mathbb P)$: it starts at $0$, has independent and stationary increments, càdlàg paths, no positive jumps, and paths that are not monotone. Its Laplace exponent is $\psi(\theta)=\log\mathbb E[e^{\theta X_1}]$, and "$\psi(v)<\infty$" means that $e^{vX_1}$ is integrable. For such $v$, the tilted exponent is $\psi_v(\theta)=\psi(\theta+v)-\psi(v)$.

The paper assumes throughout that $X$ has unbounded variation, or has bounded variation and a Lévy measure $\Lambda$ with $\Lambda(dx)\ll dx$.

For $q\ge0$, $\Phi(q)$ is the largest root of $\psi(\theta)=q$. The $q$-scale function $W^{(q)}:\mathbb R\to[0,\infty)$ is the unique function that vanishes on $(-\infty,0]$, is continuous on $(0,\infty)$, and satisfies

$$\int_0^\infty e^{-\theta x}W^{(q)}(x)\,dx=\frac1{\psi(\theta)-q},\qquad\theta>\Phi(q).$$

For $q<0$ it is defined by the series $W^{(q)}=\sum_{k\ge0}q^kW^{\star(k+1)}$, where $W=W^{(0)}$ and $\star$ is convolution on $[0,\infty)$. Further, $Z^{(q)}(x)=1+q\int_{-\infty}^xW^{(q)}(z)\,dz$. The functions $W_v^{(p)}$ and $Z_v^{(p)}$ are the same objects built from $\psi_v$ instead of $\psi$.

Under $\mathbb P_{s,x}$ the process starts at $x$ with a prior maximum $s\ge x$. Its running maximum is $\overline X_t=\max\{s,\sup_{0\le u\le t}X_u\}$, and the reflected process is $Y=\overline X-X$, which starts at $z=s-x$. For $k>0$,

$$\tau_k=\inf\{t\ge0:Y_t\notin[0,k)\}.$$

Formalization targets

Goal: Theorem 1

For $u\ge0$ and $v$ with $\psi(v)<\infty$, with $z=s-x\ge0$ and $p=u-\psi(v)$,

$$\mathbb E_{s,x}\big[e^{-u\tau_k-vY_{\tau_k}}\big]=e^{-vz}\left(Z_v^{(p)}(k-z)-W_v^{(p)}(k-z)\frac{pW_v^{(p)}(k)+vZ_v^{(p)}(k)}{W_v^{(p)\prime}(k)+vW_v^{(p)}(k)}\right).$$

Here $v$ may be negative, so $p$ may be negative, which is where the series extension of $W$ enters.

Milestones

• (2) $\mathbb E[e^{\theta X_t}]=e^{t\psi(\theta)}$.
• Remark 4: $W^{(u)}(x)=e^{vx}W_v^{(u-\psi(v))}(x)$ for every real $u$.
• Proposition 1, (9) and (10): for $x\in(a,b)$, the Laplace transforms of the exit time of $X$ from $(a,b)$ on the events of exit above and exit below.
• (13): the splitting of the goal's expectation at the first zero of $Y$.
• (14)–(15) and (16): the two expectations of (13).
• (22): the value $C$ of the functional for $Y$ started at $0$.
• Remark 6, (23): the stopped process whose martingale property is equivalent to Theorem 1.

Items (13)–(22) are stated under the proof's restriction $u\ge\psi(v)\vee0$. The goal is not.

Significance

The identity gives, for every spectrally negative Lévy process, the law of the first drawdown of size $k$ and of its overshoot. With $v=0$ it is the Laplace transform of the drawdown time. With $u=0$ it is the transform of the overshoot. The paper uses it, through its Corollary 1, to solve the perpetual Russian option and the Canadized Russian option in closed form. Identities of this form, written in scale functions, are the standard tool for drawdown and reflected-process problems for spectrally negative Lévy processes.

The theorem is proved. As far as the platform and Mathlib show, none of it is formalized: Mathlib has independent increments and cumulant generating functions but no Lévy process, no scale function and no excursion theory. This mission produces a formal statement of the paper's model and of the exit identities. A complete development would also give Mathlib its first fluctuation-theory results for Lévy processes.

Difficulty

The natural first idea is to treat $Y$ like $X$ and read off its exit from $[0,k)$ from the two-sided exit identities of Proposition 1. This works only until $Y$ first returns to $0$. Up to that time $Y$ is a copy of $-X$. After it, $Y$ is reflected at $0$, it is not a Lévy process, and no two-sided exit problem of $X$ describes it. The whole content of the theorem is the constant $C$ of (13), the value of the functional for $Y$ started at $0$, where the reflection acts at every instant. A second difficulty is the range of $(u,v)$. For $v<0$ the integrand $e^{-vY_{\tau_k}}$ is unbounded, because $Y$ can jump far above $k$. Its finiteness is part of the claim. So is the passage from the region $u\ge\psi(v)\vee0$, where every scale function in (12) comes from Definition 2, to all $u\ge0$, where $p$ can be negative.

Formalization scope

Time is $[0,\infty)$ (ℝ≥0). $X$ is a real process with $X_0=0$. $\mathbb P_x$ is encoded by the path $x+X$, and $\mathbb P_{s,x}$ by that path together with the prior maximum $s$. Random times take values in WithTop ℝ≥0, with $\infty$ as "never". The functional $e^{-u\tau_k-vY_{\tau_k}}$ and discount factors $e^{-qT}$ are set to $0$ where the time is infinite. Every stated expectation carries its integrability as part of the conclusion.

Readings of the paper's informal words:

• "Lévy process": the paths start at $0$, are càdlàg and have no positive jumps for every $\omega$, not only almost surely.
• "We exclude the case that X has monotone paths": the paths are neither almost surely nondecreasing nor almost surely nonincreasing.
• "unbounded variation": not of bounded variation. The standing assumption is "bounded variation implies (AC)".
• "$\Lambda(dx)\ll dx$": for every Lebesgue-null Borel $A$, almost surely no nonzero jump in $(0,1]$ lands in $A$. The Lévy measure is not constructed.
• "$\psi(v)<\infty$": $e^{vX_1}$ is integrable.
• "the largest root": the supremum of the nonnegative roots.
• "the unique function": a definite description by choice.
• "analytic extension": the series (5) for real negative index. Complex indices are out of scope.
• "$W'$": the derivative at $k>0$.
• "is a martingale" in (23): a martingale for the natural filtration of $X$.
• Misprint: (23) prints $vZ_v^{(q)}(k)$, and the statement uses $vZ_v^{(p)}(k)$.

The scale functions are defined from the exponent $\psi$ of the given $X$. A formalization in which $W$ is an arbitrary function satisfying a Laplace-transform hypothesis is ruled out. So is one in which $W_v^{(p)}$ is defined as $e^{-vx}W^{(p+\psi(v))}(x)$, which would make Remark 4 a tautology.

Infrastructure a complete development needs: Lévy processes and their Laplace exponent, the strong Markov property at stopping times, existence and regularity of scale functions (via Laplace inversion), and the Esscher change of measure. No statement of the mission mentions excursion theory. Contributions of reusable infrastructure for Lévy processes are welcome.

Selected references

• F. Avram, A. E. Kyprianou, M. R. Pistorius, Exit problems for spectrally negative Lévy processes and applications to (Canadized) Russian options, Ann. Appl. Probab. 14(1), 215–238, 2004. https://doi.org/10.1214/aoap/1075828052
• J. Bertoin, Lévy Processes, Cambridge University Press, 1996. https://www.cambridge.org/core/books/levy-processes/
• J. Bertoin, Exponential decay and ergodicity of completely asymmetric Lévy processes in a finite interval, Ann. Appl. Probab. 7(1), 156–169, 1997. https://doi.org/10.1214/aoap/1034625254

Motivation

In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value $v$ of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than $v$ and player 2 more than $-v$ at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.

The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$. Player $i$ has a utility $u_i:X\to\mathbb R$; write $h_i(a)=u_i(g(a))$ for $a\in S$.

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$-field $\mathcal B$ of events, a sub-$\sigma$-field $\mathcal J_i\subseteq\mathcal B$ for each player (the events regarding which $i$ is informed), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets lie in $\mathcal J_i$. For a profile $s$ of strategies, player $i$'s payoff is computed under his own beliefs:

$$H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega).$$

An event $A$ is objective if all $p_i(A)$ coincide, and subjective otherwise. It is $i$-secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$-field generated by the $\mathcal J_k$, $k\ne i$. It is public if it lies in every $\mathcal J_i$. A measure is non-atomic on a $\sigma$-field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub-$\sigma$-field of $\mathcal B$ on which every $p_j$ is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player $i$ has a $\sigma$-field $\mathcal R_i$ of $i$-secret events on which every $p_j$ is non-atomic.

The game is two-person zero-sum if $n=2$ and $u_1(x)+u_2(x)=0$ for all $x\in X$. Its value $v$ is player 1's payoff $F_1(\sigma)=\sum_{a\in S}h_1(a)\sigma_1(a_1)\sigma_2(a_2)$ at a Nash equilibrium $\sigma$ of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair $(v,-v)$.

Formalization targets

Goal: Proposition 6.1 (p. 80)

Let $G$ be a two-person zero-sum game with value $v$, and assume

$$\exists\,x,y\in X:\ u_1(x)>v>u_1(y),\tag{6.2}$$ $$\text{for each } i\in\{1,2\} \text{ there is } B_i\in\mathcal J_i \text{ with } p_1(B_i)\ne p_2(B_i).\tag{6.3}$$

Then there is a pair $s=(s_1,s_2)$ of strategies with

$$H_1(s)>v,\qquad H_2(s)>-v.\tag{6.4}$$

The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.

Milestones

1. Lemma 7.1 (p. 81): in a roulette $\mathcal R$ there is, for every $\alpha\in[0,1]$ and events $B^1,\dots,B^l$, an objective event $A\in\mathcal R$ with $p(A)=\alpha$, independent of each $B^k$.
2. Lemma 4.2 (p. 77): for every $i$, event $B$ and $\alpha\in[0,1]$ there is an objective $i$-secret event of probability $\alpha$ independent of $B$.
3. Lemma 4.4 (p. 77): if there is a public roulette, the same holds with "public" in place of "$i$-secret".
4. Remark after Proposition 6.1 (p. 80): the conclusion (6.4) under (6.2) and

$$\text{there is a public subjective event } B \text{ and there is a public roulette,}\tag{6.5}$$

a special case of the goal in which the players share both the subjective event and the correlating device.

Significance

The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows $(1,1)$ and $(2,0)$) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.

Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.

The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.

Difficulty

The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.

For Lemma 7.1, a non-atomic scalar measure takes every value in $[0,p(\Omega)]$, but the lemma asks for one event with prescribed values under $n$ measures and $nl$ further measures simultaneously; this is the range of a vector measure, not of a scalar one.

Formalization scope

• Players of the zero-sum game are 0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.
• $\mathcal B$ is the σ-field mΩ, an explicit parameter of RandomizingStructure; $\mathcal J_i$ are σ-fields below it, and each $p_i$ is a probability measure on $\mathcal B$. Probabilities are ℝ≥0∞-valued; "probability $\alpha$" is ENNReal.ofReal α with $0\le\alpha\le1$.
• Non-atomicity is the standard notion on a sub-σ-field, not Mathlib's NoAtoms, which would trivialize the roulette hypotheses.
• $H_i$ is a Bochner integral under $p_i$; for strategies with finitely many values it is the finite sum $\sum_a p_i\{s=a\}h_i(a)$.
• The value $v$ is not a free real: IsValue u g v requires $v=F_1(\sigma)$ for a Nash equilibrium $\sigma$ of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free $v$ would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.
• Assumption II is a hypothesis of every theorem, including those whose proofs do not need it.
• The conclusion of the goal and of the Remark asks for strategies, not for an equilibrium point, and does not require the strategies to be independent or objective.

Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of $H_i$ for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.

Selected references

• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. Lyapunov, Sur les fonctions-vecteurs complètement additives, Bull. Acad. Sci. URSS Sér. Math. 4 (1940) 465–478.
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928) 295–320. https://doi.org/10.1007/BF01448847
• J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529

Motivation

In a contextual bandit problem a learner repeatedly observes a context (a user, a patient, a query), chooses one of $K$ actions, and observes the reward of the chosen action only. It competes with the best policy of a fixed class $\Pi$ of maps from contexts to actions. This is the standard model for news and advertisement recommendation, adaptive clinical assignment and other interactive decision problems in which counterfactual rewards are never observed.

Two requirements pull against each other. Statistically, the optimal regret against a finite class is of order $\sqrt{KT\ln|\Pi|}$, attained by the exponential-weights algorithm Exp4 (Auer et al. 2002), whose running time is linear in $|\Pi|$ per round. Computationally, practical policy classes are exponentially large and are accessed only through a supervised learning routine. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) give ILOVETOCONBANDITS, which reaches the optimal regret while touching $\Pi$ only through an arg-max oracle, and only $\tilde O(\sqrt{KT/\ln|\Pi|})$ times in $T$ rounds.

Timeline. Exp4 (2002) attains $O(\sqrt{KT\ln|\Pi|})$ against adversarial rewards with running time $\Omega(|\Pi|)$. Epsilon-greedy and Epoch-Greedy (Langford and Zhang 2007) are oracle-efficient but have regret of order $T^{2/3}$. Exp4.P (Beygelzimer et al. 2011) proves the optimal bound with high probability. RandomizedUCB (Dudík et al. 2011) is the first oracle-based algorithm with optimal regret in the i.i.d. model, but its number of oracle calls is a large polynomial in $T$. ILOVETOCONBANDITS (2014) keeps the regret and reduces the calls to $\tilde O(\sqrt{KT/\ln(|\Pi|/\delta)})$.

Setting

There are $K$ actions, a measurable context space $X$, and a finite nonempty policy class $\Pi$ of measurable maps $X\to\{0,\dots,K-1\}$. A distribution $\mathcal D$ on $X\times[0,1]^K$ generates context/reward-vector pairs $(x_t,r_t)$, $t=1,2,\dots$, independently. In round $t$ the learner sees $x_t$, draws an action $a_t$ with probability $p_t(a_t)$, and observes only $r_t(a_t)$. The history $H_t$ is the list of records $(x_i,a_i,r_i(a_i),p_i(a_i))$, $i\le t$.

The expected reward of a policy is $\mathcal R(\pi)=\mathbb E_{(x,r)\sim\mathcal D}[r(\pi(x))]$, $\pi_\star$ is any maximizer over $\Pi$, and $\mathrm{Reg}(\pi)=\mathcal R(\pi_\star)-\mathcal R(\pi)$. The regret after $T$ rounds is the empirical cumulative quantity $\sum_{t=1}^T\bigl(r_t(\pi_\star(x_t))-r_t(a_t)\bigr)$.

The inverse propensity scoring estimate is $\widehat{\mathcal R}_t(\pi)=\frac1t\sum_{i\le t}r_i(a_i)\mathbb 1\{\pi(x_i)=a_i\}/p_i(a_i)$, and $\widehat{\mathrm{Reg}}_t(\pi)=\max_{\pi'}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$. For nonnegative weights $Q$ on $\Pi$ with total mass at most one, the smoothed projection is $Q^\mu(a\mid x)=(1-K\mu)\sum_{\pi:\pi(x)=a}Q(\pi)+\mu$.

ILOVETOCONBANDITS takes an epoch schedule $0=\tau_0<\tau_1<\cdots$ and $\delta\in(0,1)$, sets $d_t=\ln(16t^2|\Pi|/\delta)$ and $\mu_m=\min\{1/(2K),\sqrt{d_{\tau_m}/(K\tau_m)}\}$. At the end of epoch $m$ (round $\tau_m$) it chooses weights $Q_m$ solving the optimization problem (OP): with $b_\pi=\widehat{\mathrm{Reg}}_{\tau_m}(\pi)/(100\mu_m)$,

$$\sum_\pi Q(\pi)b_\pi\le2K,\qquad \widehat{\mathbb E}_{x\sim H_{\tau_m}}\bigl[1/Q^{\mu_m}(\pi(x)\mid x)\bigr]\le2K+b_\pi\ \ \forall\pi\in\Pi.$$

During epoch $m+1$ it puts the leftover mass on the empirical maximizer $\pi_{\tau_m}$, obtaining a distribution $\widetilde Q_m$, and draws $a_t\sim\widetilde Q_m^{\mu_m}(\cdot\mid x_t)$.

Formalization targets

Goal: Theorem 2 in the explicit form of Lemma 17

Assume $\tau_{m+1}\le2\tau_m$ for $m\ge1$ and let $m_0=\min\{m\ge1:d_{\tau_m}/\tau_m\le1/(4K)\}$, $\rho=\sup_{m\ge m_0}\sqrt{\tau_m/\tau_{m-1}}$, $c_0=4\rho(1+94.1)$, $C_0=400+c_0$, and $m(T)=\min\{m:T\le\tau_m\}$. For every $T$, with probability at least $1-\delta$,

$$\sum_{t=1}^T\bigl(r_t(\pi_\star(x_t))-r_t(a_t)\bigr)\le C_0\Bigl(4Kd_{\tau_{m_0-1}}+\sqrt{8Kd_{\tau_{m(T)}}\tau_{m(T)}}\Bigr)+\sqrt{8T\ln(2/\delta)}.$$

It holds for every (OP)-solution selection and every tie-breaking rule. Since $\tau_{m(T)}\le2(T-1)$ once $\tau_{m(T)-1}\ge1$, this is the paper's $O\bigl(\sqrt{KT\ln(T|\Pi|/\delta)}+K\ln(T|\Pi|/\delta)\bigr)$.

Milestones

Freedman's inequality (Lemma 9); the uniform deviation of true from empirical variances (Lemma 10); the deviation of the IPS estimates (Lemma 11); on the event $\mathcal E$ where both deviations hold, the variance bound (Lemma 12), the two-sided comparison of $\mathrm{Reg}$ and $\widehat{\mathrm{Reg}}_t$ (Lemma 13), and the low regret of the sampling distribution (Lemma 14); and the deterministic sums of the $\mu_m$ (Lemmas 15, 16).

Significance

The theorem shows that optimal regret in the i.i.d. contextual bandit problem does not require enumerating the policy class: a sequence of convex feasibility problems, each solvable with few oracle calls (Theorem 3, the companion mission), suffices. The inverse-propensity variance constraint of (OP) and the epoch-and-warm-start structure became the template for later oracle-based methods, and the paper's Online Cover variant is implemented in the Vowpal Wabbit learning system.

The result is proved in the paper; none of it is formalized. The platform holds Exp4 (Bandit Algorithms VIII, adversarial rewards and expert advice) and SquareCB (Foundations of RL II, regression oracles), both different algorithms in different models, and Azuma–Hoeffding (bounded_diff_martingale_two_sided), which the proof of Lemma 17 uses. This mission adds the first inverse-propensity estimator, the first oracle-based policy-class bandit algorithm, and Freedman's inequality with a conditional-variance sum. Several statements are proved in the paper only in outline: Lemma 10 has a proof sketch that defers to Dudík et al. (2011), and the paper asserts $\Pr(\mathcal E)\ge1-\delta/2$ without spelling out how the first case of (14) follows from Lemma 11.

Difficulty

The regret of the algorithm depends on the quality of its own data. The estimates $\widehat{\mathcal R}_t$ have variance governed by the distributions $\widetilde Q_m$ the algorithm chose earlier, and those distributions were chosen from the estimates. A direct union bound over $\Pi$ with the worst-case variance $1/\mu$ gives regret of order $T^{2/3}$, the Epoch-Greedy rate. The argument that avoids this must show that a policy with large variance was already known to be bad, and the estimated and true regrets must be compared inductively over epochs with constants that do not grow ($\theta_2\ge8\rho$). The inequality must also hold for every solution of (OP), not a particular one.

The martingale structure requires care: the action of round $t$ is drawn from a distribution that depends on the whole past and must not look at $r_t$, and Lemma 10 must hold uniformly over all distributions $P$ on $\Pi$, not just finitely supported ones.

Formalization scope

The formalization commits to the following representation and conventions.

• Actions are Fin K with 0 < K (NeZero K); $\Pi$ is a nonempty Finset (X → Fin K) of measurable maps; weights on $\Pi$ are real functions on its subtype. $\mathcal D$ is a probability measure on X × (Fin K → ℝ) with rewards in $[0,1]$ almost surely.
• The run lives on a probability space carrying $Z_t=(x_t,r_t)$ i.i.d. with law $\mathcal D$ and $U_t$ i.i.d. uniform on $[0,1]$, independent of the $Z$'s. The action is the inverse distribution function of $\widetilde Q^{\mu}(\cdot\mid x_t)$ at $U_t$, so it has the right law and is independent of $r_t$ given the past and $x_t$. The tie-breaking rule and the (OP)-selection are arbitrary measurable functions of the observable history (a list of records). The selection must return an (OP) solution for every history of length $\tau_m$; such selections exist by Theorem 3.
• Rounds and epochs are $1,2,\dots$ as in the paper; $\ln$ is Real.log.
• $\mu_0:=1/(2K)$. The printed formula is $0/0$ at $\tau_0=0$, and the proofs of Lemmas 12 and 14 use this value.
• The goal and Lemmas 13–14 assume $m_0\ge2$, i.e. $d_{\tau_1}/\tau_1>1/(4K)$, which holds e.g. for $\tau_1=1$. It replaces the paper's "$\tau_1=O(1)$". It makes $d_{\tau_{m_0-1}}$ finite and $\rho\le\sqrt2$, so $\rho$ is a genuine real supremum.
• Explicit constants: $\psi=100$, $\theta_1=94.1$, $\theta_2=\psi/6.4$, $c_0=4\rho(1+\theta_1)$, $C_0=4\psi+c_0$, $6.4$, $75$, $6.3$, $81.3$, $e-2$. $\rho$ is not replaced by $\sqrt2$.
• Where the paper allows $\lambda=0$ or $\mu_m=0$ (Lemmas 9–11), the bound is $+\infty$. These cases are excluded ($\lambda>0$, $\mu_m>0$) because $x/0=0$ in Lean. Lemma 9 adds measurability and integrability of $X_t$ and $X_t^2$.
• Probability statements bound the (outer) measure of the failure event by $\delta$.

A statement about "a policy mixture with small regret", about the pseudo-regret $\sum_t\mathrm{Reg}$ of the chosen policies, about a specially chosen (OP) solution, or about actions that may depend on $r_t$ is not Theorem 2; none of these is accepted. With these constants the bound exceeds $T$ unless $T$ is very large, which is a property of the paper's constants, not of the encoding.

Needed infrastructure: Freedman's inequality for the natural filtration, a uniform-over-distributions concentration argument (the probabilistic method of Dudík et al.), measurability of the algorithm's run, and Azuma–Hoeffding. Freedman's inequality and the IPS estimator are reusable beyond this mission. Proofs of any milestone, and sharper or cleaner restatements proved as separate lemmas, are welcome.

Selected references

• A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li, R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014; arXiv:1402.0555v2. https://arxiv.org/abs/1402.0555
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• A. Beygelzimer, J. Langford, L. Li, L. Reyzin, R. E. Schapire, Contextual bandit algorithms with supervised learning guarantees, AISTATS 2011. https://arxiv.org/abs/1002.4058
• M. Dudík, D. Hsu, S. Kale, N. Karampatziakis, J. Langford, L. Reyzin, T. Zhang, Efficient optimal learning for contextual bandits, UAI 2011. https://arxiv.org/abs/1106.2369
• J. Langford, T. Zhang, The epoch-greedy algorithm for contextual multi-armed bandits, NIPS 2007. https://papers.nips.cc/paper/3178-the-epoch-greedy-algorithm-for-multi-armed-bandits-with-side-information
• D. A. Freedman, On tail probabilities for martingales, Ann. Probab. 3(1), 1975. https://doi.org/10.1214/aop/1176996452

Motivation

A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.

Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with $N$ products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector $y^*$; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general $N$-product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).

Setting

There are $N$ products and $N$ demand classes, both numbered $1,\dots,N$. Class $i$ can be served by product $j$ whenever $j \le i$, at a unit substitution cost $b$ when $j < i$. Each class $i$ has unit revenue $p_i$ and unit backorder cost $\pi_i$; each product $j$ has unit purchase cost $c_j$ and effective unit salvage value $s_j$ (salvage value minus holding cost, possibly negative). Put $a_{ji} = p_i$ if $j = i$, $a_{ji} = p_i - b$ if $j < i$, and $T_k = p_k + \pi_k - b$. The standing assumptions are: (1) $\pi_i + p_i \ge \pi_j + p_j$ for $i < j$; (2) $s_i \ge s_j$ for $i < j$; (3) $a_{ij} + \pi_j - s_i \ge 0$ for $i \le j$.

The sequence of events: the starting inventory $x$ is observed; stock is raised to $y \ge x$ at unit costs $c$; the demand vector $d$ is realized; stock is allocated to classes; leftovers are salvaged. For fixed $y$ and $d$ the allocation is the linear program

$$G(y,d) = \max \sum_{i}\sum_{j \le i} a_{ji} w_{ji} + \sum_i s_i v_i - \sum_i \pi_i u_i$$

subject to $u_i + \sum_{j\le i} w_{ji} = d_i$, $v_j + \sum_{i \ge j} w_{ji} = y_j$, and $w, u, v \ge 0$, where $w_{ji}$ is the amount of product $j$ given to class $i$, $u_i$ the shortage of class $i$ and $v_j$ the leftover of product $j$. The expected profit is

$$P(x,y) = -\sum_k c_k (y_k - x_k) + \mathbb E\, G(y, D),$$

and the ordering problem is $\max_{y \ge x} P(x,y)$; a maximizer is an optimal level $\bar y(x)$.

Allocation Algorithm (A) serves the classes in the order $1,2,\dots,N$, class $i$ first from product $i$ and then from the leftovers of products $i-1,\dots,1$. The subproblem shortage $S^k_j$ is the unmet demand of class $j$ when (A) runs on the classes $k,\dots,j$ with the products $k,\dots,j$ only; $\vec S^k_{a,n} = 0$ means $S^k_m = 0$ for all $a \le m \le n$. The paper's first partial derivatives of $P$ are sums of salvage values, substitution costs and the $T_k$, weighted by probabilities of such shortage events.

Formalization targets

Goal: Theorem 2

With $y^*$ a maximizer of $P(0,\cdot)$ over $y \ge 0$, every optimal level $\bar y$ for every starting inventory $x \ge 0$ satisfies

$$x_i \ge y^*_i \implies \bar y_i = x_i .$$

Milestones

• Proposition 1: Algorithm (A) is feasible and optimal for the allocation LP, and its value is $G(y,d)$.
• Proposition 2: $y \mapsto P(x,y)$ is concave and submodular on $\{y \ge 0\}$.
• Eq. (4): the explicit formula for $\partial P/\partial y_i$ in terms of shortage probabilities.
• Theorem 1: there is $y^* \ge 0$ with $\bar y(x) = y^*$ whenever $0 \le x \le y^*$.
• Lemmas 1, 2, 3, 5: identities and monotonicity properties of the shortage probabilities used to compare $\partial P/\partial y_i$ and $\partial P/\partial y_{i+1}$.

Significance

Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector $y^*$, computed once, determines the decision for every starting inventory in the region $x \le y^*$ and fixes the order of every overstocked product elsewhere. The paper builds its bounds on $y^*$, its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.

The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair $j = i+1$, and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.

Difficulty

The obvious argument for Theorem 2 is the one-dimensional one: if $x_i \ge y^*_i$ then $\partial P/\partial y_i \le 0$ at $\bar y$, so product $i$ should not be raised. It fails because $\partial P/\partial y_i$ depends on the other coordinates: at $\bar y$ some products are raised above $x$ and others kept at $x_j > y^*_j$, and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product $i$ propagates through the greedy allocation of every later class.

Formalization scope

Products and classes are indexed by Fin N (the paper's index $k$ is Lean index $k-1$); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs $w_{ji}$, $i < j$, forbidden (fixed to $0$), as in the paper's proof of Proposition 1; $G$ is the supremum of the LP objective. The demand law is a product $\nu_1 \otimes \dots \otimes \nu_N$. Submodularity is the lattice inequality $P(x, y \vee y') + P(x, y \wedge y') \le P(x,y) + P(x,y')$, which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.

Hypotheses the paper uses without stating, made explicit here:

• the substitution cost is nonnegative, $b \ge 0$ (Proposition 1 is false for $b < 0$);
• the demand classes are independent (product forms in Lemma 3 and Appendix B);
• each demand is nonnegative, has finite mean and has a density;
• $s_i < c_i < p_i + \pi_i$ for every product (Theorem 1's proof);
• every demand law charges every nonempty open interval of $[0,\infty)$, standing in for the uniqueness of the optimal level $\bar y(x)$ that the notation presupposes (Theorems 1 and 2).

The goal quantifies over every maximizer $y^*$ of $P(0,\cdot)$ and every optimal $\bar y$; it is not an existence statement, and $y^*$ is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for $x_i \ge y^*_i$.

A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of $S^k_j$ in $y$ and $d$), are welcome.

Selected references

• Y. Bassok, R. Anupindi, R. Akella, Single-Period Multiproduct Inventory Models with Substitution, Operations Research 47(4):632–642, 1999. https://doi.org/10.1287/opre.47.4.632
• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• E. Ignall, A. F. Veinott, Jr., Optimality of Myopic Inventory Policies for Several Substitute Products, Management Science 15(5):284–304, 1969. https://doi.org/10.1287/mnsc.15.5.284
• A. J. Hoffman, On Simple Linear Programming Problems, in V. Klee (ed.), Convexity, Proceedings of Symposia in Pure Mathematics, Vol. 7, AMS, 1963.