Probability

Motivation

A retailer deciding which variants of a product to carry (colors, sizes, flavors) trades the extra sales that variety brings against the inventory cost of stocking many low-volume items. van Ryzin and Mahajan (Management Science 45(11), 1999) gave the first model that couples a multinomial logit (MNL) choice model of consumer substitution with newsvendor inventory costs, and showed that the resulting assortment problem has a simple structure. Their paper is a standard starting point of the assortment-planning literature in operations management: the "popular set" structure it proves is the benchmark that later work on assortment optimization under MNL demand (with capacity constraints, dynamic substitution, or other choice models) compares against.

This mission formalizes the paper's first main result, Theorem 1, together with the facts its proof rests on.

Setting

A store offers a subset $S$ of the variants $N=\{1,\dots,n\}$ of a category. Each variant $j$ has an MNL preference $v_j>0$, and the option of buying nothing has preference $v_0>0$. A customer facing $S$ buys variant $j\in S$ with probability

$$q_j(S)=\frac{v_j}{\sum_{i\in S}v_i+v_0}.$$

Variants are labelled so that $v_1\ge v_2\ge\cdots\ge v_n$, and the most-popular sets are $A_i=\{1,\dots,i\}$.

The retailer sells at price $p$ and buys at unit cost $c$, with $0<c<p$, and stocks $x_j$ units of each variant before the season. The critical fractile is $z=\Phi^{-1}(1-c/p)$, with $\Phi$ the standard normal distribution function. Two models of aggregate demand $Y_j$ are considered, both with store volume $\lambda>0$:

• Independent population model. $Y_j$ is normal with mean $\lambda q_j$ and standard deviation $\sigma(\lambda q_j)^\beta$, where $\sigma>0$ and $0\le\beta<1$. The optimal expected profit $\max_{x\ge0}\sum_{j\in S}E[p\min\{x_j,Y_j\}-cx_j]$ equals

$$\pi_I(S,v)=(p-c)\lambda\sum_{j\in S}q_j-\frac{p\sigma\lambda^\beta e^{-z^2/2}}{\sqrt{2\pi}}\sum_{j\in S}q_j^\beta .$$

• Trend-following population model. All customers make the same choice, so $Y_j=\lambda$ with probability $q_j$ and $Y_j=0$ otherwise. The optimal expected profit is

$$\pi_T(S,v)=\sum_{j\in S}(pq_j-c)^+\lambda .$$

The assortment problem is $\max_{S\subseteq N}\pi(S,v)$ for $\pi=\pi_I$ or $\pi=\pi_T$.

For Lemma 1, fix $S$ and let $\delta\ge0$ be the preference of a variant added to it: $f(\delta)=\sum_{j\in S}v_j+\delta+v_0$, $g_I$ and $g_T$ are the numerators of the profit after the addition, and $h_I=g_I/f$, $h_T=g_T/f$.

Formalization targets

Goal: Theorem 1 (p. 1503)

For each demand model there is a most-popular set that is optimal among all $2^n$ assortments:

$$\exists\,i\in\{0,\dots,n\}\ \forall S\subseteq N:\ \pi_I(S,v)\le\pi_I(A_i,v),\qquad \exists\,i\in\{1,\dots,n\}\ \forall S\subseteq N:\ \pi_T(S,v)\le\pi_T(A_i,v).$$

The paper prints $i\in\{1,\dots,n\}$ for both models. In the independent model the empty assortment can be the unique optimum (when $\pi_I(A_1,v)<0$, for instance at small $\lambda$), so $i=0$ is allowed there; the trend-following range is the printed one.

Milestones

1. (4)–(7): under normal demand, $x^*_j=\lambda q_j+z\sigma(\lambda q_j)^\beta$ is the optimal stocking vector and the optimal profit is $\pi_I(S,v)$.
2. (8): under trend-following demand, stocking $\lambda$ exactly when $pq_j\ge c$ is optimal and the optimal profit is $\pi_T(S,v)$.
3. Mangasarian (1969): a convex function divided by a positive affine function is quasiconvex.
4. Appendix: $g_I$ and $g_T$ are convex in $\delta$ on $[0,v_1]$.
5. Lemma 1: $h_I$ and $h_T$ are quasi-convex on $[0,v_1]$.
6. §3.1: $h(v_j)=\pi(S\cup\{j\},v)$ for $j\notin S$, and $h(0)=\pi(S,v)$.

Significance

The search over assortments is a priori a search over $2^n$ subsets. Theorem 1 cuts it to the $n+1$ nested sets $A_0\subset A_1\subset\cdots\subset A_n$, so the optimal assortment is found by comparing $n+1$ numbers. The result is not obvious: the paper's example ($n=8$, $v_1=v_2=10$, $v_8=1$) shows that $\{1,8\}$ can beat $\{1,2\}$, so the best assortment of a given size need not be the most popular one, and yet the overall optimum is always a most-popular set. The structure is used in the paper's own comparative statics (how optimal variety moves with price, store volume and the no-purchase preference) and its comparison of fashion categories under majorization, which are the other two missions of this series.

The theorem is proved in the paper; nothing here is open. To our knowledge no part of it, nor the closed-form normal newsvendor optimum (7), has a machine-checked proof. Formalizing it fixes the edge cases the printed statement glosses over (the empty assortment, the $\beta=0$ boundary) and produces reusable pieces: the normal newsvendor profit formula and Mangasarian's ratio criterion for quasiconvexity.

Difficulty

The obvious argument, "add variants in order of popularity", fails because adding a variant both brings new sales and cannibalizes the shares of the others, and the inventory term $\sum q_j^\beta$ is concave in the shares, so profit is not monotone or submodular in $S$ in any simple sense. The proof instead compares a set with the sets obtained by removing its least popular member or exchanging it for a more popular outside variant, and needs the profit after adding a variant of preference $\delta$ to be quasi-convex in $\delta$. That quasi-convexity is not visible from (7) directly; it requires rewriting the profit as a ratio $g/f$ with $f$ affine and proving $g_I$ convex, which in turn needs concavity of $(\sum_{j\in S}v_j^\beta+\delta^\beta)(\sum_{j\in S}v_j+\delta+v_0)^{1-\beta}$. The exchange argument must also handle ties among the $v_j$, which the printed proof passes over. Milestone 1 needs the derivative of the normal newsvendor objective and the identity $E(Z-z)^+=\varphi(z)-z(1-\Phi(z))$, neither of which is in Mathlib in this form.

Formalization scope

• Variants are Fin n, 0-based: the paper's variant $j$ is index $j-1$, $A_i$ is the set of indices below $i$, and the paper's $v_1$ is the first entry v ⟨0, _⟩. The no-purchase preference $v_0$ is a separate real v0, never a variant. Preferences are strictly positive and the sorting $v_1\ge\cdots\ge v_n$ is the hypothesis Antitone v.
• Standing hypotheses: $0<c<p$, $\lambda>0$, $\sigma>0$, $0\le\beta<1$; the goal also assumes $n\ge1$ (the trend-following range $1\le i\le n$ needs it).
• $z$ is defined from $p$ and $c$ as the least $x$ with $\Phi(x)\ge1-c/p$, $\Phi$ the c.d.f. of Mathlib's gaussianReal 0 1; a separate theorem states $\Phi(z)=1-c/p$ and uniqueness.
• Powers are Real.rpow, so $0^0=1$. At $\beta=0$ this keeps (7) correct ($\sum_{j\in S}q_j^0=|S|$), but $h_I(0)=\pi_I(S,v)$ then fails; that one clause carries $\beta>0$. The goal keeps $0\le\beta<1$.
• The positive part $(\cdot)^+$ is max · 0. In (11), $\lambda$ multiplies both terms; the printed (11) has it on the sum only, which would break $h_T(v_j)=\pi_T(S\cup\{j\},v)$ unless $\lambda=1$.
• "Optimal" means $\pi(S,v)\le\pi(A_i,v)$ for every $S\subseteq N$, including $S=\emptyset$. A formalization that maximizes only over prefix sets, assumes the optimum nonempty or the profit nonnegative, treats $z$ as a free real unrelated to $p$ and $c$, or drops one of the two demand models, is a different and weaker statement and does not count.
• In milestone 1 the order-up-to levels $x^*_j$ are assumed nonnegative, the formal content of the paper's assumption $\lambda^{1-\beta}q_j\gg\sigma q_j^\beta$.

Needed infrastructure: the normal loss function and the first-order condition for the newsvendor under gaussianReal; quasiconvexity of convex-over-positive-affine ratios; concavity of weighted geometric means. The newsvendor and quasiconvexity pieces are reusable well beyond this mission. Proofs of any milestone, and alternative routes to Theorem 1 that avoid Lemma 1, are welcome.

Selected references

• G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11):1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496
• O. L. Mangasarian, Nonlinear Programming, McGraw-Hill, 1969 (reprinted SIAM Classics in Applied Mathematics 10, 1994). https://doi.org/10.1137/1.9781611971255
• R. D. Luce, Individual Choice Behavior: A Theoretical Analysis, Wiley, 1959.

Motivation

How likely is a sum of independent random variables to exceed a large level $x$? If the summands have exponential moments, the classical answer is a Bernstein- or Hoeffding-type bound, exponentially small in $x$. Many quantities met in statistics, queueing, insurance mathematics and the analysis of algorithms have only finitely many moments, and then no exponential bound can hold: the tail of the sum is at least as heavy as the tail of the largest summand. The Fuk–Nagaev inequality is the standard answer for this situation. It bounds $P(S_n\ge x)$ by a polynomial term, which accounts for one summand being large, plus a Gaussian term, which accounts for the bulk of the sum.

The inequality was proved by D. Kh. Fuk and S. V. Nagaev in 1971 (Fuk–Nagaev 1971). S. V. Nagaev's survey of 1979 in the Annals of Probability states it as Theorem 1.3 and gives a complete proof, together with its corollaries (1.23) and (1.24). The form (1.24), $P(S_n\ge x)\le c_t^{(1)}A_t^+x^{-t}+\exp\{-c_t^{(2)}x^2/B_n^2\}$, is the version quoted in the later literature on heavy-tailed sums, empirical processes and high-dimensional statistics, where it is the usual replacement for Bernstein's inequality under polynomial moments.

Setting

Let $X_1,\dots,X_n$ be independent real random variables on a probability space, with distribution functions $F_i(u)=P(X_i<u)$, and let $S_n=X_1+\dots+X_n$. Fix a level $x>0$, truncation levels $Y=\{y_1,\dots,y_n\}$ (positive numbers), and a number $y\ge\max_iy_i$.

The truncated summands are $\tilde X_i=X_i$ if $X_i\le y_i$ and $\tilde X_i=0$ if $X_i>y_i$, with sum $\tilde S_n=\sum_i\tilde X_i$. The paper writes $\mu(\cdot,\cdot)$, $B^2(\cdot,\cdot)$ and $A(t;\cdot,\cdot)$ for sums of truncated means, second moments and absolute moments of order $t$, the arguments being the truncation levels. The three used here are

$$\mu(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u\,dF_i(u),\qquad B^2(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u^2\,dF_i(u),\qquad A(t;0,Y)=\sum_{i=1}^n\int_{0\le u\le y_i}|u|^t\,dF_i(u).$$

For $t\ge2$, $0<\alpha<1$ and $\beta=1-\alpha$, write $L=\log\big(\beta xy^{t-1}/A(t;0,Y)+1\big)$ and define

$$P_4=\exp\Big\{\beta\frac xy-\Big(\big(1-\tfrac\alpha2\big)\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},\qquad P_5=\exp\Big\{\Big(\beta-\frac{t\alpha}2\Big)\frac xy-\Big(\beta\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},$$ $$P_6=\exp\Big\{-\frac{\alpha x\,(\alpha x/2-\mu(-\infty,Y))}{e^tB^2(-\infty,Y)}\Big\}.$$

Finally $A_t^+=\sum_i\int_{u\ge0}u^t\,dF_i(u)$ and $B_n^2=\sum_i\operatorname{Var}X_i$.

In Lean these are the definitions S, Xt, St, muY, B2Y, AY, Atplus, Bn2, P4, P5, P6 of NagaevLD.FukNagaev.Setting.

Formalization targets

Goal: Theorem 1.3 (p. 749)

Suppose $t\ge2$, $0<\alpha<1$, $\beta=1-\alpha$ and $B^2(-\infty,Y)<\infty$. Write (1.4) for $\max[t,L]\ge\alpha xy/(e^tB^2(-\infty,Y))$ and (1.6) for $\max[t,L]<\alpha xy/(e^tB^2(-\infty,Y))$. Then

$$\text{(1.4)}\implies P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+P_6,\qquad \text{(1.6)}\implies P(S_n\ge x)<\sum_{i=1}^nP(X_i>y_i)+P_4,$$

and if (1.6) holds together with $\beta\ge t\alpha/2$ or $\beta x\ge\mu(-\infty,Y)$, then $P(S_n\ge x)<\sum_iP(X_i>y_i)+P_5$. The page prints the last case as "if, instead of (1.6), …"; the proof on p. 752 proves it "if, in addition", and this is what is stated.

Milestones

The milestones follow the proof: the truncation inequality (1.8); the exponential Chebyshev bound with factorisation (1.9); Lemma 1.4, the cumulant bounds (1.10) and (1.11) for a variable bounded above, with the intermediate estimates (1.13) and (1.16); the bounds (1.17) and (1.18) for $P(\tilde S_n\ge x)$; the equivalence of (1.4) with $h_1\le\max[t/y,h_2]$; (1.19), $P(\tilde S_n\ge x)\le P_6$ under (1.4); $P(\tilde S_n\ge x)<P_4$ under (1.6); and (1.20), $P(\tilde S_n\ge x)<P_5$.

Corollaries

Corollary 1.7 (1.23): for $\mathbb EX_i=0$, $\beta=t/(t+2)$, $\alpha=1-\beta$,

$$P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+\exp\Big\{-\frac{\alpha^2x^2}{2e^tB^2(-\infty,Y)}\Big\}+\Big(\frac{A(t;0,Y)}{\beta xy^{t-1}}\Big)^{\beta x/y}.$$

Corollary 1.8 (1.24): for $\mathbb EX_i=0$, $A_t^+<\infty$, $t\ge2$,

$$P(S_n\ge x)\le\Big(1+\frac2t\Big)^tA_t^+x^{-t}+\exp\Big\{-\frac{2e^{-t}x^2}{(t+2)^2B_n^2}\Big\}.$$

Significance

Theorem 1.3 makes no assumption on the summands beyond independence and finiteness of the truncated moments; no centring, no identical distribution, no bound on the summands. The free parameters $y_i$, $y$, $\alpha$ let a user trade the polynomial term against the Gaussian term. Corollary 1.8 is the form used for moment bounds of sums ($t$-th moment inequalities of Rosenthal type follow by integrating it in $x$), for maximal inequalities, and for concentration of empirical processes indexed by heavy-tailed classes.

The result has been proved since 1971 and is not open. As far as a search of the Prove2Me catalog and of Mathlib shows, it has not been formalized: Mathlib has the exponential Chebyshev bound and the moment generating function of independent sums, but no tail inequality for sums of heavy-tailed summands. This mission produces a checked proof of the theorem in the paper's exact form, of the cumulant bound of Lemma 1.4, and of both corollaries with their explicit constants $(1+2/t)^t$ and $2(t+2)^{-2}e^{-t}$.

Difficulty

The obvious argument, Chernoff's bound applied to $S_n$, fails at once: without exponential moments $\mathbb Ee^{hS_n}$ is infinite for every $h>0$. Truncating the summands repairs this, but the bound then depends on the choice of the exponent $h$, and no single choice works for all parameters. The proof splits into cases according to the relative position of three numbers, $t/y$ and the minimisers $h_1$, $h_2$ of two convex functions, and every case needs its own estimate of the cumulant of a variable bounded above. The bookkeeping of strict and non-strict inequalities across these cases is exactly what (1.7) and (1.7a) assert, and the printed text has a misprint at that point.

The corollaries need a separate step: Corollary 1.7 requires $\mu(-\infty,Y)\le0$, which follows from centring only because truncation removes positive mass, and Corollary 1.8 requires combining the Chebyshev bound for $P(X_i>\beta x)$ with the truncated moment $A(t;0,Y)$ so that the two polynomial terms add to exactly $A_t^+/(\beta x)^t$.

Formalization scope

• The summands are X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); index $i$ stands for the paper's $i+1$. $x>0$, $y_i>0$, $y\ge y_i$ and $y>0$ are hypotheses ($y>0$ follows from the others when $n\ge1$).
• Every integral $\int_E\varphi(u)\,dF_i(u)$ is the expectation of $\varphi(X_i)$ over the event $\{X_i\in E\}$, with the endpoints of $E$ copied from the page. Powers with exponent $t$ are real powers; $A(t;0,Y)$ uses $|u|^t$.
• Added hypotheses. Finiteness of $B^2(-\infty,Y)$ is assumed as integrability of $X_i^2$ on $\{X_i\le y_i\}$ for each $i$; Lemma 1.4 assumes $X\in L^2$ (its $\beta=\mathbb EX^2$ is a number); Corollary 1.8 assumes each $X_i\in L^2$, since Mathlib's variance is $0$ outside $L^2$. On the page an infinite second moment makes each bound trivial; in Lean it would be replaced by $0$ and the statements would become false.
• Degenerate values. On the page $A(t;0,Y)=0$ makes $L=+\infty$, so (1.4) holds. Lean's division by $0$ would make $L=0$; condition (1.4) is therefore the definition cond_1_4, which includes the case $A(t;0,Y)=0$, and (1.6) is cond_1_6, which requires $A(t;0,Y)>0$. For $A\ge0$ the two are exact complements. If $B^2(-\infty,Y)=0$, $P_6$ and the exponential term of (1.23) take the page's limiting value $0$, and so does the exponential term of (1.24) when $B_n^2=0$; Lean's $x/0=0$ would otherwise make them $1$.
• Ruled out. Stating the goal for the truncated sum $\tilde S_n$ instead of $S_n$, or only the moment-generating-function bound, would replace the theorem by a step of its proof; the goal is about $P(S_n\ge x)$, with the strict inequalities of (1.7) and (1.7a) kept strict.
• Lemma 1.4 uses $\beta$ for $\mathbb EX^2$; it is unrelated to $\beta=1-\alpha$ of Theorem 1.3.
• Reusable beyond this mission: Lemma 1.4 (a cumulant bound for variables bounded above) and the truncation inequality (1.8). Contributions welcome on any milestone, and on the corollaries independently of the goal.

Selected references

• S. V. Nagaev, Large deviations of sums of independent random variables, Ann. Probab. 7(5):745–789, 1979. https://doi.org/10.1214/aop/1176994938
• D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory Probab. Appl. 16(4):643–660, 1971. https://doi.org/10.1137/1116071

Why the cost of path simulation matters

Pricing a financial derivative, estimating a risk measure, or computing any expected functional of a stochastic differential equation (SDE) by simulation runs into two errors at once: the statistical error of averaging finitely many sampled paths, and the discretisation bias of replacing the exact SDE solution by a numerical scheme with a positive timestep. With the Euler scheme and $N$ independent paths, the mean-square error behaves like $c_1N^{-1}+c_2h^2$, so a root-mean-square accuracy $\varepsilon$ requires $N\sim\varepsilon^{-2}$ paths of $h^{-1}\sim\varepsilon^{-1}$ steps each: a cost of order $\varepsilon^{-3}$.

Giles' Multilevel Monte Carlo path simulation (Operations Research 56(3), 2008) showed that combining simulations on a geometric hierarchy of timesteps reduces this cost to order $\varepsilon^{-2}(\log\varepsilon)^2$ for the Euler scheme with a Lipschitz payoff, and to $\varepsilon^{-2}$, the cost of an unbiased estimator, when the level differences have fast-decaying variance. The two-level case is due to Kebaier (2005), who reduced the cost to order $\varepsilon^{-2.5}$; Heinrich's multilevel method for parametric integration (2001) is a precursor. The paper's Theorem 3.1 is stated abstractly, in terms of four rate conditions, and has since been applied to SDEs, SPDEs, Markov chains and nested simulation; the survey of Giles (Acta Numerica 2015) traces this development.

The multilevel estimator

Fix an integer refinement factor $M\ge2$ and a horizon $T>0$, and let the timestep of level $l$ be $h_l=M^{-l}T$, $l=0,1,2,\dots$. On a probability space, let $P$ be the quantity of interest (in the paper, a functional of the solution of an SDE driven by a Brownian path) and $\widehat P_l$ its approximation with timestep $h_l$. Since

$$E[\widehat P_L]=E[\widehat P_0]+\sum_{l=1}^{L}E[\widehat P_l-\widehat P_{l-1}],$$

the method estimates each term independently. For each level $l$ and sample size $N_l\ge1$, $\widehat Y_l$ is an estimator of $E[\widehat P_0]$ ($l=0$) or of $E[\widehat P_l-\widehat P_{l-1}]$ ($l>0$) built from $N_l$ samples, with computational complexity $C_l$. The multilevel estimator is $\widehat Y=\sum_{l=0}^{L}\widehat Y_l$, its total complexity is $C=\sum_{l=0}^LC_l$, and its mean-square error is $\mathrm{MSE}=E[(\widehat Y-E[P])^2]$.

The hypotheses are four rate conditions, with constants $\alpha\ge\frac12$ and $\beta,c_1,c_2,c_3>0$: (i) $|E[\widehat P_l-P]|\le c_1h_l^\alpha$ (weak convergence order $\alpha$); (ii) $E[\widehat Y_l]$ equals $E[\widehat P_0]$ or $E[\widehat P_l-\widehat P_{l-1}]$ (unbiasedness of each level); (iii) $V[\widehat Y_l]\le c_2N_l^{-1}h_l^\beta$ (variance decay rate $\beta$); (iv) $C_l\le c_3N_lh_l^{-1}$ (cost proportional to samples times steps).

Formalization targets

Goal: Theorem 3.1

There is a constant $c_4>0$ such that for every $0<\varepsilon<e^{-1}$ there are $L$ and $N_l\ge1$ with

$$\mathrm{MSE}<\varepsilon^2,\qquad C\le\begin{cases}c_4\varepsilon^{-2},&\beta>1,\\ c_4\varepsilon^{-2}(\log\varepsilon)^2,&\beta=1,\\ c_4\varepsilon^{-2-(1-\beta)/\alpha},&0<\beta<1.\end{cases}$$

The constant $c_4$ is uniform in $\varepsilon$; its value is not part of the goal.

Milestones

The milestones are the displayed steps of the paper's proof, in its order: the choice of the finest level and the resulting two-sided bound (6) on $c_1h_L^\alpha$; the bound $\frac12\varepsilon^2$ on the squared bias; the geometric bound (7) on $\sum_l h_l^{-1}$; and, for each of the three regimes $\beta=1$, $\beta>1$, $\beta<1$, a choice of $N_l$ with a $\frac12\varepsilon^2$ bound on the variance (using the geometric bounds (8) and (9) in the last two) and an explicit cost bound with an explicit constant $c_4$. In case $\beta=1$ the bound $L+1\le c_5\log\varepsilon^{-1}$ on the number of levels is a separate milestone.

What the result gives

The theorem turns the multilevel idea into a complexity statement: whenever a discretisation has weak order $\alpha$ and its level corrections have variance decay $\beta$, the cost of accuracy $\varepsilon$ is known up to a constant. It identifies $\beta$ as the parameter governing the method, explains where the effort is spent (coarse levels for $\beta>1$, fine levels for $\beta<1$), and is the template that later multilevel analyses (Milstein schemes, multi-index Monte Carlo, randomised MLMC) follow and refine.

The result is proved in the paper and widely reused. To our knowledge it has no machine-checked proof. The mission produces one: a Lean statement of the abstract theorem and of each step of the proof, with the paper's explicit constants. Its probabilistic content is light (linearity of expectation, the bias-variance decomposition, Bienaymé's identity for independent variables); most of the work is careful real analysis with ceilings, logarithms and real powers.

Where the difficulty lies

No single step is deep; the difficulty is bookkeeping under exact constants. The obvious argument "choose $h_L\approx\varepsilon$, choose $N_l\propto\varepsilon^{-2}h_l^{(\beta+1)/2}$" is asymptotic. The theorem demands, for every $\varepsilon<e^{-1}$, an exact bound with a constant independent of $\varepsilon$. This forces the integer ceilings in $L$ and $N_l$ to be controlled explicitly (each ceiling adds one sample per level, whose total cost is (7)), the number of levels to be bounded by a multiple of $\log\varepsilon^{-1}$, and the three geometric series to be summed with constants independent of $L$. The strict inequality $\mathrm{MSE}<\varepsilon^2$ is not delivered by the paper's own choice in case $\beta=1$, where both halves give only $\le\frac12\varepsilon^2$; a solver must adjust the sample sizes.

Formalization scope

$P$, $\widehat P_l$ and the level estimators are arbitrary real random variables on a probability space $(\Omega,\mu)$; the SDE and its discretisation enter the theorem only through (i)–(iv), so they are not modelled. This makes the statement more general, not weaker. Expectations are Bochner integrals and $V$ is Mathlib's variance. The conventions are:

• the level estimator is indexed by level and sample size, $\widehat Y_l^{(n)}$, and (ii), (iii), (iv), square integrability and mutual independence of $(\widehat Y_l^{(N_l)})_l$ are assumed for every sample size $n\ge1$ (every choice of $N_l\ge1$), because the conclusion chooses the sample sizes;
• (i) carries an absolute value: the page prints the one-sided $E[\widehat P_l-P]\le c_1h_l^\alpha$, under which the theorem is false;
• $P$ and $\widehat P_l$ are integrable and $\widehat Y_l^{(n)}\in L^2$, because Lean's integral and variance return $0$ off these classes;
• $M\ge2$ (the paper's standing assumption), $T>0$, and $\varepsilon>0$ (implicit in "$\varepsilon<e^{-1}$");
• the cost $C_l^{(n)}$ is an abstract real number constrained only by (iv), and $C=\sum_{l=0}^LC_l$;
• $L$ in (6) is an integer ceiling, which can be negative for large $\varepsilon$; the milestones with explicit constants assume it is a natural number, a case the paper's proof assumes silently, while the goal does not;
• real powers are Real.rpow, $\lceil\cdot\rceil$ is Int.ceil for $L$ and Nat.ceil for $N_l$ (whose arguments are positive).

A formalization in which the cost is defined as $c_3\sum_lN_lh_l^{-1}$, in which (ii)–(iv) hold only for one fixed sample size, or in which the MSE and cost bounds are proved for different $L$ and $N_l$, is a different and weaker theorem and is ruled out by the statement.

Infrastructure needed: geometric-series bounds with real ratios, floor and ceiling estimates for logarithms, and Bienaymé's identity (Mathlib's IndepFun.variance_sum). The bias-variance decomposition $\mathrm{MSE}=V[\widehat Y]+(E[\widehat Y]-E[P])^2$ for $L^2$ variables is reusable beyond this mission. Proofs of individual milestones, and alternative proofs of the goal, are welcome.

Selected references

• M. B. Giles, Multilevel Monte Carlo path simulation, Operations Research 56(3):607–617, 2008. https://doi.org/10.1287/opre.1070.0496
• A. Kebaier, Statistical Romberg extrapolation: a new variance reduction method and applications to option pricing, Annals of Applied Probability 15(4):2681–2705, 2005 (cited as reference in Giles 2008, p. 617).
• M. B. Giles, Multilevel Monte Carlo methods, Acta Numerica 24:259–328, 2015. https://doi.org/10.1017/S096249291500001X
• S. Heinrich, Multilevel Monte Carlo methods, Large-Scale Scientific Computing, LNCS 2179, 58–67, Springer, 2001. https://doi.org/10.1007/3-540-45346-6_5

Motivation

Exponential tail bounds for sums of bounded martingale differences (Bernstein, Bennett, Hoeffding, Freedman) are the workhorses of probability, statistics and learning theory. They bound how far a martingale can travel in a given amount of conditional variance. The converse question is just as basic: how much conditional variance does a martingale need before it reaches a given level? An answer controls the time a martingale spends below a barrier, and it is the ingredient that turns the upper half of a law of the iterated logarithm into the lower half.

David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) derives both kinds of result from a single observation: the exponential process $Q_\lambda(T_n, S_n)$ is a supermartingale and $R_\lambda(T_n, S_n)$ a submartingale. The first gives the inequality now called Freedman's inequality (Theorem (1.6)/(4.1)); the second gives Theorem (1.8), the subject of this mission, a lower bound on the Laplace transform of the conditional variance accumulated up to the first crossing of a level. From (1.8) the paper derives Corollary (1.9), the tail bound $P\{W_a \ge b\} < 5(a+1)/b^{1/2}$, Lévy's theorem that $\sup_n S_n = \infty$ almost surely on $\{\sum V_i = \infty\}$ (Corollary (4.5)), and, through a separate analytic argument, the lower-tail bound (1.10).

Setting

Let $(\Omega, \mathcal F, P)$ be a probability space and $\mathcal F_0 \subset \mathcal F_1 \subset \cdots$ an increasing sequence of sub-$\sigma$-fields of $\mathcal F$. Let $X_1, X_2, \dots$ be real random variables with $X_n$ measurable with respect to $\mathcal F_n$, satisfying the standing condition (1.1):

$$|X_n| \le 1 \quad\text{and}\quad E\{X_n \mid \mathcal F_{n-1}\} = 0 \qquad (n \ge 1).$$

The conditional variance of the $n$-th step is $V_n = \operatorname{Var}\{X_n \mid \mathcal F_{n-1}\}$. The partial sums are $S_n = X_1 + \cdots + X_n$ and the intrinsic time is $T_n = V_1 + \cdots + V_n$, with $S_0 = T_0 = 0$.

For a real $\lambda$, let $f(\lambda) = e^{-\lambda} - 1 + \lambda$ (positive for $\lambda > 0$), and $R_\lambda(v, y) = \exp\{\lambda y - f(\lambda) v\}$.

A stopping time is a random variable $\sigma$ with values in $\{0, 1, 2, \dots, \infty\}$ such that $\{\sigma = n\} \in \mathcal F_n$ for every $n$; it is uniformly bounded if $\sigma \le N$ everywhere for some integer $N$.

Fix a level $a > 0$. The crossing time $\tau_a$ is the least $n$ with $S_n \ge a$, and $\tau_a = \infty$ if there is none. The crossing variance is

$$W_a = T_{\tau_a} = \sum_{i=1}^{\tau_a} V_i \in [0, \infty],$$

the total conditional variance the process needs to cross the level $a$ if it crosses, and otherwise the total conditional variance $\sum_{i \ge 1} V_i$, which may be infinite.

Formalization targets

Goal: Theorem (1.8)

For every $\lambda > 0$ and $a > 0$,

$$E\{\exp[-f(\lambda) W_a]\} \ge \exp[-\lambda(a+1)],$$

with the convention $\exp[-f(\lambda)\cdot\infty] = 0$.

Milestones

1. The two-point cases of (3.7): for $X$ taking only the values $-1$ and $a > 0$ (Case 1), or only $-b$ and $a$ with $0 < b \le 1$ (Case 2), with $E(X) = 0$ and $\lambda \ge 0$,

$$E\{\exp(\lambda X)\} \ge \exp\{f(\lambda) \operatorname{Var} X\}.$$

2. Inequality (3.7): the same bound for every random variable $X \ge -1$ with $E(X) = 0$.
3. Proposition (3.6): under (1.1), $E\{R_\lambda(T_\sigma, S_\sigma)\} \ge 1$ for every $\lambda \ge 0$ and every uniformly bounded stopping time $\sigma$.
4. From (4.2): $S_n \le a + 1$ for $n \le \tau_a$, and for every $n$,

$$1 \le E\{\exp[\lambda S_{\tau_a\wedge n} - f(\lambda)T_{\tau_a\wedge n}]\} \le \exp[\lambda(a+1)]\cdot E\{\exp[-f(\lambda)T_{\tau_a\wedge n}]\}.$$

Significance

The result. Theorem (1.8) says that the Laplace transform of $W_a$ cannot be small, so $W_a$ cannot be large: a bounded martingale difference sequence crosses any level after a finite amount of conditional variance with high probability. The paper turns this into the explicit tail estimate (1.9), into Lévy's theorem that a bounded martingale with divergent conditional variance is almost surely unbounded above and below, and, combined with the upper bound (4.8) on the same Laplace transform, into the lower-tail estimate (1.10) that gives the lower half of the law of the iterated logarithm for martingales in intrinsic time. Example (4.3) of the paper shows the theorem fails when the increments are only bounded below, so the two-sided bound in (1.1) is needed.

Formalizing it. The result is classical and proved in the paper; to the best of current knowledge it has no machine-checked proof. Mathlib has conditional variance, stopping times and optional stopping for bounded stopping times, but no reverse moment-generating-function inequality such as (3.7), no submartingale property for exponential processes in intrinsic time, and no crossing-time variables valued in $[0,\infty]$. The mission produces these, with the conventions at infinity made explicit, as a base for the remaining results of the paper (Corollary (1.9), Corollary (4.5), the lower-tail bound (1.10)).

Difficulty

The obvious route is optional stopping at $\tau_a$ itself. It fails: $\tau_a$ is unbounded and may be infinite with positive probability, and Proposition (3.6) holds only for uniformly bounded stopping times. The argument must stop at $\tau_a \wedge n$, use the overshoot bound $S_{\tau_a \wedge n} \le a + 1$ (which relies on $X_n \le 1$), and pass to the limit $n \to \infty$ in a way that sends the integrand to $0$ on $\{W_a = \infty\}$; the limit exchange needs $T_n \to W_a$ in $[0, \infty]$ and $f(\lambda) > 0$. A second obstacle is the one-step inequality (3.7): it is a lower bound on a moment-generating function, valid for random variables bounded only from below, where $E\exp(\lambda X)$ may be infinite; the usual convexity bounds go in the opposite direction.

Formalization scope

The source is the published Annals of Probability article (a scanned copy); all page numbers are the journal's.

Conventions. Increments are a sequence X : ℕ → Ω → ℝ used from index $1$; $X_0$ is never read. Measurability is "$X_n$ is $\mathcal F_n$-strongly measurable for $n \ge 1$", and the two parts of (1.1) are assumed almost surely. $V_n$ is Mathlib's condVar of $X_n$ given $\mathcal F_{n-1}$; under (1.1) every $X_n$ is square-integrable, so this is a genuine conditional variance and no square-integrability hypothesis is added to the martingale statements. Stopping times are Ω → WithTop ℕ (⊤ is $\infty$). $\tau_a$ is WithTop ℕ-valued and $W_a$ is $[0,\infty]$-valued (ℝ≥0∞), built from the nonnegative parts of the $V_i$, which agree with $V_i$ almost surely. The integrand of the goal is the function that equals $e^{-f(\lambda) W_a}$ on $\{W_a < \infty\}$ and $0$ on $\{W_a = \infty\}$; replacing it by $\exp(-f(\lambda)\cdot\mathrm{toReal}(W_a))$, which is $1$ on $\{W_a = \infty\}$, would formalize a strictly weaker statement and is ruled out. In (3.7), where $\exp(\lambda X)$ need not be integrable, the expectation is a lower Lebesgue integral in $[0,\infty]$, and $X$ is assumed square-integrable so that $\operatorname{Var} X$ is finite.

Corrected misprints. Definition (1.2)(e) prints $R_\lambda(v,y) = \exp\{\lambda h - f(\lambda) v\}$; $h$ is read as $y$. The display in (4.2) prints the last factor without its expectation sign; the $E$ is restored.

Ranges. The goal uses $\lambda > 0$ and $a > 0$ as in (1.2) and (1.7); (3.6), (3.7) and its two cases are stated for $\lambda \ge 0$ as on p. 107.

Lemma (3.1) ($g(x) = (e^x - 1 - x)/x^2$ is increasing), used in Case 2, is posed in the companion mission on Freedman's inequality and not here. Contributions welcome: proofs of the milestones, a general lemma that $R_\lambda(T_n, S_n)$ is a submartingale, and Corollary (1.9) as a follow-up.

Selected references

• David A. Freedman, On Tail Probabilities for Martingales, The Annals of Probability 3(1), 1975, 100–118. https://doi.org/10.1214/aop/1176996452
• Paul Lévy, Théorie de l'addition des variables aléatoires, Gauthier-Villars, 1937 (Theorem 68, p. 247, cited in (4.5)).

Motivation

A recurring task in martingale theory is to compare a sum of nonnegative random variables $z_1, z_2, \dots$ with the sum of their predictable projections $E(z_k \mid \mathcal A_{k-1})$: the conditional expectation of each term given the information available one step earlier. Such comparisons are the step that turns a statement about the conditional square function $s(f)$ of a martingale into a statement about the martingale itself, and they recur in the proofs of the Burkholder–Davis–Gundy inequalities and of their conditional variants.

In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder proves two such comparisons for a function $\Phi$ applied to the sums. For convex $\Phi$ of moderate growth, the sum of predictable projections is controlled by the sum itself, up to a constant (Lemma 16.1, the "convexity lemma", §16). For concave $\Phi$, §20 proves the reverse comparison, with the explicit constant $2$. This mission is the concave case, Theorem 20.1.

The same section derives Theorem 20.2 from it: for a martingale $f$ and concave $\Phi$, $E\Phi((f^*)^2) \le 5\,E\Phi(s^2(f))$. For the concave powers $\Phi(\lambda) = \lambda^p$, $0 < p \le 1$, that bound had been proved by another method in Burkholder, Davis and Gundy 1972. Comparisons of the same kind between an increasing process and its compensator were later systematized as the Lenglart domination principle (Lenglart 1977).

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space and $\mathcal A_0 \subseteq \mathcal A_1 \subseteq \cdots$ a non-decreasing sequence of sub-$\sigma$-fields of $\mathcal A$. In Lean this is a probability measure P together with a filtration ℱ : Filtration ℕ mΩ, ℱ k $= \mathcal A_k$.

Let $z_1, z_2, \dots$ be nonnegative measurable functions on $(\Omega, \mathcal A)$, with values in $[0, \infty]$. They need not be integrable, and they need not be adapted: $z_k$ is only $\mathcal A$-measurable. For a nonnegative function the conditional expectation $E(z_k \mid \mathcal A_{k-1})$ always exists as an $\mathcal A_{k-1}$-measurable function with values in $[0, \infty]$, determined up to null sets by $\int_A E(z_k \mid \mathcal A_{k-1})\,dP = \int_A z_k\,dP$ for $A \in \mathcal A_{k-1}$. Put

$$Z = \sum_{k=1}^\infty z_k, \qquad W = \sum_{k=1}^\infty E(z_k \mid \mathcal A_{k-1}),$$

and, for $0 \le n \le \infty$, the partial sums $Z_n$, $W_n$ over $1 \le k \le n$.

A function $\Phi : [0, \infty] \to [0, \infty]$ is concave as above in the paper's sense if it is non-decreasing and continuous on $[0, \infty]$, $\Phi(0) = 0$, it satisfies the growth condition $\Phi(2\lambda) \le c\,\Phi(\lambda)$ for $\lambda > 0$, and it is concave on $[0, \infty)$. Concavity alone already gives $\Phi(2\lambda) \le 2\Phi(\lambda)$. Examples: $\Phi(\lambda) = \lambda^p$ for $0 < p \le 1$, $\Phi(\lambda) = \lambda \wedge a$, $\Phi(\lambda) = \log(1 + \lambda)$.

For a martingale $f = (f_1, f_2, \dots)$ with differences $d_k = f_k - f_{k-1}$ ($f_0 = 0$), the maximal function is $f^* = \sup_n |f_n|$ and the conditional square function is $s(f) = \bigl[\sum_{k=1}^\infty E(d_k^2 \mid \mathcal A_{k-1})\bigr]^{1/2}$.

Formalization targets

Goal: Theorem 20.1 (p. 38)

$$E\Phi\Bigl(\sum_{k=1}^\infty z_k\Bigr) \le 2\,E\Phi\Bigl(\sum_{k=1}^\infty E(z_k \mid \mathcal A_{k-1})\Bigr)$$

for every $\Phi$ concave as above and all nonnegative measurable $z_1, z_2, \dots$. The constant $2$ is universal: it does not depend on $\Phi$, on the growth constant $c$, on the probability space or on the $z_k$.

Milestones

1. (§20, proof of Theorem 20.1.) For $\tau = \inf\{n \ge 0 : W_{n+1} > \lambda\}$: $EZ_\tau = EW_\tau \le E(W \wedge \lambda)$ and $E[\lambda I(\tau < \infty)] = \lambda P(W > \lambda) \le E(W \wedge \lambda)$.
2. (20.2) The truncated inequality

$$E(Z \wedge \lambda) \le 2\,E(W \wedge \lambda), \qquad \lambda > 0.$$

3. (§20, proof of Theorem 20.1.) Inequality (20.2) implies (20.1). This is stated for arbitrary measurable $[0, \infty]$-valued $Z$ and $W$, since the paper's argument uses nothing about $Z$ and $W$ beyond (20.2).

Further result: Theorem 20.2 (p. 39)

For a martingale $f$ and $\Phi$ concave as above,

$$E\Phi\bigl((f^*)^2\bigr) \le 5\,E\Phi\bigl(s^2(f)\bigr).$$

It is posed as a separate theorem and is not a milestone of the goal.

Significance

Theorem 20.1 holds without any integrability and without adaptedness, so it applies to arbitrary nonnegative sequences. With $z_k = d_k^2$ it compares the square function $S^2(f) = \sum d_k^2$ of a martingale with $s^2(f)$: for concave $\Phi$, $E\Phi(S^2(f)) \le 2E\Phi(s^2(f))$. Together with the Burkholder–Davis–Gundy comparison of $S(f)$ and $f^*$, this is one route from the conditional square function to the maximal function in the range of exponents $p \le 2$, where the convex methods of the rest of the paper do not apply. Theorem 20.2 is the result of this kind that the paper states.

The paper proves Theorem 20.1 in about half a page. As far as is known, neither Theorem 20.1 nor Theorem 20.2 has been formalized in any proof assistant. Mathlib provides the $[0, \infty]$-valued conditional expectation (condLExp), filtrations, stopping times and Lebesgue integrals of extended nonnegative functions. It has no comparison theorem of this type between a sum and its predictable projections. A formal proof would therefore add a new, reusable tool to Mathlib's discrete-time martingale library, one that an eventual formal Lenglart inequality or conditional BDG inequality would need.

Difficulty

The obvious first idea is Jensen's inequality for conditional expectations. For concave $\Phi$ it gives $E(\Phi(z_k) \mid \mathcal A_{k-1}) \le \Phi(E(z_k \mid \mathcal A_{k-1}))$ term by term, but $\Phi$ of a sum is not the sum of the $\Phi$'s, and summing the termwise bounds loses the comparison. Another first idea, comparing $EZ$ and $EW$ (which are equal by the tower property), handles only linear $\Phi$, and both sides may be infinite.

The content lies in two places. The first is the truncated inequality for $\Phi(t) = t \wedge \lambda$, where neither $Z$ nor $W$ is integrable in general and the comparison must hold level by level. The second is the passage from the truncated family to an arbitrary concave $\Phi$. It needs a representation of concave $\Phi$ through the truncations $t \wedge \lambda$, including the cases $t = 0$ and $t = \infty$ and a possibly infinite right derivative at $0$ (as for $\lambda^p$). Both steps must be carried out in $[0, \infty]$ arithmetic.

Formalization scope

• Values in $[0, \infty]$. $z_k$, the sums $Z$, $W$, $\Phi$ and all expectations are ℝ≥0∞-valued; expectations are lower Lebesgue integrals ∫⁻. The conditional expectation is Mathlib's condLExp (notation P⁻[z | ℱ k]), never the Bochner P[z | ℱ k]. The Bochner version is $0$ on non-integrable functions and would make the goal false (take $W = 0$).
• Indexing. z (k+1) is $z_{k+1}$ and is paired with ℱ k $= \mathcal A_k$, so $z_1$ is conditioned on $\mathcal A_0$, as in the paper. z 0 is unused.
• "Concave as above" is IsPhi Φ c for an arbitrary constant c, together with IsConcavePhi Φ: concavity of $t \mapsto \Phi(t)$ on $[0, \infty)$, read through real values. This is honest because IsPhi forces $\Phi$ to be finite on finite arguments. The growth condition is required for every $x \in [0, \infty]$, which is equivalent to (6.1) by continuity. The paper's exclusion of $\Phi \equiv 0$ is dropped, since the conclusion is trivial there.
• Measurability. The $z_k$ are $\mathcal A$-measurable and are not assumed adapted. $\lambda$ in (20.2) is a positive real (l : ℝ≥0).
• Theorem 20.2 uses Mathlib's Martingale f ℱ P. It reads f n only for $n \ge 1$, with the paper's convention $f_0 = 0$. Mathlib's extra constraint on f 0 is no restriction, since every martingale of the paper extends by $f_0 := E(f_1 \mid \mathcal A_0)$.
• Ruled out. Assuming the $z_k$ integrable or square integrable, using the Bochner conditional expectation, or letting the constant depend on $\Phi$ would each change the theorem. None of them is used.
• Infrastructure. A complete development needs the tower and pull-out properties of condLExp for indicators of $\mathcal A_{k-1}$-sets, monotone convergence for condLExp, and the integral representation of a concave non-decreasing $\Phi$ with $\Phi(0) = 0$ as a mixture of the functions $t \mapsto t \wedge \lambda$ plus a linear part. The last is reusable well beyond this mission. Contributions to any of these are welcome.

Selected references

• D. L. Burkholder, Distribution Function Inequalities for Martingales, Annals of Probability 1(1), 19–42, 1973. https://doi.org/10.1214/aop/1176997023
• D. L. Burkholder, B. J. Davis and R. F. Gundy, Integral inequalities for convex functions of operators on martingales, Proc. Sixth Berkeley Symp. Math. Statist. Prob. 2, 223–240, 1972. https://projecteuclid.org/proceedings/berkeley-symposium-on-mathematical-statistics-and-probability/Proceedings-of-the-Sixth-Berkeley-Symposium-on-Mathematical-Statistics-and/Chapter/Integral-inequalities-for-convex-functions-of-operators-on-martingales/bsmsp/1200514225
• E. Lenglart, Relation de domination entre deux processus, Annales de l'Institut Henri Poincaré B 13(2), 171–179, 1977. http://www.numdam.org/item/AIHPB_1977__13_2_171_0/
• A. Zygmund, Trigonometric Series, Vol. I, Cambridge University Press, 1959 (the concave-function representation the paper cites, p. 24). https://doi.org/10.1017/CBO9781316036587