Probability

Operations Research Optimization·Captain: mikedeng1

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments II: Optimal Variety Rises with Price and Store Volume and Falls as the No-Purchase Preference VanishesResearch Paper

Motivation

A retailer deciding how many variants of a product to carry (colours, sizes, flavours) faces a trade-off. A broader assortment captures customers whose favourite variant would otherwise be missing, but it splits demand into more, smaller streams, each of which needs its own safety stock. van Ryzin and Mahajan (Management Science 45(11), 1999) combine a multinomial logit model of customer choice with a newsvendor model of inventory and show that the optimal assortment always consists of the $k$ most popular variants for some $k$ (their Theorem 1). That reduces "how much variety" to a single index, and the paper's Theorem 2 then answers which economic parameters push that index up or down: the selling price, the strength of the customers' outside option, and the store's traffic volume. These comparative statics are the paper's main managerial predictions (high-margin categories and high-traffic "super stores" carry more variety; categories with a weak outside option carry less), and they are what later work on assortment planning cites the model for.

Setting

There are $n$ variants $N=\{1,\dots,n\}$ . Variant $j$ has a preference $v_j>0$ and the option of buying nothing has preference $v_0>0$ . The variants are numbered so that $v_1\ge v_2\ge\dots\ge v_n$ , and $A_i=\{1,\dots,i\}$ denotes the set of the $i$ most popular variants ( $A_0=\emptyset$ , $A_n=N$ ).

When the store offers an assortment $S\subseteq N$ , each customer buys variant $j\in S$ with the multinomial logit share

q_j(S)=\frac{v_j}{\sum_{k\in S}v_k+v_0}.

Each variant sells at price $p$ and costs $c$ per unit, with $0<c<p$ . Let $\Phi$ be the standard normal distribution function and define the critical fractile $z=\Phi^{-1}(1-c/p)$ ; it moves with $p$ .

Two models of aggregate demand are compared. In the independent population model, $\lambda>0$ customers arrive on average, demand for variant $j$ is normal with mean $\lambda q_j$ and standard deviation $\sigma(\lambda q_j)^\beta$ , where $\sigma>0$ and $0\le\beta<1$ , and each variant is stocked at its newsvendor optimum. The resulting optimal expected profit is

\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 .

In the trend-following population model all $\lambda$ customers make the same choice, so variant $j$ sells $\lambda$ units with probability $q_j$ and nothing otherwise, and the optimal expected profit is

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

Inside the proofs, $t_j$ and $w_j$ denote the shares on $A_i$ and on $A_{i+1}$ .

Formalization targets

Goal: Theorem 2 (p. 1504)

For all $n>i\ge1$ :

\text{(a)}\quad \pi(A_{i+1},v)>\pi(A_i,v)\ \text{ for all sufficiently high } p,\ \text{for } \pi=\pi_I \text{ and } \pi=\pi_T;

\text{(b)}\quad \pi(A_{i+1},v)<\pi(A_i,v)\ \text{ for all sufficiently small } v_0>0,\ \text{for } \pi=\pi_I \text{ and } \pi=\pi_T;

\text{(c)}\quad \pi_I(A_{i+1},v)>\pi_I(A_i,v)\ \text{ for all sufficiently large } \lambda .

The goal is a single Lean theorem whose conjuncts are (a), (b) and (c), each for every admissible value of the parameters held fixed. In the trend-following half of (b) it carries the extra hypothesis $p\,v_1>c\sum_{j\le i}v_j$ ; see Formalization scope.

Milestones

Equation (6): the critical fractile is the unique solution of $\Phi(z)=1-c/p$ .
Equation (13): $\pi_I(A_{i+1},v)\ge\pi_I(A_i,v)$ if and only if

\Big(1-\frac cp\Big)\frac{\sqrt{2\pi}}{\sigma}\lambda^{1-\beta}e^{z^2/2}\ \ge\ \frac{\sum_{j\le i+1}w_j^\beta-\sum_{j\le i}t_j^\beta}{\sum_{j\le i+1}w_j-\sum_{j\le i}t_j},

together with the strict version. 3. Equation (14): $\pi_T(A_{i+1},v)\ge\pi_T(A_i,v)$ if and only if $\sum_{j\le i+1}(pw_j-c)^+\ge\sum_{j\le i}(pt_j-c)^+$ , with the strict version. 4. $z$ and the left side of (13) are increasing in $p$ on $(c,\infty)$ . 5. As $v_0\to0$ , $q_j\to v_j/\sum_{k\in S}v_k$ , so $\sum w_j-\sum t_j\to0$ . 6. As $v_0\to0$ , the numerator of the right side of (13) converges to a positive constant. 7. The left side of (13) is increasing (and unbounded) in $\lambda$ .

Significance

The result. Theorem 2 gives three qualitative predictions with opposite signs, all from one model: higher margins favour broader assortments, a vanishing outside option favours narrower ones (customers then buy something regardless, so extra variants mainly cannibalise each other and add safety stock), and in the independent model higher volume favours broader assortments through risk pooling, a scale economy that the trend-following model does not have because its profit is proportional to $\lambda$ . Combined with Theorem 1 these statements locate the optimal number of variants, not only its direction of change.

Formalizing it. The theorem is proved in the paper, but the published argument is a sketch: the positivity of the limiting numerator in (b) is asserted ("one can easily show"), and the trend-following half of (b) is dispatched in one sentence that does not cover every case (see below). A machine-checked development fixes exactly which hypotheses each part needs. No part of this paper has been formalized before, and Mathlib has no normal quantile function; the development of $\Phi^{-1}$ and of the monotonicity of $(1-c/p)e^{z^2/2}$ in $p$ is reusable for any newsvendor analysis.

Difficulty

The comparisons are between finite sums of real powers of shares whose denominators all move with the parameter. Three steps are not routine. For (a), the left side of (13) is a product of $1-c/p$ and $e^{z^2/2}$ , and $e^{z^2/2}$ is not monotone in $p$ (it decreases while $z<0$ , i.e. while $p<2c$ ); so monotonicity of the product depends on the shape of the normal distribution, and part (a) also needs this left side to grow without bound, which the paper does not state. For (b), the positivity of the limiting numerator is where the ordering $v_1\ge\dots\ge v_n$ and $\beta<1$ enter; it fails for unordered preferences. For the trend-following half of (b), the positive parts $(\cdot)^+$ make the comparison piecewise, and the strict inequality can fail outright.

Formalization scope

All objects live in RetailVariety.Statics. Variants are Fin n, 0-based (the paper's variant $j$ is ⟨j-1, _⟩), and $A_i$ is A n i, the indices with value below $i$ , so $A_0=\emptyset$ . The preferences are v : Fin n → ℝ with 0 < v j and Antitone v; $v_0$ is a separate real v0, not a variant. The shares are share v v0 S j. $\Phi$ is ProbabilityTheory.cdf (gaussianReal 0 1), and $z$ is criticalFractile p c, the infimum of $\{x:\Phi(x)\ge1-c/p\}$ ; it is a function of $p$ , never a free parameter. Powers are real powers (Real.rpow); shares of offered variants are positive, so the convention $0^0=1$ does not enter. $(x)^+$ is max x 0. Price, cost, volume, $\sigma$ , $\beta$ and $v_0$ are explicit arguments of profitI and profitT.

"Sufficiently high/low" is encoded as an eventual statement: ∀ᶠ p in atTop, ∀ᶠ v0 in 𝓝[>] 0 (a right limit, since $v_0>0$ ), ∀ᶠ lam in atTop. Fixed parameters stay in the paper's ranges: $c>0$ , $\sigma>0$ , $0\le\beta<1$ throughout, $\lambda>0$ and $v_0>0$ in (a), $c<p$ in (b) and (c).

One deviation from the printed statement. In the trend-following model, part (b) as printed is false: with $n=3$ , $v=(1,1,1)$ , $i=2$ and $p=1.5c$ , every share is below $1/2$ , so $\pi_T(A_2,v)=\pi_T(A_3,v)=0$ for every $v_0>0$ . The goal therefore assumes $p\,v_1>c\sum_{j\le i}v_j$ for that conjunct only (the most popular variant earns a positive margin on $A_i$ when $v_0\to0$ ); the condition is also necessary for the strict inequality.

Formalizations that would trivialize the mission are ruled out: an existential ("for some $p$ ") in place of the eventual quantifiers; non-strict inequalities in the goal; a critical fractile $z$ independent of $p$ ; dropping the trend-following half of (a); and equal preferences or a fixed number of variants.

Needed infrastructure: the normal quantile and its basic properties, monotonicity facts about the normal distribution function and density, limits of the shares as $v_0\to0$ , and elementary inequalities for $x\mapsto x^\beta$ with $0\le\beta<1$ . Proofs of any milestone, and of the quantile facts as standalone lemmas, are welcome.

Selected references

G. van Ryzin and 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

9 thms2 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

Coalescents With Multiple Collisions 2: Coagulating an (α, θ) Partition by (β, θ/α) Equals Fragmenting an (αβ, θ) Partition by (α, −αβ)Research Paper

Motivation

Random partitions of the positive integers $\mathbb N=\{1,2,\dots\}$ are the common language of population genetics, Bayesian nonparametrics and the theory of coalescent processes. When a sample of genes, customers or particles is grouped into classes, the grouping is a partition, and in most models its law is exchangeable: it does not depend on the labels. The best-known example is the Ewens sampling formula of population genetics (Ewens 1972); Kingman's representation theory (Kingman 1978) describes all exchangeable random partitions of $\mathbb N$ .

Pitman's two-parameter family of exchangeable partitions, the $(\alpha,\theta)$ partitions (Pitman 1995; Pitman and Yor 1997), contains Ewens' family as $\alpha=0$ and is the partition counterpart of the two-parameter Poisson–Dirichlet distribution. Theorem 12 of Pitman 1999 shows that two natural random operations act on this family in a dual way: merging blocks of an $(\alpha,\theta)$ partition according to an independent exchangeable partition (coagulation) and splitting each block of an $(\alpha\beta,\theta)$ partition by independent exchangeable partitions (fragmentation) produce the same joint law of a fine and a coarse partition. The paper uses it to describe the Bolthausen–Sznitman coalescent (Bolthausen and Sznitman 1998).

Timeline. 1972: Ewens' sampling formula, the case $\alpha=0$ . 1978: Kingman's correspondence between exchangeable partitions and random mass partitions. 1995: Pitman introduces exchangeable partition probability functions and the $(\alpha,\theta)$ formula (15). 1997: Pitman and Yor study the two-parameter Poisson–Dirichlet law. 1999: this paper proves the coagulation–fragmentation duality (Theorem 12) and its sharper converse, by reduction to an identity between explicit formulas. The duality is treated again in Pitman's lecture notes Combinatorial Stochastic Processes (2006).

Setting

A partition of a set is a collection of disjoint nonempty blocks whose union is the set. Write $\mathcal P_n$ for the partitions of $[n]=\{1,\dots,n\}$ and $\mathcal P_\infty$ for those of $\mathbb N$ ; the restriction $R_n\pi$ of $\pi\in\mathcal P_\infty$ to $[n]$ keeps the nonempty sets $A\cap[n]$ . $\mathcal P_\infty$ carries the $\sigma$ -algebra generated by the $R_n$ . Writing $\pi=\{A_1,A_2,\dots\}$ lists the blocks in increasing order of least elements.

A random partition $\Pi$ of $\mathbb N$ is exchangeable with EPF $p$ if for every $n$ and every partition $\{B_1,\dots,B_k\}$ of $[n]$ ,

\mathbb P\big(R_n\Pi=\{B_1,\dots,B_k\}\big)=p(|B_1|,\dots,|B_k|).

For $0\le\alpha<1$ and $\theta>-\alpha$ the $(\alpha,\theta)$ EPF is

p_{\alpha,\theta}(n_1,\dots,n_k)=\frac{[\theta/\alpha]_k}{[\theta]_n}\prod_{i=1}^k-[-\alpha]_{n_i},\qquad [x]_m=\prod_{i=1}^m(x+i-1),\quad n=\textstyle\sum_i n_i,

with factors of $\alpha$ and $\theta$ cancelled before evaluation when $\alpha=0$ or $\theta=0$ . An $(\alpha,\theta)$ partition is an exchangeable random partition with EPF $p_{\alpha,\theta}$ .

Coagulation (Definition 5): for $\pi=\{A_1,A_2,\dots\}$ and $\gamma=\{B_1,B_2,\dots\}$ , the $\gamma$ -coagulation of $\pi$ has blocks $\bigcup_{j\in B_i}A_j$ . $\Pi'$ is a $p$ -coagulation of $\Pi$ if, given $\Pi=\pi$ , it is the $\gamma$ -coagulation of $\pi$ for an independent $\gamma$ with EPF $p$ . Fragmentation (Definition 11): $\Pi$ is a $p$ -fragmentation of $\Pi'$ if, given $\Pi'=\pi'$ , $\Pi$ restricted to the $m$ -th block of $\pi'$ equals $\Gamma^{(m)}$ restricted to that block, for independent $\Gamma^{(1)},\Gamma^{(2)},\dots$ with EPF $p$ . In Lean these are coag, frag, pdEPF and IsEPFLaw in LambdaCoalescent.CoagFrag.Setting.

Formalization targets

Goal: Theorem 12

For $0<\alpha<1$ , $0\le\beta<1$ , $\theta>-\alpha\beta$ , the following are equivalent: (i) $\Pi$ is an $(\alpha,\theta)$ partition and $\Pi'$ is a $(\beta,\theta/\alpha)$ -coagulation of $\Pi$ ; (ii) $\Pi'$ is an $(\alpha\beta,\theta)$ partition and $\Pi$ is an $(\alpha,-\alpha\beta)$ -fragmentation of $\Pi'$ . Formally, with laws $\mu,\nu,\rho,\kappa$ of EPFs $p_{\alpha,\theta},p_{\beta,\theta/\alpha},p_{\alpha\beta,\theta},p_{\alpha,-\alpha\beta}$ :

(\mu\otimes\nu)\{(\pi,\gamma):(\pi,\mathrm{coag}(\pi,\gamma))\in S\}=(\rho\otimes\kappa^{\otimes\mathbb N})\{(\pi',\Gamma):(\mathrm{frag}(\pi',\Gamma),\pi')\in S\}

for every measurable $S\subseteq\mathcal P_\infty\times\mathcal P_\infty$ .

Milestones

Lemma 9 (existence): for $0\le\alpha<1$ , $\theta>-\alpha$ a law with EPF $p_{\alpha,\theta}$ exists.
Lemma 34: $\Pi^2$ is a $p$ -coagulation of $\Pi^1$ with EPF $p_1$ iff $\mathbb P(\Pi^1_n=\pi^1,\Pi^2_n=\pi^2)=p_1(a_1,\dots,a_K)\,p(j_1,\dots,j_k)$ for refining pairs.
Lemma 35: the fragmentation analogue, $\prod_i\hat p(a_{i,1},\dots,a_{i,j_i})\,p_2(b_1,\dots,b_k)$ .
The EPF identity in the proof of Theorem 12: (62) equals (63) for the four laws of Theorem 12.
The sharper form: for parameters in $\mathrm{PAR}=\{0\le\alpha<1,\theta>-\alpha\}$ the two joint laws agree iff $\alpha_f=\alpha$ , $\theta_f=-\alpha_1=-\alpha\alpha_c$ , $\theta_c=\theta/\alpha$ , $\theta_1=\theta$ (64).

Significance

Theorem 12 identifies one law of a nested pair of exchangeable partitions from both ends. Read from (i) to (ii), it shows that coagulating an $(\alpha,\theta)$ partition by an independent $(\beta,\theta/\alpha)$ partition yields an $(\alpha\beta,\theta)$ partition; read backwards, that an $(\alpha\beta,\theta)$ partition fragmented by $(\alpha,-\alpha\beta)$ partitions yields an $(\alpha,\theta)$ partition. Through Kingman's correspondence it gives Corollary 13 on Poisson–Dirichlet laws, and with $\beta=0$ it connects the two-parameter family with Ewens' family. In the paper it is the tool for describing the Bolthausen–Sznitman coalescent through Poisson–Dirichlet laws. The sharper form shows the parameter relations (64) are forced.

The theorem has been proved since 1999. What this mission adds is a machine-checked development: exchangeable random partitions of $\mathbb N$ with their EPFs, the coagulation and fragmentation kernels, and the reduction of identities between laws on $\mathcal P_\infty$ to identities between finite-dimensional formulas. None of these objects is in Mathlib, and no formalization of the duality is known.

Difficulty

The algebraic heart, the EPF identity, is a finite computation with rising factorials. The difficulty is measure-theoretic and combinatorial. A law on $\mathcal P_\infty$ must be pinned down by its values on the cylinder events $\{R_n\pi=\pi_n\}$ . Computing $\mathbb P(R_n\Pi=\pi^1,R_n\Pi'=\pi^2)$ under the coagulation kernel requires that the blocks of $\pi$ meeting $[n]$ are exactly the first $K$ blocks in order of least elements, and that the induced partition of $[K]$ has law given by the EPF; under the fragmentation kernel it requires the independence of the $\Gamma^{(m)}$ and that the restriction of an exchangeable partition to an arbitrary finite set (not an initial segment $[b]$ ) is governed by the same EPF. The converse in Lemmas 34 and 35 needs the bookkeeping that the formula on refining pairs exhausts total mass. Lemma 9 is an existence theorem for a projective family of laws, which the paper cites rather than proves.

Formalization scope

A partition of $\mathbb N$ is an equivalence relation on Lean's $\mathbb N=\{0,1,\dots\}$ (PInf := Setoid ℕ), a partition of $[n]$ one on Fin n; labels shift by one, which preserves the order of least elements, and block indices are 0-based. The $\sigma$ -algebra on PInf is generated by the coordinates $i\sim_\pi j$ , equivalently by the $R_n$ . Coagulation is stated with $\gamma\in\mathcal P_\infty$ (Definition 5's case $n=\infty$ ). The EPF is the cancelled form

p_{\alpha,\theta}(n_1,\dots,n_k)=\frac{\prod_{i=1}^{k-1}(\theta+i\alpha)}{[\theta+1]_{n-1}}\prod_{i=1}^k[1-\alpha]_{n_i-1},

equal to (15) for $\alpha,\theta\ne0$ ; this is needed because $\theta_f=-\alpha\beta=0$ at $\beta=0$ . Conditional laws "for all $\pi$ " are encoded as joint laws, and equalities of laws are stated on preimages of measurable sets, so no Measure.map of an unproved-measurable map appears. Fragmenting partitions are one sample of Measure.infinitePi (fun _ => κ). In the sharper form, $\theta_c=\theta/\alpha$ is written as $\alpha\theta_c=\theta$ , since PAR allows $\alpha=0$ .

Not formalized: the stick-breaking characterization (12)–(13) in Lemma 9, Corollary 13 and Kingman's correspondence, and the auxiliary fact " $\prod[-\alpha]_{n_i}=c_{n,k}\prod[-\beta]_{n_i}\Rightarrow\alpha=\beta$ ", which as printed fails at $\alpha=0$ .

A formalization in which no measure satisfies IsEPFLaw (pdEPF α θ) would make Theorem 12 and Lemmas 34–35 vacuous; Lemma 9 rules this out and must be proved for the parameters used, not assumed.

Infrastructure needed: cylinder-set uniqueness on PInf, the law of the restriction of an exchangeable partition to a finite set, block enumeration by least elements, and rising-factorial algebra (ascPochhammer). The partition, EPF and kernel definitions are reusable for any work on exchangeable partitions, Chinese restaurant processes or $\Lambda$ -coalescents. Proofs of Lemma 9, of Lemmas 34–35 and of the EPF identity are each welcome as independent contributions.

Selected references

J. Pitman, Coalescents with multiple collisions, Ann. Probab. 27(4) (1999), 1870–1902. https://doi.org/10.1214/aop/1022874819
J. Pitman, Exchangeable and partially exchangeable random partitions, Probab. Theory Related Fields 102 (1995), 145–158. https://doi.org/10.1007/BF01213386
J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2) (1997), 855–900. https://doi.org/10.1214/aop/1024404422
J. F. C. Kingman, The representation of partition structures, J. London Math. Soc. (2) 18 (1978), 374–380. https://doi.org/10.1112/jlms/s2-18.2.374
W. J. Ewens, The sampling theory of selectively neutral alleles, Theor. Popul. Biol. 3 (1972), 87–112. https://doi.org/10.1016/0040-5809(72)90035-4
E. Bolthausen and A.-S. Sznitman, On Ruelle's probability cascades and an abstract cavity method, Comm. Math. Phys. 197 (1998), 247–276. https://doi.org/10.1007/s002200050450
J. Pitman, Combinatorial Stochastic Processes, Lecture Notes in Mathematics 1875, Springer, 2006. https://doi.org/10.1007/b11601500

8 thms2 active usersReviewed

Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 4: The Density of V_1 under PD(α, θ) Is Determined by the PD(α, α + θ) Law of V_1Research Paper

Motivation

A random discrete distribution is a random sequence of frequencies $V_1 \ge V_2 \ge \cdots \ge 0$ with $\sum_n V_n = 1$ . Such sequences model the relative sizes of species in a large population, of allele classes in population genetics, of cycles of a random permutation, of prime factors of a random integer, and of the excursion intervals of a Brownian motion or Bessel process. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ , $0 \le \alpha < 1$ , $\theta > -\alpha$ , contains Kingman's one-parameter law $\mathrm{PD}(0,\theta)$ (Ewens sampling formula, random permutations) and the law $\mathrm{PD}(\alpha, 0)$ of the ranked jumps of a stable subordinator. It is the reference prior in Bayesian nonparametrics (the Pitman–Yor process) and the reference model in the combinatorics of random partitions.

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), extend what was known for $\mathrm{PD}(0,\theta)$ and $\mathrm{PD}(\alpha,0)$ to the whole family. This mission formalizes one of their results: an identity (Proposition 19, p. 867) that describes the law of the largest frequency $V_1$ under $\mathrm{PD}(\alpha,\theta)$ through the law of the largest frequency under $\mathrm{PD}(\alpha,\alpha+\theta)$ .

Timeline. McCloskey (1965) showed that sampling from $\mathrm{PD}(0,\theta)$ discovers the frequencies in the stick-breaking order of independent $\mathrm{beta}(1,\theta)$ variables. Dickman (1930) found the distribution of the largest prime factor; Vershik (1986) recorded it as the case $\alpha = 0$ , $\theta = 1$ of an equation of this form. Engen (1978) introduced the two-parameter stick-breaking scheme for $\theta > 0$ . Perman, Pitman and Yor (1992) and Pitman (1996) proved that this scheme is the size-biased permutation of the ranked frequencies for the whole parameter range (Proposition 2 here). Pitman and Yor (1997) derived (52) for all $0 \le \alpha < 1$ , $\theta > -\alpha$ .

Setting

Fix $0 \le \alpha < 1$ and $\theta > -\alpha$ . Let $\tilde Y_1, \tilde Y_2, \dots$ be independent random variables, $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha, \theta + n\alpha)$ , with density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$ for $a = 1-\alpha$ , $b = \theta+n\alpha$ . Break a stick of length one:

\tilde V_1 = \tilde Y_1, \qquad \tilde V_n = (1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\,\tilde Y_n \quad (n \ge 2). \tag{4}

Let $V_1 \ge V_2 \ge \cdots$ be the ranked values of the pieces $\tilde V_n$ . The law of $(V_n)$ is $\mathrm{PD}(\alpha,\theta)$ (Definition 1, p. 857); $P_{\alpha,\theta}$ denotes probability for this construction.

A random variable $\tilde V_1$ is a size-biased pick from $(V_n)$ if $P(\tilde V_1 = V_n \mid V_1, V_2, \dots) = V_n$ for every $n$ : it is the frequency of the species of an individual drawn at random. A size-biased permutation continues the sampling without replacement, (2) and p. 857. A sample from $(V_n)$ is a random index $N$ with $P(N = n \mid V) = V_n$ (113).

In Lean all sequences are ℕ → ℝ, 0-based (V ω 0 is $V_1$ ); the objects are stick, ranked, IsStickLaw, HasPD, IsSizeBiasedPick, IsSizeBiasedPerm, IsSample, deleteAt, insertAt in the namespace PoissonDirichlet.MaxDensity.

Formalization targets

Goal: Proposition 19, identity (52)

For $0 \le \alpha < 1$ , $\theta > -\alpha$ , the variable $V_1$ lies in $(0,1)$ almost surely and

\frac{P_{\alpha,\theta}(V_1 \in dx)}{dx} = \frac{\Gamma(\theta+1)}{\Gamma(\theta+\alpha)\Gamma(1-\alpha)}\, x^{-\alpha-1}(1-x)^{\alpha+\theta-1}\; P_{\alpha,\alpha+\theta}\!\left(V_1 < \frac{x}{1-x}\right), \qquad 0 < x < 1.

Milestones

Proposition 2 (p. 857): $V_1 > V_2 > \cdots > 0$ , $\sum_n V_n = 1$ a.s., and $(\tilde V_n)$ is a size-biased permutation of $(V_n)$ .
Corollary 3 (p. 858): every size-biased pick from a $\mathrm{PD}(\alpha,\theta)$ sequence has the $\mathrm{beta}(1-\alpha,\theta+\alpha)$ law.
Display (6) (p. 858): $E\sum_n f(V_n) = E[f(\tilde V_1)/\tilde V_1] = \frac{\Gamma(\theta+1)}{\Gamma(\theta+\alpha)\Gamma(1-\alpha)}\int_0^1 f(u)(1-u)^{\alpha+\theta-1}u^{-\alpha-1}\,du$ .
The stick-tail identity (p. 876): $(\tilde V_2, \tilde V_3, \dots)/(1-\tilde V_1)$ has the $P_{\alpha,\alpha+\theta}$ law of $(\tilde V_1, \tilde V_2, \dots)$ , independently of $\tilde V_1$ .
Display (91) (p. 876): $P_{\alpha,\theta}(V_1 \in dx, V_1 = \tilde V_1) = x\,P_{\alpha,\theta}(V_1 \in dx)$ .
Display (92) (p. 876): the same quantity equals $\frac{\Gamma(\theta+1)}{\Gamma(\theta+\alpha)\Gamma(1-\alpha)}x^{-\alpha}(1-x)^{\alpha+\theta-1}\,dx\,P_{\alpha,\alpha+\theta}(V_1 < x/(1-x))$ .
Uniqueness (p. 877): (52), imposed for all $\theta > -\alpha$ , determines the family of laws of $V_1$ .
Propositions 34 and 35 (p. 881): deleting a sampled frequency and renormalising maps $\mathrm{PD}(\alpha,\theta)$ to $\mathrm{PD}(\alpha,\theta+\alpha)$ , independently of $V_N \sim \mathrm{beta}(1-\alpha,\theta+\alpha)$ ; inserting an independent beta variable reverses it.

Significance

The result. The law of $V_1$ under $\mathrm{PD}(\alpha,\theta)$ has no closed form. Identity (52) is a functional equation in the parameter: on $(1/2,1)$ the last factor equals one and the density is explicit; on $(1/(n+1), 1/n)$ it is expressed through the law of $V_1$ under $\mathrm{PD}(\alpha,\alpha+\theta)$ on $(1/n, 1)$ . Specialised to $\alpha = 0$ , $\theta = 1$ it is Dickman's equation for the largest prime factor of a random integer and for the longest cycle of a random permutation. The size-biased tools of the milestones (Corollary 3, (6), Propositions 34 and 35) are the standard way to compute with $\mathrm{PD}(\alpha,\theta)$ and its partition structure.

Formalizing it. All results here are proved in the literature; none is formalized. Mathlib has the beta distribution, infinite product measures, independence and conditional expectation, but no random discrete distributions, no ranking of a countable sequence, and no size-biased sampling. The mission produces these objects and the first theorems about them: the identification of the stick-breaking scheme with the size-biased permutation of the ranked frequencies (cited by the paper, not proved there), the structural distribution, and the density identity.

Difficulty

The obvious obstacle is Proposition 2: the identification of the stick-breaking order with the size-biased order of the ranked values is a statement about conditional probabilities given an infinite sequence, it is only cited in the paper, and its proof (Perman–Pitman–Yor, Pitman) goes through exchangeable partitions or Poisson point processes. Everything else in the mission rests on it. A second obstacle is the events themselves: $\{V_1 = \tilde V_1\}$ coincides with $\{\max_{n \ge 2}\tilde V_n < \tilde V_1\}$ only because the pieces are almost surely distinct, and conditioning on $\tilde V_1 = x$ needs the independence of the renormalised tail from $\tilde V_1$ , which is not a pointwise identity but a statement about infinite product measures. Reading (52) off the page as a pointwise identity of densities is not enough: densities are defined only almost everywhere.

Formalization scope

The parameter range $0 \le \alpha < 1$ , $\theta > -\alpha$ of Definition 1 is a hypothesis of every statement; $\alpha = 0$ is included. A sequence "has the $\mathrm{PD}(\alpha,\theta)$ distribution" (HasPD) if it is a.e.-measurable and, for some law $\mu$ of independent beta variables as in Definition 1 (IsStickLaw), $P(V \in S) = \mu(\text{ranked stick} \in S)$ for every measurable $S$ . Ranked values are defined with Set.encard, so infinitely many large terms are never counted as zero. Conditional probabilities are conditional expectations of indicators; size-biased picks, permutations and samples are measurable random variables, an assumption the page makes implicitly. Expectations of nonnegative functions are lower Lebesgue integrals. The density identity is an equality of measures on Borel subsets of $(0,1)$ , with two probability spaces for the two parameter values. Indices are 0-based. Insertion (p. 881) is defined with the index $n-1$ for the shifted tail, where the page prints $n+1$ .

The formalization rules out the trivial readings: no Measure.map of a possibly non-measurable map (which would be the zero measure), no Set.ncard in the ranking, no Bochner integral of a possibly non-integrable function (whose value would be $0$ ), no limUnder, and no dropped parameter range. Corollary 3 quantifies over every pick from every $\mathrm{PD}(\alpha,\theta)$ sequence, not over the stick-breaking construction where it is the hypothesis. A sorry-free check shows that IsStickLaw is inhabited for every admissible $(\alpha,\theta)$ , so HasPD is not vacuous.

Contributions are welcome at every level: measurability of ranked, the law of the renormalised stick tail (infinite product measures), Proposition 2 through exchangeable partitions, and the recursion of the uniqueness statement, which is pure measure theory. The definitions are reusable by the other missions of this series.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992. https://doi.org/10.1007/BF01205234
J. Pitman, Random discrete distributions invariant under size-biased permutation, Adv. Appl. Probab. 28:525–539, 1996. https://doi.org/10.2307/1428070
K. Dickman, On the frequency of numbers containing prime factors of a certain relative magnitude, Arkiv för Matematik, Astronomi och Fysik 22:1–14, 1930.
S. Engen, Stochastic Abundance Models, Chapman and Hall, 1978.
J. W. McCloskey, A model for the distribution of individuals by species in an environment, PhD thesis, Michigan State University, 1965.
A. M. Vershik, The asymptotic distribution of factorizations of natural numbers into prime divisors, Soviet Math. Dokl. 34:57–61, 1986.

13 thms2 active usersReviewed

Completed

Captain: mikedeng1

Large Deviations of Sums of Independent Random Variables 3: For Centered Summands and x ≥ 2B_n, P(S_n ≥ x) ≥ ½ΣP(X_j ≥ 2x)Research Paper

Motivation

The probability that a sum of independent random variables exceeds a large level is a central quantity in large deviation theory. It appears, for example, when relating tail assumptions on individual summands to the tail of their sum. For summands with light (exponentially decaying) tails, exponential bounds are often effective. For heavier tails, a large value of the sum can instead be produced by one large summand. Nagaev's survey studies bounds that make the contribution of such summands explicit.

S. V. Nagaev's survey Large deviations of sums of independent random variables, Ann. Probab. 7 (1979) collects upper bounds of this type. Its best-known result, the Fuk–Nagaev inequality (Theorem 1.3, p. 749), bounds $P(S_n\ge x)$ from above by $\sum_i P(X_i>y_i)$ plus an explicit term built from truncated moments. Upper bounds alone do not show that the one-summand term is necessary. At the end of §1 (pp. 758–759) the paper gives a complementary lower bound that needs neither identical distributions nor regular variation of the tails, only centred summands with finite variances. This mission formalizes that lower bound and the steps of its proof.

Timeline. Fuk and Nagaev (1971) proved truncation inequalities of this kind; the survey refers to that paper for the proofs of its Theorems 1.1 and 1.2 (p. 752). A. V. Nagaev (1969) obtained the asymptotics of Theorem 1.9 (p. 753) for identically distributed, centred summands with tails $1-F(x)=l(x)x^{-t}(1+o(1))$ , $t>2$ , $l$ slowly varying; in the range where one summand dominates, the survey's own argument gives $P(S_n\ge x_n)=nP(X_1\ge x_n)(1+o(1))$ , display (1.46), p. 756. The lower bound treated here (1979, p. 759) drops both the identical-distribution and the regular-variation hypotheses in exchange for explicit constants ( $\tfrac12$ , and $2x$ in place of $x$ ).

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1,\dots,X_n$ independent real random variables on it. The paper writes

S_n=\sum_{i=1}^n X_i,\qquad \sigma_i^2=\operatorname{Var}X_i,\qquad B_n^2=\sum_{i=1}^n\sigma_i^2,\qquad B_n=(B_n^2)^{1/2}.

Throughout, $x>0$ is the level (p. 747). For an index $j$ , the sum without the $j$ -th summand is

S_n^j=\sum_{i\ne j}X_i=S_n-X_j ,

and the one-big-summand probability is

P_j=P\Big(S_n\ge x,\ X_j\ge x,\ \max_{i\ne j}X_i<x\Big),

the probability that the sum reaches $x$ while $X_j$ is the only summand that does.

In the Lean development these are S n X, Sj n X j, Bn2 P X and Pj P X x j, in the namespace NagaevLD.LowerBound.

Formalization targets

Goal: the lower bound (p. 759, after (1.58))

Assume $EX_i=0$ for every $i$ and $B_n^2<\infty$ . Then for $x\ge 2B_n$

P(S_n\ge x)\ \ge\ \frac12\sum_{j=1}^n P(X_j\ge 2x).

Milestones (in the paper's order)

(1.57), p. 758: $\displaystyle P(S_n\ge x)\ge\sum_{j=1}^n P_j$ .
The bound on $P_j$ , p. 758: $P_j\ge P(X_j\ge 2x)\,P\big(S_n^j\ge -x,\ \max_{i\ne j}X_i<x\big)$ .
"It is clear that", p. 759: $P\big(S_n^j\ge -x,\ \max_{i\ne j}X_i<x\big)\ge P(S_n^j\ge -x)-P\big(\max_{i\ne j}X_i\ge x\big)$ .
First Chebyshev bound, p. 759: $P(S_n^j\ge -x)\ge 1-B_n^2/x^2$ .
Second Chebyshev bound, p. 759: $P\big(\max_{i\ne j}X_i\ge x\big)\le B_n^2/x^2$ .
(1.58), p. 759: $P_j\ge\tfrac12P(X_j\ge 2x)$ if $x\ge 2B_n$ .

Significance

The result. Set beside the Fuk–Nagaev upper bound, the lower bound shows that in the range $x\ge 2B_n$ the probability $P(S_n\ge x)$ is at least a fixed fraction of a one-summand term, $\tfrac12\sum_jP(X_j\ge 2x)$ , for any centred summands with finite variances. It is valid for every $n$ and every family of independent, centred, square-integrable summands, with no asymptotic regime and no tail regularity. It is a non-asymptotic counterpart of the asymptotics $P(S_n\ge x)\sim nP(X_1\ge x)$ for regularly varying tails, and it indicates that the term $\sum_iP(X_i>y_i)$ in upper bounds of Fuk–Nagaev type cannot be removed.

Formalizing it. The result is proved in the 1979 paper; the local Prove2Me catalogue search found no exact formal statement of this bound. A formal proof would produce a reusable lower bound for tails of sums of independent variables and the decomposition (1.57) into one-big-summand events, which applies to any family of real random variables.

Difficulty

The individual steps are short. The step that needs care is the bound on $P_j$ : it requires the event $\{X_j\ge 2x\}$ to be independent of the event $\{S_n^j\ge -x,\ \max_{i\ne j}X_i<x\}$ , which is generated by the other $n-1$ summands. Deriving this from mutual independence of $X_1,\dots,X_n$ means grouping the summands into $\{j\}$ and its complement and passing to a function of the complementary block. The first Chebyshev bound similarly needs the variance of $S_n^j$ to equal $\sum_{i\ne j}\sigma_i^2$ , again by independence of a sub-family. A naive union bound $P(S_n\ge x)\ge P(X_j\ge 2x)-\dots$ for one $j$ alone does not give the sum over $j$ : the decomposition into the disjoint events of (1.57) is what makes the sum appear.

Formalization scope

Representation. The summands are a family X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); the paper's $X_1,\dots,X_n$ are X 0, …, X (n-1). Probabilities are P.real of sets, with $\ge$ , $>$ and $<$ exactly as printed.
$B_n^2<\infty$ . The page's hypothesis is stated as square integrability of every summand (MemLp (X i) 2 P). Mathlib's variance returns $0$ for a variable that is not square integrable, so without this hypothesis $B_n^2$ could be $0$ while the summands have infinite variance, and the goal would be false. $EX_i=0$ is stated as $\int X_i\,dP=0$ .
The maximum over $i\ne j$ . $\max_{i\ne j}X_i<x$ is written " $X_i<x$ for every $i\ne j$ " and $\max_{i\ne j}X_i\ge x$ as "some $i\ne j$ has $X_i\ge x$ ", so the case $n=1$ , where the maximum is over the empty set, needs no convention.
Printed slips. In the "It is clear that" step the page writes $\max_{i\ne j}X_i\le x$ and $>x$ , while (1.57) uses $<x$ . Milestones 3 and 5 are stated with $<x$ and $\ge x$ , the form the argument uses; milestone 5 with $\ge x$ is stronger than the printed $>x$ .
Minimal hypotheses. (1.57) and milestone 3 hold for any measurable family and are stated without independence or moments. The other statements carry the paper's standing assumptions (independence, $x>0$ ) and the hypotheses $EX_i=0$ , $B_n^2<\infty$ of the page.
No trivialization. The hypotheses are satisfiable by every i.i.d. family with a centred square-integrable law, for instance Rademacher signs, so the goal is not vacuous; and $B_n$ is the square root of the true sum of variances, not a free parameter.
Welcome contributions. Lemmas on independence of a single summand from a function of the remaining ones, and on the variance of a sub-sum of independent variables, are reusable beyond this mission.

Selected references

S. V. Nagaev, Large deviations of sums of independent random variables, Annals of Probability 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 of Probability and Its Applications 16(4), 643–660, 1971. https://doi.org/10.1137/1116071
A. V. Nagaev, Limit theorems for large deviations where Cramér's conditions are violated (in Russian), Izv. Akad. Nauk UzSSR Ser. Fiz.-Mat. Nauk 6, 17–22, 1969 (reference [27] of the survey; no DOI).

9 thms2 active usersReviewed

Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 3: Moments E_{α,θ}(V_n^p) of the n-th Largest PD(α, θ) Frequency as One Integral of φ_α and ψ_αResearch Paper

Motivation

Random discrete distributions — a random sequence of nonnegative frequencies $V_1\ge V_2\ge\dots$ summing to one — model the relative sizes of species in a population, of cycles in a random permutation, of excursion intervals of a Markov process, and of clusters in Bayesian nonparametric models. The two-parameter Poisson–Dirichlet law $\mathrm{PD}(\alpha,\theta)$ is the family that contains Kingman's one-parameter law $\mathrm{PD}(0,\theta)$ (Ewens sampling, random permutations) and the law $\mathrm{PD}(\alpha,0)$ of ranked excursion lengths of a stable subordinator. J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), developed its distribution theory systematically. In Bayesian nonparametrics the same family appears as the Pitman–Yor process prior.

A basic quantitative question about any random discrete distribution is the size of its $n$ -th largest atom. This mission formalizes the paper's answer for $\mathrm{PD}(\alpha,\theta)$ : every moment $E(V_n^p)$ as one explicit integral.

Timeline. The moment formula for $\mathrm{PD}(0,\theta)$ (Corollary 18 below) was known before 1997 (references [63, 73, 25, 50] of the paper). The Laplace transform of $1/V_n$ under $\mathrm{PD}(\alpha,0)$ was obtained, in different settings, by Darling (1952) and Lamperti (1961) for $n=1$ and by Wendel (1964) for $n=2,3,\dots$ . Perman, Pitman and Yor (1992) proved that $\mathrm{PD}(\alpha,\theta)$ has density a constant times $L^{\theta/\alpha}$ relative to $\mathrm{PD}(\alpha,0)$ . Pitman and Yor (1997) combined these into Proposition 17.

Setting

Fix $0\le\alpha<1$ and $\theta>-\alpha$ . Let $\tilde Y_1,\tilde Y_2,\dots$ be independent with $\tilde Y_n\sim\mathrm{beta}(1-\alpha,\theta+n\alpha)$ , the law with density $\frac{\Gamma(a+b)}{\Gamma(a)\Gamma(b)}x^{a-1}(1-x)^{b-1}$ on $(0,1)$ . Break a unit stick:

\tilde V_1=\tilde Y_1,\qquad \tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n\quad(n\ge2),

and let $V_1\ge V_2\ge\dots$ be the ranked values of the $\tilde V_n$ . The law of $(V_n)$ is $\mathrm{PD}(\alpha,\theta)$ (Definition 1); $E_{\alpha,\theta}$ denotes expectation under it.

For $0<\alpha<1$ and $\lambda\ge0$ the paper introduces

\phi_\alpha(\lambda)=\alpha\int_1^\infty e^{-\lambda x}x^{-\alpha-1}\,dx,\qquad \psi_\alpha(\lambda)=1+\alpha\int_0^1(1-e^{-\lambda x})x^{-\alpha-1}\,dx .

Under $\mathrm{PD}(\alpha,0)$ the local time $L=\lim_{n\to\infty}nV_n^\alpha$ exists almost surely. From $(V_n)$ one derives $R_n=V_{n+1}/V_n$ , $A_n=(V_1+\dots+V_n)/V_{n+1}$ (with $A_0=0$ ) and $X_n=LV_n^{-\alpha}$ . Finally

C_{\alpha,\theta}=\frac{\Gamma(\theta+1)}{\Gamma(\theta/\alpha+1)}\Gamma(1-\alpha)^{\theta/\alpha}.

The Lean declarations Xseq, pdConst, and expIntE are in PoissonDirichlet.Moments; the other objects come from the frozen shared PoissonDirichlet.Ratio and PoissonDirichlet.Wendel modules.

Formalization targets

Goal: Proposition 17

For $0<\alpha<1$ , $\theta>-\alpha$ , $p>0$ with $\theta+p>0$ , and $n=1,2,\dots$ ,

E_{\alpha,\theta}(V_n^p)=\frac{\Gamma(1-\alpha)^{\theta/\alpha}}{\Gamma(n)}\frac{\Gamma(\theta+1)}{\Gamma(\theta+p)}\frac{\Gamma(\theta/\alpha+n)}{\Gamma(\theta/\alpha+1)}\int_0^\infty t^{p+\theta-1}e^{-t}\phi_\alpha(t)^{n-1}\psi_\alpha(t)^{-\theta/\alpha-n}\,dt .

Milestones, in attack order

(86): for $X>0$ a.s. and $p>0$ , $E[X^{-p}]=\frac1{\Gamma(p)}\int_0^\infty t^{p-1}E[e^{-tX}]\,dt$ .
Proposition 26: under $\mathrm{PD}(\alpha,0)$ , $E[\exp(-\lambda/V_n)\mid R_1,\dots,R_{n-1},X_n]=\exp(-\lambda(1+A_{n-1}))\exp[-X_n(\psi_\alpha(\lambda)-1)]$ .
(36): under $\mathrm{PD}(\alpha,0)$ , $E[\exp(-\lambda A_{n-1})]=\phi_\alpha(\lambda)^{n-1}$ .
Under $\mathrm{PD}(\alpha,0)$ , $X_n$ is $\mathrm{gamma}(n)$ and independent of $A_{n-1}$ .
Lemma 27: under $\mathrm{PD}(\alpha,0)$ , for $\ell>-1$ , $p>0$ , $p+\ell\alpha>0$ ,

E[L^\ell V_n^p]=\frac{\Gamma(\ell+n)}{\Gamma(n)\Gamma(p+\ell\alpha)}\int_0^\infty t^{p+\ell\alpha-1}e^{-t}\phi_\alpha(t)^{n-1}\psi_\alpha(t)^{-\ell-n}\,dt .

Proposition 14: $E_{\alpha,\theta}[f(V)]=C_{\alpha,\theta}E_{\alpha,0}[L^{\theta/\alpha}f(V)]$ for nonnegative measurable $f$ , and $C_{\alpha,\theta}=1/E_{\alpha,0}(L^{\theta/\alpha})$ .

Two consequences close the list: (50), $n^{p/\alpha}E_{\alpha,\theta}(V_n^p)\to C_{\alpha,\theta}/C_{\alpha,\theta+p}$ , and Corollary 18, the $\mathrm{PD}(0,\theta)$ formula

E_{0,\theta}(V_n^p)=\frac{\Gamma(\theta)}{\Gamma(\theta+p)}\frac{\theta^n}{\Gamma(n)}\int_0^\infty t^{p-1}e^{-t}E(t)^{n-1}e^{-\theta E(t)}\,dt,\qquad E(t)=\int_t^\infty x^{-1}e^{-x}dx .

Significance

The ranked frequencies of $\mathrm{PD}(\alpha,\theta)$ have no tractable joint density; their one-dimensional laws are known only through transforms. Proposition 17 makes every moment of $V_n$ computable by a single quadrature, for all parameters at once. It yields the large- $n$ decay (50), $V_n\approx(L/n)^{1/\alpha}$ in mean, and recovers the classical $\mathrm{PD}(0,\theta)$ formula in the limit $\alpha\downarrow0$ . The intermediate statements, the conditional Wendel formula and the joint moments $E[L^\ell V_n^p]$ , are used elsewhere in the paper (Proposition 16, Lemma 29).

All statements are proved in the 1997 paper, except Proposition 14, which the paper quotes from Perman, Pitman and Yor (1992). To our knowledge none of them has been machine-checked. A formal development would produce the first verified construction of the Poisson–Dirichlet family in Lean, together with reusable facts about stick-breaking with beta variables, ranked rearrangements of sequences, and the Laplace-transform representation of negative moments.

Difficulty

The identity (86) and the final integration are elementary. The difficulty lies upstream. The naive route, computing $E(V_n^p)$ from the stick-breaking definition, fails: $V_n$ is the $n$ -th ranked value of the $\tilde V_k$ , and ranking destroys the product structure of the beta variables. The paper instead works under $\mathrm{PD}(\alpha,0)$ , where the ranked sequence is the normalized sequence of points of a Poisson random measure (equivalently, transformed arrival times of a unit Poisson process). Proposition 14 is itself a deep change-of-measure result about stable subordinators, and the existence of the local time $L$ is an almost sure limit theorem. Neither has any counterpart in Mathlib.

Formalization scope

Sequences are indexed from $0$ in Lean: the paper's $V_n$ is V ω (n-1), and statements "for $n=1,2,\dots$ " quantify over k : ℕ with $n=k+1$ . $\mathrm{PD}(\alpha,\theta)$ is defined exactly as Definition 1, with independent beta coordinates (Mathlib's betaMeasure) and the ranked values defined with Set.encard. The law is stated through preimages, so no measurability of the ranking map is presupposed. The local time $L$ is carried as a random variable together with its defining almost sure limit (24). Expectations of quantities that may be infinite are lower integrals. The conditional expectation of Proposition 26 is stated through its defining property, for every nonnegative measurable test function of $(R_1,\dots,R_{n-1},X_n)$ . The parameter ranges $0<\alpha<1$ , $\theta>-\alpha$ (and $\theta>0$ at $\alpha=0$ ) are hypotheses wherever the page has them. Two hypotheses are added and disclosed: $\theta+p>0$ in Proposition 17 and $p+\ell\alpha>0$ in Lemma 27. Without them the printed $t$ -integrals diverge and $\Gamma$ is evaluated at a pole or a negative argument, while the left sides are finite. Both follow from the printed hypotheses when $\theta\ge0$ (resp. $\ell\ge0$ ).

Trivializing encodings are ruled out: no law is written as an image measure of a possibly non-measurable map, no count uses Set.ncard, no limit uses limUnder, $C_{\alpha,\theta}$ is not defined as $1/E(L^{\theta/\alpha})$ , and every Bochner integral in a statement is of an integrable function under the stated hypotheses, so no statement holds because of a junk value $0$ .

A complete development needs: infinite products of beta laws, the ranked rearrangement and its measurability, the Poisson-process representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10), and the change of measure of Proposition 14. These are reusable beyond this mission. Proofs of the general identity (86), of the gamma–independence milestone, and of Lemma 27 from its milestones are welcome independently.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992. https://doi.org/10.1007/BF01205234
J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964. https://doi.org/10.7146/math.scand.a-10703
J. F. C. Kingman, Random discrete distributions, J. Roy. Statist. Soc. Ser. B 37:1–22, 1975. https://doi.org/10.1111/j.2517-6161.1975.tb01024.x

10 thms2 active usersReviewed

Analysis Operations Research Stochastic Systems·Captain: mikedeng1

Implicit Renewal Theory and Tails of Solutions of Random Equations 3: Rate of Approach — t^κP(R > t) Equals C₊ Minus a Contour Integral Plus O(t^{−β/2})Research Paper

Motivation

Random equations of the form $R \overset{\mathcal L}{=} \Psi(R)$ , with $\Psi$ a random function independent of $R$ , describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations $R = Q + MR$ , and the stationary workload of certain queueing and storage models. When $\Psi(t)$ acts like multiplication by a random variable $M$ for large $|t|$ , and $\mathbf E|M|^\kappa = 1$ for some $\kappa > 0$ , the solution has power-law tails: $P(R > t) \sim C_+ t^{-\kappa}$ . This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.

A tail asymptotic alone says nothing about how fast $t^\kappa P(R > t)$ approaches $C_+$ . For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of $1 - \hat\eta$ , where $\eta$ is a tilted law of $\log M$ , plus a remainder $O(t^{-\beta/2})$ .

Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.

Setting

Let $(\Omega, \mathcal A, P)$ be a probability space carrying independent real random variables $M \ge 0$ and $R$ . Fix $\kappa > 0$ with $\mathbf E M^\kappa = 1$ (the Cramér condition, (2.3)) and $\beta > 0$ with $\mathbf E M^{\kappa+\beta} < \infty$ (3.3).

The tilted law of $M$ is the probability measure $\eta(dx) = e^{\kappa x} P(\log M \in dx)$ on $\mathbb R$ , computed on $\{M > 0\}$ . Its transforms are $\tilde\eta(\beta) = \int e^{\beta t}\eta(dt)$ for real $\beta$ and $\hat\eta(\theta) = \int e^{i\theta t}\eta(dt)$ for complex $\theta$ ; for a function $f$ , $\hat f(\theta) = \int e^{i\theta t} f(t)\,dt$ . Convolution powers are $\eta^{(0)} = \delta_0$ , $\eta^{(n+1)} = \eta^{(n)} * \eta$ , and the renewal measure is $\nu = \sum_{n \ge 0}\eta^{(n)}$ . A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of $\log M$ given $M \ne 0$ .

Set $m = \mathbf E M^\kappa \log M$ and

g_1(t) = e^{\kappa t}\big(P(R > e^t) - P(MR > e^t)\big), \qquad C_+ = \frac1m\int_0^\infty \big(P(R > t) - P(MR > t)\big) t^{\kappa - 1}\,dt,

with $g_{-1}$ and $C_-$ defined the same way for the lower tail. The strip is $D = \{\theta : -\beta < \Im\theta < 0\}$ , and $\mathscr C$ denotes a positively oriented closed contour in $D$ enclosing every zero of $1 - \hat\eta$ in $D$ .

Formalization targets

Goal: Theorem 3.2

If, in addition, $\eta^{(n_0)} = (1 - \delta)\varphi_0 + \delta\varphi_1$ for some $n_0$ , with $\delta \in [0, 1)$ , $\varphi_0$ absolutely continuous and $\delta\tilde\varphi_1(\beta) < 1$ , and $\hat\eta \ne 1$ on $\Im\theta = -\beta$ , then $\int_0^\infty |P(R > t) - P(MR > t)|\,t^{\kappa+\beta-1}dt < \infty$ implies

t^\kappa P(R > t) = C_+ - \frac1{2\pi}\,\Re\oint_{\mathscr C} e^{-i\theta\log t}\,\frac{\hat g_1(\theta)}{1 - \hat\eta(\theta)}\,d\theta + O(t^{-\beta/2}), \qquad t \to \infty,

with the analogous statement for $P(R < -t)$ ; and if $R \overset{\mathcal L}{=} \Psi(R)$ with $R$ independent of $(M, \Psi)$ , the integrability hypotheses may be replaced by $\mathbf E|(\Psi(R)^\pm)^{\kappa+\beta} - ((MR)^\pm)^{\kappa+\beta}| < \infty$ . The theorem also asserts that $\eta$ is a spread-out probability measure.

Milestones

Lemma 9.5: Stone's inversion formula for the density of $\sum_n \chi * \mu^{(n)}$ .
Theorem 3.1: the renewal measure splits as $\nu = \nu_0 + \nu_1$ , $\nu_1$ finite with $\tilde\nu_1(\beta) < \infty$ , $\nu_0$ with continuous bounded density

p(t) = \frac1m - \frac1{2\pi}\oint_{\mathscr C} e^{-i\theta t}\frac{d\theta}{1 - \hat\eta(\theta)} + o(e^{-\beta t}).

(9.23) and (9.24): the smoothed identity and the smoothed rate $K * \Re r_1(t) = o(e^{-\beta t})$ for the kernel $K(t) = be^{-bt}\mathbf 1_{t>0}$ .
Theorem 9.6: the Beurling–Ganelius Tauberian remainder theorem.

Significance

Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form $(\log t)^{j-1}t^{\Im\theta_l}$ times oscillating factors, one family for each zero $\theta_l$ of $1 - \hat\eta$ with $0 < -\Im\theta_l \le \beta/2$ , and their form does not depend on the unknown law of $R$ . It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.

The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.

Difficulty

The first-order theorem follows from the key renewal theorem applied to $r(t) = e^{\kappa t}P(R > e^t)$ . That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields $e^{\beta t}g_1 \in L^1$ but not $e^{\beta t}g_1(t) = o(1)$ , so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of $r$ , where Stone's decomposition with the contour expansion of the renewal density gives an $o(e^{-\beta t})$ remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for $r$ and for the contour term, and costs half the exponent. The contour expansion itself requires showing that $1 - \hat\eta$ has finitely many zeros in the strip and handling their orders through residues.

Formalization scope

All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps $\Omega \to \mathbb R$ on a probability space; $M \ge 0$ almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as $\mathbf E M^{\kappa+\beta}$ and $\tilde\mu(\beta)$ are lower Lebesgue integrals in $[0, \infty]$ . The transforms $\hat\mu$ and $\hat f$ are Bochner integrals at complex arguments with the $+i$ sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.

The contour. A contour $\mathscr C$ is the positively oriented boundary of an axis-parallel rectangle whose closure lies in $D$ and whose interior contains every zero of $1 - \hat\eta$ in $D$ ; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.

The variable in (3.8) and (3.10). The paper prints $e^{-i\theta t}$ in the contour term, but its proof establishes the expansion in the logarithmic variable $s = \log t$ . The targets are stated with $e^{-i\theta\log t}$ , which is what the proof gives. With the printed $e^{-i\theta t}$ the contour term would decay exponentially and the statement would claim $t^\kappa P(R > t) = C_+ + O(t^{-\beta/2})$ , which is not what is proved. Hypothesis (3.7) is printed with $P(R > -t)$ and is read with $P(R > t)$ .

Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of $1 - \hat\eta$ in $D$ ; and the contour must enclose all zeros in the strip, not a chosen subset.

Theorem 9.6 is stated for a complex-valued kernel and a finite strip width $a$ ; the application with $a = \infty$ follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of $\chi$ has compact support, which the proof uses and the application provides.

Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.

Selected references

C. M. Goldie, Implicit renewal theory and tails of solutions of random equations, Ann. Appl. Probab. 1(1):126–166, 1991. https://doi.org/10.1214/aoap/1177005985
H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Math. 131:207–248, 1973. https://doi.org/10.1007/BF02392040
C. Stone, On absolutely continuous components and renewal theory, Ann. Math. Statist. 37(1):271–275, 1966. https://doi.org/10.1214/aoms/1177699617
T. H. Ganelius, The remainder in Wiener's Tauberian theorem, Acta Univ. Gothoburgensis, Mathematica Gothoburgensia 1, 1962 (cited in Goldie 1991).
A. K. Grincevičius, One limit distribution for a random walk on the line, Lithuanian Math. J. 15:580–589, 1975 (cited in Goldie 1991).

12 thms2 active usersReviewed

Control Theory Stochastic Systems·Captain: mikedeng1

Backward-Forward Stochastic Differential Equations 3: A Linear Backward-Forward System with Lipschitz Constant 1 Has No Solution on a Horizon T ≥ 1Research Paper

Motivation

A forward equation evolves from an initial random value, while a backward equation is constrained by a terminal random value. When the two unknown processes appear in both equations, these boundary conditions can be incompatible. Such coupled systems occur in stochastic control, where a state moves forward and a cost or adjoint variable is determined backward. Antonelli's 1993 paper studies existence and uniqueness for a class of backward–forward stochastic differential equations and gives explicit examples showing why its smallness assumption on the coefficients cannot be discarded (Antonelli 1993, §§1 and 3).

This mission formalizes the first of those examples. It is a deliberately small two-equation system: both integrators are ordinary time, the coefficients are deterministic, and the Lipschitz constant is one. Nevertheless, the system has no solution when the time horizon reaches one. The claim identifies a genuine boundary for the paper's existence result rather than a failure caused by exotic stochastic integration. Antonelli presents it immediately after the existence theorem to show what can go wrong beyond the theorem's coefficient bound (Antonelli 1993, Theorem 3.1 and Example 1).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ and a filtration $(\mathcal F_t)_{t\ge0}$ . The filtration satisfies the usual hypotheses: it is right-continuous, and $\mathcal F_0$ contains every subset of every $P$ -null set. Let $T>0$ be a deterministic horizon. The initial random variable $J_0$ is $\mathcal F_0$ -measurable, and the terminal random variable $Y$ is $\mathcal F_T$ -measurable. Both are integrable and strictly positive almost surely. These choices specialize the filtered space and input assumptions of §3 to Example 1 (Antonelli 1993, pp. 777, 785, 790).

The unknowns are two real-valued stochastic processes $U=(U_t)$ and $V=(V_t)$ . Their norm is

\|X\|_{L^1(dt\otimes P)}=E_P\!\left[\int_0^T |X_t|\,dt\right].

Thus a solution is a pair in $L^1(dt\otimes P)^2$ of adapted processes satisfying a forward integral equation and a backward conditional-expectation equation almost surely at each time $t\le T$ . Under the usual hypotheses every $L^1$ -class solution has such a representative, so this is the paper's $L^1(\mu)\otimes L^1(\mu)$ solution class. The system uses $A_t=C_t=t$ and the constant input process $J_t=J_0$ . In this specialization, the measure $\mu$ used in the paper is $dt\otimes P$ , and the variation control process is $D_t=t$ (Antonelli 1993, (3.1)–(3.3), pp. 785–786).

The forward coefficient is $f(u,v)=u+|v|$ and the backward coefficient is $g(u,v)=u+v$ . Each has Lipschitz constant one with respect to $|u-u'|+|v-v'|$ . The absolute value is part of the example: it appears in the forward equation and does not appear in the backward equation (Antonelli 1993, (3.6)–(3.7), p. 790).

Formalization targets

Main goal

For every horizon $T\ge1$ and all data satisfying the assumptions above, there is no pair $(U,V)\in L^1(dt\otimes P)^2$ satisfying

U_t=J_0+\int_0^t(U_s+|V_s|)\,ds,\qquad V_t=E_P\!\left[\int_t^T(U_s+V_s)\,ds+Y\mid\mathcal F_t\right].

This is Example 1's conclusion, including the boundary case $T=1$ (Antonelli 1993, pp. 790–791).

Intermediate targets

The milestones follow the four statements written in the example: representations of $U$ and $V$ in terms of each other, positivity and passage to the linear system (3.8)–(3.9), the martingale identity for their sum, and the identity $\beta(1-T)=E_P[J_0+Y]>0$ for its constant mean $\beta$ . Their full text and page provenance are attached to the milestone list. The goal remains nonexistence for every $T\ge1$ ; it does not assert a particular formula for a solution.

Significance

The preceding existence theorem assumes a coefficient bound that becomes $kT<1$ in this time-integrator case. Example 1 has $k=1$ and shows that the system can fail to have a solution as soon as that strict inequality fails. At $T=1$ , the obstruction is already present, so replacing $T\ge1$ by $T>1$ would lose part of the paper's conclusion (Antonelli 1993, p. 791).

A formalization would make the failure precise for the same $L^1$ solution class used by the paper. The current mission contains compile-checked Lean statements and definitions; the theorem proofs are still open. A complete development would also provide reusable statements about jointly measurable conditional-expectation versions, finite-horizon time integrals of processes, and martingales arising from coupled equations. These can support the paper's neighboring existence and nonsingular-example missions.

Difficulty

The main difficulty is the coupling between the two boundary conditions. The forward equation starts at $J_0$ , while the backward equation ends at $Y$ ; neither equation can be treated as an independent ordinary differential equation. The absolute value in the forward coefficient also prevents the coupled system from being treated as a linear system at the outset. A second difficulty for Lean is that conditional expectation is defined only up to almost-sure equality at each fixed time, whereas the solution equations are equalities over time and probability together. The formal statement must connect these two kinds of almost-everywhere equality without strengthening the theorem to an identity at every time on every sample path.

Formalization scope

Time is represented by $\mathbb R_{\ge0}$ , with only $(0,T]$ used in the $L^1$ norm. Time integration is Lebesgue integration on $(s,t]$ ; endpoints have zero $dt$ mass. The norm is an extended nonnegative lintegral, so a nonintegrable process cannot be assigned the value zero by a real-valued integral's fallback convention. The random variable inside each conditional expectation is required to be integrable. The conditional-expectation process is a jointly measurable version whose value at each time agrees almost surely with the conditional expectation. The solution predicate asks, for each $t\le T$ , that $U_t$ and $V_t$ be $\mathcal F_t$ -measurable, that the two equations hold $P$ -almost surely, and that the time integrands be integrable along almost every path. Any $L^1$ -class solution can be replaced by such a representative, $J_0+\int_0^t f(U_s,V_s)\,ds$ and the conditional-expectation version, so non-existence in this class is non-existence in the paper's class. For the Lipschitz coefficients in this example, finite $L^1(dt\otimes P)$ norm gives pathwise integrability almost surely for the time integrals used in the equations.

The paper calls $J_0$ and $Y$ “positive.” Here that means strictly positive almost surely. The weaker nonnegative reading would admit the zero pair when both data are zero and would falsify the target. Integrability of $J_0$ makes explicit §3's standing bound on the constant input process. The completeness and right-continuity of the filtration are also explicit. The solution class and equations are defined for general $T>0$ ; the restriction $T\ge1$ belongs only to the nonexistence theorem. For example, on a one-point probability space with $T=1/2$ , $J_0=Y=1$ , the deterministic pair $U_t=1+4t$ , $V_t=3-4t$ solves the equations on $[0,1/2]$ . This rules out a definition that makes all solutions impossible by construction.

The development needs Mathlib's filtration, conditional expectation, probability measure, and integration APIs. Contributions proving the milestone statements or supplying reusable lemmas for their $L^1$ and martingale interfaces fit the mission. No semimartingale stochastic integral is required for this example.

Selected references

F. Antonelli, Backward-forward stochastic differential equations, Annals of Applied Probability 3(3), 777–793, 1993. DOI: 10.1214/aoap/1177005363.

8 thms2 active usersReviewed

Control Theory Operations Research Stochastic Systems·Captain: mikedeng1

Reflected Solutions of Backward SDE's, and Related Obstacle Problems for PDE's 2: With a Concave Coefficient, the Reflected BSDE Is the Value of a Minimax Optimal Stopping–Control ProblemResearch Paper

Motivation

A backward stochastic differential equation (BSDE) prescribes the terminal value of an adapted process instead of its initial value. Pardoux and Peng (1990) proved existence and uniqueness for Lipschitz coefficients, and BSDEs have since become a standard tool in stochastic control, mathematical finance and the probabilistic treatment of semilinear PDEs. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE, whose solution is constrained to stay above a given obstacle process. Reflected BSDEs describe the price of American options in nonlinear markets (El Karoui, Pardoux and Quenez 1997), Dynkin games (Cvitanić and Karatzas 1996), and obstacle problems for parabolic PDEs.

In §7 of the 1997 paper the coefficient is assumed concave. Then the solution of the reflected BSDE is the value of a game: one player chooses a stopping time, the other chooses a control that sets the discount rate and the change of measure, and the value does not depend on which player moves first. This mission formalizes that statement (Theorem 7.2) and the results its proof uses.

Setting

Let $(\Omega,\mathcal F,P)$ carry a $d$ -dimensional standard Brownian motion $B$ , fix a horizon $T\ge0$ , and let $\mathcal F_t$ be the natural filtration of $B$ augmented by the $P$ -null sets. Write $\mathbb L^2$ for the square-integrable $\mathcal F_T$ -measurable random variables, $\mathbb H^2$ for the progressively measurable processes $\varphi$ with $E\int_0^T|\varphi_t|^2dt<\infty$ , and $\mathcal S^2$ for those with $E\sup_{t\le T}|\varphi_t|^2<\infty$ .

The data are a terminal value $\xi\in\mathbb L^2$ ; a coefficient $f(\omega,t,y,z)$ , $y\in\mathbb R$ , $z\in\mathbb R^d$ , with $f(\cdot,y,z)\in\mathbb H^2$ for every $(y,z)$ and Lipschitz in $(y,z)$ with a constant $K$ ; and a continuous progressively measurable obstacle $S$ with $E\sup_t(S_t^+)^2<\infty$ and $S_T\le\xi$ . A solution of the reflected BSDE is a triple $(Y,Z,K)$ of progressively measurable processes with $Z\in\mathbb H^2$ , $Y\in\mathcal S^2$ , $K_T\in\mathbb L^2$ , and

Y_t=\xi+\int_t^Tf(s,Y_s,Z_s)\,ds+K_T-K_t-\int_t^T(Z_s,dB_s),\qquad Y_t\ge S_t,

where $K$ is continuous, nondecreasing, $K_0=0$ and $\int_0^T(Y_t-S_t)\,dK_t=0$ : $K$ pushes $Y$ up only when $Y$ touches $S$ .

For $t\le T$ , $\mathcal T_t$ is the set of stopping times $v$ with $t\le v\le T$ . When $f(\omega,t,\cdot,\cdot)$ is concave, its conjugate is

F(\omega,t,\beta,\gamma)=\sup_{(y,z)}\big[f(\omega,t,y,z)-\beta y-\langle\gamma,z\rangle\big]\in(-\infty,+\infty].

The admissible controls $\mathcal A$ are the bounded progressively measurable $(\beta_t,\gamma_t)$ with $E\int_0^TF(t,\beta_t,\gamma_t)^2dt<\infty$ . Each $(\beta,\gamma)\in\mathcal A$ gives the affine coefficient $f^{\beta,\gamma}(t,y,z)=F(t,\beta_t,\gamma_t)+\beta_ty+\langle\gamma_t,z\rangle$ , its reflected BSDE solution $Y^{\beta,\gamma}$ , the process $\Gamma^{\beta,\gamma}_{t,s}$ solving $d\Gamma_{t,s}=\Gamma_{t,s}(\beta_sds+(\gamma_s,dB_s))$ , $\Gamma_{t,t}=1$ , and the payoff

\Phi(t,v,\beta,\gamma)=\Gamma^{\beta,\gamma}_{t,v}\big[S_v1_{\{v<T\}}+\xi1_{\{v=T\}}\big]+\int_t^v\Gamma^{\beta,\gamma}_{t,s}F(s,\beta_s,\gamma_s)\,ds.

Formalization targets

Goal: Theorem 7.2 (p. 725)

For every $t\in[0,T]$ and $(\beta,\gamma)\in\mathcal A$ , $Y^{\beta,\gamma}_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Phi(t,v,\beta,\gamma)\mid\mathcal F_t]$ , and

Y_t=\operatorname*{ess\,inf}_{\mathcal A}Y^{\beta,\gamma}_t=\operatorname*{ess\,inf}_{\mathcal A}\operatorname*{ess\,sup}_{v\in\mathcal T_t}E[\Phi\mid\mathcal F_t]=\operatorname*{ess\,sup}_{v\in\mathcal T_t}\operatorname*{ess\,inf}_{\mathcal A}E[\Phi\mid\mathcal F_t].

The last equality, the interchange of the two essential extrema, is the minimax content.

Milestones

Theorem 4.1 (p. 712): comparison. If $\xi\le\xi'$ , $f\le f'$ and $S\le S'$ , and one of $f,f'$ is Lipschitz, then $Y\le Y'$ .
§7 conjugacy (p. 724): a concave Lipschitz $f$ equals $\min_{(\beta,\gamma)\in D^F_t}\{F(t,\beta,\gamma)+\beta y+\langle\gamma,z\rangle\}$ , the minimum is attained, and the domain $D^F_t$ of $F$ is a.s. bounded.
Proposition 7.1 (p. 724): for an affine coefficient $\delta_t+\beta_ty+\langle\gamma_t,z\rangle$ , $\Gamma_tY_t=\operatorname{ess\,sup}_{v\in\mathcal T_t}E[\Gamma_v\xi1_{\{v=T\}}+\Gamma_vS_v1_{\{v<T\}}+\int_t^v\Gamma_s\delta_sds\mid\mathcal F_t]$ .
§7 optimal control (p. 725): some $(\beta^*,\gamma^*)\in\mathcal A$ satisfies $f(t,Y_t,Z_t)=F(t,\beta^*_t,\gamma^*_t)+\beta^*_tY_t+\langle\gamma^*_t,Z_t\rangle$ $dt\times dP$ -a.e., so $(Y,Z,K)$ solves the reflected BSDE with coefficient $f^{\beta^*,\gamma^*}$ .

Significance

Theorem 7.2 identifies the solution of a nonlinear reflected BSDE with the value of a zero-sum game between a stopper and a controller. In finance, with $f$ the driver of a pricing rule under constraints or ambiguity, it says that the nonlinear price of an American claim is the worst case, over a family of discount rates and changes of measure, of linear American prices; and the stopper may announce the stopping rule first without changing the value. Concave drivers include the hedging equations with different borrowing and lending rates. The representation reduces questions about the nonlinear equation to a family of linear ones, which is how monotonicity, convexity and stability properties of nonlinear American prices are usually derived.

All four results and the goal are proved in the paper, with references to standard convex analysis and a measurable section theorem for two steps. None of them has a machine-checked proof. Mathlib has Brownian motion, filtrations, stopping times and conditional expectation, but no stochastic integral; the mission uses the Itô integral of the published Peng1990.SMP.Stochastic layer. A formal proof would give, beyond the theorem, a reusable comparison theorem for reflected BSDEs, a Snell-envelope representation for linear reflected BSDEs, and a measurable selection of supergradients along a process.

Difficulty

The inequality $Y_t\le Y^{\beta,\gamma}_t$ for each control is a direct consequence of comparison, since $f\le f^{\beta,\gamma}$ . The difficulty is the reverse inequality, which needs a single admissible control that attains the conjugate representation along the solution $(Y,Z)$ for almost every $(t,\omega)$ . Choosing a supergradient pointwise is easy; choosing it progressively measurable, bounded, and with $F(t,\beta^*_t,\gamma^*_t)$ square integrable is a measurable-selection problem. The interchange of ess inf and ess sup does not follow from a general minimax theorem: the family $\mathcal A$ is not compact and the payoff is not convex–concave in any usable topology. It uses a specific stopping time, the first time $Y$ touches $S$ , together with comparison on the random interval before it. Proposition 7.1 requires the linear change of variables $\Gamma_tY_t$ , whose transformed equation lacks the square integrability of the original one, so the Snell-envelope argument has to be rerun with weaker moments.

Formalization scope

Time and spaces. Time is $\mathbb R_{\ge0}$ with $T:\mathbb R_{\ge0}$ , and time integrals run over $[t,T]\subset\mathbb R$ . $\mathbb H^2$ is the published L2F (progressive in place of predictable); $\mathcal S^2$ and the obstacle condition are lower Lebesgue integrals in $[0,\infty]$ .
Filtration. The natural filtration of $B$ joined with the σ-algebra of $P$ -null sets.
Norms. $|z|$ is the Euclidean norm and $\langle\gamma,z\rangle=\sum_j\gamma_jz_j$ .
Lipschitz condition. Read as: almost surely, for all $t\le T$ and all $y,y',z,z'$ .
Solutions. Solutions are in the square-integrable class (v)–(viii). $Y$ has continuous paths. Equation (vi) holds for each $t$ almost surely, and $Y\ge S$ holds almost surely for all $t$ . $K$ is continuous and nondecreasing on every path. $\int_0^T(Y-S)\,dK=0$ is taken against the Lebesgue–Stieltjes measure of the path of $K$ .
Extended values. $F$ takes values in the extended reals. $F^2$ in the definition of $\mathcal A$ is taken in $[0,\infty]$ , so admissibility forces $F<\infty$ almost everywhere along the control.
Stochastic exponential. $\Gamma^{\beta,\gamma}_{t,s}$ is the Doléans-Dade exponential, built from Itô integrals of $\gamma$ with continuous paths.
Essential extrema. They are predicates relative to $\mathcal F_t$ , real valued: the essential infimum is the published MultiperiodRisk.Bellman.EssInf, and the essential supremum is its mirror image.
Added hypothesis. $S\in\mathcal S^2$ is assumed wherever a conditional expectation of the payoff appears (Remark 3.2: without loss of generality). Otherwise the payoff may fail to be integrable, and Lean's conditional expectation of a non-integrable function is $0$ .
Hypothesized families. The solutions $Y^{\beta,\gamma}$ and the Itô integrals defining $\Gamma^{\beta,\gamma}$ are hypotheses indexed by $\mathcal A$ . They exist by the existence theorem of the first mission of this series and by continuity of Itô integrals.

Several formalizations of the goal would make it trivial, and each is ruled out. The conjugate is not a real-valued supremum, which takes a junk value when unbounded. The essential infimum over $\mathcal A$ is not a pointwise infimum. The interchange of ess inf and ess sup is not dropped. The coefficient is a random field $f(\omega,t,y,z)$ , not a deterministic or Markovian one.

The closing gloss of Theorem 7.2, that the triple $(\beta^*,\gamma^*,D_t)$ is optimal, is not stated separately; milestone 4 is its control half. Contributions are welcome on a continuous version of the Itô integral, Itô's formula for products with $\Gamma$ , the Snell envelope in continuous time, and measurable selection of supergradients; all of these are reusable beyond this mission.

Selected references

N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng, M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, Ann. Probab. 25(2), 1997, 702–737. https://doi.org/10.1214/aop/1024404416
É. Pardoux, S. Peng, Adapted solution of a backward stochastic differential equation, Systems Control Lett. 14, 1990, 55–61. https://doi.org/10.1016/0167-6911(90)90082-6
N. El Karoui, S. Peng, M.-C. Quenez, Backward stochastic differential equations in finance, Math. Finance 7(1), 1997, 1–71. https://doi.org/10.1111/1467-9965.00022
J. Cvitanić, I. Karatzas, Backward stochastic differential equations with reflection and Dynkin games, Ann. Probab. 24(4), 1996, 2024–2056. https://doi.org/10.1214/aop/1041903216
S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990, 966–979. https://doi.org/10.1137/0328054

10 thms2 active usersReviewed

Functional Analysis Markov Chain·Captain: mikedeng1

Logarithmic Sobolev Inequalities for Finite Markov Chains 3: Lower Bound α ≥ (1 − 2/q)λ / 2(λt_q + log M_q + (q − 2)/q) from a Bound on ‖H_{t_q}‖_{2→q}Research Paper

Motivation

A finite Markov chain describes a system that changes state according to fixed transition probabilities. For a chain that settles toward an equilibrium distribution, a central question is how quickly the effect of its starting state disappears. The logarithmic Sobolev constant supplies quantitative control of this convergence and, through hypercontractive estimates, also governs how the continuous-time transition operator changes the size of functions measured in different norms. Diaconis and Saloff-Coste's 1996 paper develops these relations for finite chains and uses them to study mixing on graphs and product spaces.

The constant can be hard to calculate directly. Its definition is an infimum over all nonconstant functions, while a particular Markov semigroup may admit an accessible bound from $\ell^2$ to $\ell^q$ at one time. Theorem 3.9 turns such an operator estimate into a numerical lower bound for the log-Sobolev constant. This mission formalizes that result, including both finite $q$ and the supremum-norm endpoint.

Setting

Let $\mathcal X$ be a finite state space. A Markov kernel $K(x,y)$ is nonnegative, with $\sum_yK(x,y)=1$ for every $x$ . A strictly positive stationary distribution $\pi$ satisfies $\sum_x\pi(x)K(x,y)=\pi(y)$ and $\sum_x\pi(x)=1$ . The chain is reversible when $\pi(x)K(x,y)=\pi(y)K(y,x)$ for every pair of states. Its continuous-time heat semigroup is $H_t=e^{-t(I-K)}$ , acting on a function $f$ by $H_tf$ . These conventions follow §§2.1–2.3 of the source paper.

For a real function on $\mathcal X$ , write $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$ when $p$ is finite, and $\|f\|_\infty=\max_x|f(x)|$ . The Dirichlet form is $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$ . The quadratic entropy functional is $\mathcal L(f)=\sum_x|f(x)|^2\log(|f(x)|^2/\|f\|_2^2)\pi(x)$ , with a zero contribution where $f(x)=0$ . Write $Ef=\sum_xf(x)\pi(x)$ and $\operatorname{Var}_\pi(f)=\|f-Ef\|_2^2$ .

The spectral gap in this mission is the variational constant $\lambda=\inf_{\operatorname{Var}_\pi(f)\ne0}\mathcal E(f,f)/\operatorname{Var}_\pi(f)$ , as in (2.4). The log-Sobolev constant is $\alpha=\inf_{\mathcal L(f)\ne0}\mathcal E(f,f)/\mathcal L(f)$ , as in (3.1). These definitions specify the quantities that Theorem 3.9 relates; in particular, $\lambda$ is the paper's variational quantity, rather than an eigenvalue expression imported from a different convention.

Formalization targets

Theorem 3.9: a single heat-operator estimate bounds $\alpha$

Suppose $2<q<\infty$ , $t_q>0$ , and $M_q$ satisfy $\|H_{t_q}f\|_q\le M_q\|f\|_2$ for every function $f$ . The paper's theorem asserts

\alpha\ge\frac{(1-2/q)\lambda}{2\left(\lambda t_q+\log M_q+(q-2)/q\right)}.

It also covers $q=\infty$ : the hypothesis then uses $\|H_{t_q}f\|_\infty$ , and the two fractions involving $q$ in the displayed bound become $1$ .

Companion results

Theorem 3.10 replaces $H_{t_q}$ in the norm hypothesis with $H_{t_q}-E$ , where $E$ sends a function to its constant mean. Corollary 3.11 relates $\alpha$ to $\tau$ , the first time at which every heat-kernel density $h_t^x(y)=H_t(x,y)/\pi(y)$ is within $1/e$ of $1$ in $\ell^2(\pi)$ :

\frac1{2\alpha}\le\tau\le\frac{4+\log\log(1/\pi_*)}{4\alpha}, \qquad \pi_*=\min_x\pi(x).

The three milestones reproduce the interpolation estimate (3.6), the resulting entropy inequality, and the centering inequality (3.7). Theorem 3.10's printed finite- $q$ denominator contains $(q-2)/2$ ; its displayed proof and the $q=\infty$ use in Corollary 3.11 require $(q-2)/q$ . That proof also needs $\log M_q+(q-2)/q\ge0$ , which the page does not state and without which the printed statement fails on a four-state product chain. The formal companion records both corrections, while the main goal follows the printed Theorem 3.9 exactly.

Significance

Theorem 3.9 makes a norm bound at a chosen time useful beyond that time: it yields a bound on a functional inequality that holds for every function on the state space. Thus estimates obtained from an explicit heat kernel or another analytic method can be compared across chains using the same constant $\alpha$ . The centered version and the bound for $\tau$ connect this functional viewpoint back to convergence from a point mass, as the paper explains in §3.4.

The mathematical results are proved in the 1996 paper. Here the remaining work is to give their finite-state objects, norm hypotheses, and constants machine-checked meanings, then formalize the proofs. The definition layer and the centering inequality have use beyond this mission: they can support other statements about entropy decay and heat-kernel convergence in the same paper.

Difficulty

A bound for $H_t$ in the same norm is too weak to recover the displayed lower bound: the information here is the change from an $\ell^2$ input to an $\ell^q$ output. The dependence of the exponent on time must retain the factors $(1-2/q)$ and $(q-2)/q$ exactly. The endpoint $q=\infty$ also requires a separate norm statement, since a real exponent cannot represent infinity. The centering inequality (3.7) is another substantial step; the paper points to earlier proofs rather than treating it as immediate.

Formalization scope

The state space is a finite Lean type, the kernel a real matrix, and the invariant law a positive real-valued probability vector. Reversibility is detailed balance, and irreducibility is retained from the standing setting of §3.1. The heat semigroup uses the already published Poissonized heat kernel. Operator norms are represented by inequalities quantified over every real function. The finite- $q$ and $q=\infty$ conclusions are separate clauses of the goal. Time is real; $t_q>0$ makes explicit the positive-time convention used in §3.4. Theorem 3.10 carries the condition $M_q\ge e^{-(q-2)/q}$ (and $M_\infty\ge e^{-1}$ ) described above; Corollary 3.11 is stated without any extra condition.

The variational constants are real infima, the logarithms and real powers use Lean's total operations, and the supremum norm is a supremum over the finite state space. The stationary probability hypothesis rules out an empty state space; the operator hypothesis on the constant function forces $M_q\ge1$ in Theorem 3.9. These facts prevent the bound from arising from a zero norm, an empty operator test, an invalid logarithm, or an eigenvalue convention different from (2.4). Useful contributions include finite-state entropy inequalities, interpolation machinery, estimates for the heat operator, and proofs of the three stated milestones.

Selected references

P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Annals of Applied Probability 6 (1996), 695–750. DOI.

10 thms2 active usersReviewed

Complexity Theory Quantum Information Theoretical Computer Science·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing II: Relative to a Random Permutation, a Quantum Algorithm Needs Ω(2^{n/3}) Queries to Decide the First Bit of A⁻¹(1ⁿ)Research Paper

Motivation

An oracle lets an algorithm ask for the value of a function without giving it a description of that function. An oracle lower bound isolates how many questions are needed, even when computation between questions is unrestricted. Bennett, Bernstein, Brassard and Vazirani used this viewpoint to compare classical and quantum access to randomly chosen functions and permutations. Their Theorem 3.6 states an almost-sure separation: relative to a random permutation oracle, a quantum machine using time $o(2^{n/3})$ cannot capture all of $(\mathrm{NP}\cap\mathrm{coNP})^A$ BBBV, Theorem 3.6. The same paper notes that its exponent $1/3$ may reflect the available argument rather than the true boundary BBBV, p. 12.

The finite statement behind that separation is a quantum query lower bound for a uniformly random permutation. It asks about one bit of the inverse image of a fixed string, rather than inversion of the whole permutation. This gives a sharply defined target with the paper's explicit query and error constants.

Setting

Let $\Sigma^n=\{0,1\}^n$ , and let $A$ be a permutation oracle of $\Sigma^n$ . Its inverse image of the all-one string $1^n$ exists and is unique. Define the language $\mathcal L_A$ by putting $y$ in $\mathcal L_A$ when the first bit of $A^{-1}(y)$ is $1$ . The paper observes that access to $A$ puts this language in both $\mathrm{NP}^A$ and $\mathrm{coNP}^A$ : either possible bit of the inverse image can be witnessed by an input to the permutation BBBV, p. 10. This mission tests membership only at $y=1^n$ .

A $T$ -query quantum algorithm starts in a unit vector of a finite complex Hilbert space. A basis configuration records an optional length- $n$ query string, an answer register, and finite workspace. On a querying configuration $(x,z,w)$ , an oracle operation replaces the answer register by $z\oplus A(x)$ ; it leaves a nonquerying configuration unchanged. Each oracle operation is followed by an algorithm-chosen unitary. The final acceptance probability is the sum of the squared amplitudes of accepting basis configurations. A run decides a yes-or-no question if its acceptance probability is at least $2/3$ on a yes instance and at most $1/3$ on a no instance. These thresholds match the paper's bounded-error convention BBBV, §2 and §3.1.

For a state $\phi$ , the query magnitude $q_y(\phi)$ is the total squared amplitude of basis configurations querying string $y$ . Thus $0\le q_y(\phi)\le1$ for a unit state, and the magnitudes over all strings sum to at most $1$ . This is Definition 3.2 of the paper BBBV, p. 7.

Formalization targets

The goal is the finite claim in the proof of Theorem 3.6. For every $n\ge1$ , every finite-workspace algorithm $M$ with $T$ queries, and a uniform permutation $A$ of $\Sigma^n$ ,

T\le\frac{2^{n/3}}{100} \quad\Longrightarrow\quad \Pr_A\!\left[M\text{ fails to decide whether the first bit of }A^{-1}(1^n)\text{ is }1\right]\ge\frac18.

The milestones follow the statements used in the paper: Theorem 3.1 relates Euclidean distance between final states to their observed distributions; Theorem 3.3 bounds the effect of changing answers at queried strings; and the proof of Theorem 3.6 establishes the uniform transposition chain, the $1/2$ membership split, the expected query-magnitude estimate, and the $1/50$ expected final-state distance BBBV, pp. 7–11. The source text of each milestone is recorded with its page in the mission's milestone list.

Significance

The result identifies a concrete task that cannot be decided reliably with too few quantum oracle calls for a positive fraction of length- $n$ permutation oracles. The inverse image exists by definition, so the obstruction is the number of queries needed to learn its first bit. This is the quantitative part of the paper's relative separation for $\mathrm{NP}\cap\mathrm{coNP}$ ; the passage to an almost-sure statement over countably many machines is described in the paper but lies beyond this mission's formal goal BBBV, pp. 10–12.

The theorem is proved on paper and is not claimed here as an open mathematical problem. Formalizing it produces reusable finite-dimensional machinery for quantum queries: an XOR oracle as a unitary basis permutation, query magnitude, a time-dependent hybrid oracle, and counting-based probability over finite permutation spaces. The milestone statements remain open Lean proof obligations in this proposal.

Difficulty

A direct comparison of an algorithm's run under two nearby permutation oracles requires knowing that the algorithm seldom queries the locations where those oracles differ. The distinguished preimage $A^{-1}(1^n)$ cannot simply be declared rarely queried: learning about it is exactly the task under study. The paper therefore studies a chain of random transpositions and a run whose oracle changes by step. The subtle point is that a string used in a later transposition is still uniform when the earlier query state is formed BBBV, pp. 10–11. The expected query-magnitude milestone states that point explicitly.

Formalization scope

The Lean carrier of strings is $\mathrm{Fin}(n)\to\mathbb Z/2\mathbb Z$ . Algorithms use finite configuration types and EuclideanSpace ℂ; the query register is optional, and none represents configurations that make no length- $n$ query. An oracle answers with the full length- $n$ value by XOR in the answer register. The paper describes a Boolean oracle, but one full-value query can be simulated with $n$ Boolean queries and one Boolean query with two full-value queries. The latter direction transfers this lower bound to the paper's oracle at a changed constant. Answers at lengths other than $n$ are fixed and absorbed into the inter-query unitaries, as in the paper's finite-length argument. The full oracle quantum Turing machine, complexity classes as Lean objects, and the almost-sure conclusion are outside the model.

Probabilities and expectations are finite counting fractions. The chain samples a uniform $\pi_0$ and independent uniform $x_1,\ldots,x_{T+1}$ , with $x_0=\pi_0^{-1}(1^n)$ ; this has the same joint law as the paper's conditional sampling order. The recurrence $\pi_{i+1}=\pi_i\circ(x_i\ x_{i+1})$ uses the paper's composition direction. The first-bit test requires $n\ge1$ , and any comparison to $\pi_{T-1}$ requires $T\ge1$ . The goal quantifies over every finite workspace and algorithm before sampling the permutation. A uniform function in place of a permutation, or a predetermined inverse image, would change the task and is excluded.

The paper's Theorem 3.3 prints a final-state bound $\varepsilon$ that fails for a one-query XOR example; the milestone states the valid $2\varepsilon$ bound. Its baseline oracle may vary by step because the proof of Theorem 3.6 uses the hybrid run. The explicit constants $T\le 2^{n/3}/100$ , failure probability $1/8$ , and expected distance $1/50$ remain as printed. General finite-dimensional unitary and probability lemmas, together with a proof of the time-dependent hybrid bound, are welcome contributions. The finite query model and transposition-chain definitions are reusable in other oracle lower bounds.

Selected references

C. H. Bennett, E. Bernstein, G. Brassard, and U. Vazirani, Strengths and weaknesses of quantum computing, SIAM Journal on Computing 26(5), 1997; arXiv:quant-ph/9701001v1.

10 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 2: For a Compact Convex Set of Discrete Distributions, Worst-Case CVaR Equals min_α max_π G_β(x, α, π)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection and risk-averse optimization: for a confidence level $\beta$ it is, roughly, the expected loss in the worst $(1-\beta)$ fraction of outcomes. Its practical appeal comes from the representation of Rockafellar and Uryasev (2000, 2002), which writes CVaR as the minimum over a scalar threshold $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex (often linear) program.

That representation presupposes that the distribution of the uncertain data is known exactly. In practice the scenario probabilities are estimated, and decisions that are optimal for the estimate can perform poorly under a nearby distribution. Zhu and Fukushima (Oper. Res. 57(5), 2009) study the worst-case CVaR: the largest CVaR over a set of distributions that the decision maker considers plausible. For a finite scenario model they show (Theorem 2) that when the plausible set of probability vectors is compact and convex, the worst-case CVaR again has a min–max representation in the threshold $\alpha$ . This is what makes worst-case CVaR minimization tractable: under box uncertainty it becomes a linear program and under ellipsoidal uncertainty a second-order cone program (§2.2.1–2.2.2 of the paper).

Setting

A decision $x \in \mathbb R^n$ incurs the loss $f(x,y)$ , where $y \in \mathbb R^m$ is random. In the discrete model $y$ takes the finitely many values $y_{[1]},\dots,y_{[S]}$ , the scenarios, with probabilities $\pi_1,\dots,\pi_S$ , where $\pi_k \ge 0$ and $\sum_k \pi_k = 1$ . Fix a confidence level $0<\beta<1$ and write $[t]^+ = \max\{t,0\}$ . The Rockafellar–Uryasev function for the distribution $\pi$ is

G_\beta(x,\alpha,\pi) = \alpha + \frac{1}{1-\beta}\sum_{k=1}^S \pi_k\,[f(x,y_{[k]})-\alpha]^+, \qquad \alpha\in\mathbb R,

and the CVaR of the loss at $x$ under $\pi$ is

\mathrm{CVaR}_\beta(x,\pi) = \min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).

The distribution is not known; it is only known to lie in an ambiguity set $\mathcal P_\pi \subseteq \mathbb R^S$ of probability vectors. The worst-case CVaR at $x$ is

\mathrm{WCVaR}_\beta(x) = \sup_{\pi\in\mathcal P_\pi}\mathrm{CVaR}_\beta(x,\pi) = \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi).

In the Lean development these objects are WorstCaseCVaR.Discrete.G, cvar and wcvar, with the scenarios given as ys : Fin S → (Fin m → ℝ) and $\mathcal P_\pi$ as a set P of vectors Fin S → ℝ.

Formalization targets

Goal: Theorem 2 (p. 1159)

If $\mathcal P_\pi$ is a nonempty compact convex set of probability vectors, then for each $x$

\mathrm{WCVaR}_\beta(x) = \min_{\alpha\in\mathbb R}\max_{\pi\in\mathcal P_\pi} G_\beta(x,\alpha,\pi),

with the inner maximum attained for every $\alpha$ and the outer minimum attained at some $\alpha_0$ . The statement fixes no constants and no particular ambiguity set.

Milestones (the steps of the paper's proof, p. 1167)

$G_\beta(x,\alpha,\pi)$ is convex in $\alpha$ for each probability vector $\pi$ and affine in $\pi$ for each $\alpha$ .
There is one nonempty closed bounded interval $\mathcal A$ such that, for every $\pi\in\mathcal P_\pi$ , $\min_{\alpha\in\mathbb R} G_\beta(x,\alpha,\pi) = \min_{\alpha\in\mathcal A} G_\beta(x,\alpha,\pi)$ .
Lemma 1 (p. 1157, Ky Fan's minimax theorem): for convex–concave, suitably semicontinuous $\phi$ on a product of nonempty compact convex sets, $\min_x\max_y\phi = \max_y\min_x\phi$ .
Lemma 1 on $\mathcal A\times\mathcal P_\pi$ : $\max_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathcal A}G_\beta = \min_{\alpha\in\mathcal A}\max_{\pi\in\mathcal P_\pi}G_\beta$ .
The min-max inequality $\inf_{\alpha\in\mathbb R}\sup_{\pi\in\mathcal P_\pi}G_\beta(x,\alpha,\pi) \ge \sup_{\pi\in\mathcal P_\pi}\min_{\alpha\in\mathbb R}G_\beta(x,\alpha,\pi)$ .

Significance

Theorem 2 converts a supremum over distributions of a minimum over thresholds into a minimum over thresholds of a worst case of a function that is affine in $\pi$ . Minimizing $\mathrm{WCVaR}_\beta(x)$ over decisions $x$ is therefore the single minimization problem (16)–(20) of the paper in the variables $(x,u,\alpha,\theta)$ , whose only nonstandard constraint is $\max_{\pi\in\mathcal P_\pi}(\alpha+\frac{1}{1-\beta}\pi^Tu)\le\theta$ . For box and ellipsoidal ambiguity sets that constraint is dualized into linear or conic constraints, which gives the robust portfolio models of §§2.2.1–3 of the paper. The same exchange of $\sup_\pi$ and $\min_\alpha$ underlies many later distributionally robust CVaR models.

The result is proved in the paper (appendix, p. 1167) and is not open. The mission produces a machine-checked proof of it, which to our knowledge does not exist. Mathlib contains Sion's minimax theorem (Sion.exists_isSaddlePointOn), which covers Lemma 1; what is missing is the CVaR-specific part: the convexity of $G_\beta$ in $\alpha$ , the reduction of the threshold to a compact interval uniform over $\mathcal P_\pi$ , and the passage from the compact interval back to all of $\mathbb R$ .

Difficulty

The obvious approach applies a minimax theorem directly to $G_\beta$ on $\mathbb R\times\mathcal P_\pi$ . That fails because $\mathbb R$ is not compact, and minimax equalities on a noncompact factor can fail; the threshold must first be confined to a bounded interval, and the interval must work for every $\pi\in\mathcal P_\pi$ simultaneously. After the exchange on the interval, the minimum over the interval has to be identified with the infimum over all of $\mathbb R$ , which needs the min-max inequality on the unrestricted line. A second subtlety is attainment: every "min" and "max" in the statement is a claim that an extremum exists, and in the real-valued formalization each must be exhibited rather than read off from a supremum.

Formalization scope

Conventions committed to in the Lean statements:

Scenarios are indexed zero-based by Fin S; probability vectors are elements of stdSimplex ℝ (Fin S).
The confidence level satisfies $0<\beta<1$ in every statement (the paper says only that $\beta$ is a confidence level, usually above $0.9$ ).
$\mathrm{CVaR}_\beta(x,\pi)$ is defined as the paper does for discrete distributions, as the minimum of $G_\beta(x,\cdot,\pi)$ , encoded as the real infimum of its values; $\mathrm{WCVaR}_\beta(x)$ is the real supremum of the image of $\mathcal P_\pi$ . Both are true infima and suprema under the hypotheses carried by every theorem.
Theorem 2's hypothesis " $\mathcal P_\pi$ is a compact convex set" is completed by two standing assumptions of §2.2: $\mathcal P_\pi$ consists of probability vectors, and it is nonempty. Without the first, $G_\beta(x,\cdot,\pi)$ can be unbounded below and the real infimum returns a junk value; without the second the supremum is over the empty set.
Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$ , which the paper omits and which are needed for the extrema to exist; its conclusion is a saddle point, equivalent to the attained min–max equality.
In the goal, the right-hand side exhibits an explicit minimizer $\alpha_0$ and the inner maximum is shown to be attained; neither is replaced by a bare infimum or supremum.

No vacuous version of the goal is admissible: the ambiguity set must be nonempty and consist of probability vectors, and the minimum over $\alpha$ must be witnessed.

The development needs only finite sums, convexity on $\mathbb R$ and on the simplex, compactness of $\mathcal P_\pi$ and of closed intervals, and Mathlib's minimax theorem. The reduction to a bounded interval and the min-max inequality are reusable for other finite-scenario CVaR results. Proofs of any milestone are welcome, as are alternative proofs of the goal that avoid the interval reduction.

Selected references

S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar and S. Uryasev, Optimization of Conditional Value-at-Risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar and S. Uryasev, Conditional Value-at-Risk for General Loss Distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
K. Fan, Minimax Theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
M. Sion, On General Minimax Theorems, Pacific Journal of Mathematics 8(1):171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171

7 thms2 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management 1: Under Mixture Distribution Uncertainty, Worst-Case CVaR Equals the Minimum over α of max_i F^i_β(x, α)Research Paper

Motivation

Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection, insurance and stochastic programming. Its practical appeal comes from a variational formula of Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002): CVaR at level $\beta$ is the minimum over a scalar $\alpha$ of a convex function, so that minimizing CVaR over decisions becomes a single convex program, a linear program when the distribution is given by scenarios.

The formula needs the distribution of the random returns, and in practice that distribution is estimated and uncertain. Zhu and Fukushima (Oper. Res. 57(5), 2009) introduce the worst-case CVaR: the supremum of CVaR over a set $\mathcal P$ of candidate distributions. They show it is again a coherent risk measure and that, for several natural choices of $\mathcal P$ , minimizing it remains a tractable convex program. This mission formalizes the first of these results, for $\mathcal P$ the set of all mixtures of finitely many given distributions, a model used in robust statistics and in finance to describe returns under several market regimes.

Setting

A decision $x\in\mathbb R^n$ and a random vector $y\in\mathbb R^m$ determine a loss $f(x,y)\in\mathbb R$ . A confidence level $\beta$ satisfies $0<\beta<1$ (in applications $\beta\ge0.9$ ). Write $[t]^+=\max\{t,0\}$ .

For a probability distribution $P$ of $y$ under which $f(x,\cdot)$ is integrable, the Rockafellar–Uryasev function is

F_\beta(x,\alpha)=\alpha+\frac1{1-\beta}\int_{\mathbb R^m}[f(x,y)-\alpha]^+\,dP(y),\qquad\alpha\in\mathbb R, \tag{1}

and CVaR is its minimum over $\alpha$ :

\mathrm{CVaR}_\beta(x)=\min_{\alpha\in\mathbb R}F_\beta(x,\alpha). \tag{2}

Fix $l\ge1$ likelihood distributions $P^1,\dots,P^l$ on $\mathbb R^m$ and let $\Lambda=\{\lambda\in\mathbb R^l:\lambda_i\ge0,\ \sum_i\lambda_i=1\}$ be the probability simplex. The ambiguity set is the set of mixtures

\mathcal P_M=\Big\{\textstyle\sum_{i=1}^l\lambda_iP^i:\ \lambda\in\Lambda\Big\},

and the worst-case CVaR of $x$ is

\mathrm{WCVaR}_\beta(x)=\sup_{\lambda\in\Lambda}\ \mathrm{CVaR}_\beta(x)\ \text{ under }\ \textstyle\sum_i\lambda_iP^i. \tag{3}

Write $F^i_\beta(x,\alpha)$ for the function (1) with $P=P^i$ , $F^{\mathcal L}_\beta(x,\alpha)=\max_{i\in\mathcal L}F^i_\beta(x,\alpha)$ with $\mathcal L=\{1,\dots,l\}$ , and $H_\beta(x,\alpha,\lambda)$ for the function (1) of the mixture $\sum_i\lambda_iP^i$ .

Formalization targets

Goal: Theorem 1

For every $x$ with $f(x,\cdot)$ integrable under every $P^i$ ,

\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\ \max_{i\in\mathcal L}F^i_\beta(x,\alpha),

with the minimum attained. The supremum over infinitely many distributions on the left becomes a minimum of the pointwise maximum of $l$ functions on the right.

Milestones

The milestones follow the paper's appendix proof (pp. 1166–1167) in order:

(53): $H_\beta(x,\alpha,\lambda)=\sum_i\lambda_iF^i_\beta(x,\alpha)$ for $\lambda\in\Lambda$ .
(54): $\mathrm{WCVaR}_\beta(x)=\max_{\lambda\in\Lambda}\min_{\alpha}H_\beta(x,\alpha,\lambda)$ , both extrema attained.
The minimizer set of $F_\beta(x,\cdot)$ is a nonempty closed bounded interval $[\underline\alpha^*,\overline\alpha^*]$ .
Minimizers of a nonnegative combination of two convex functions on $\mathbb R$ lie between the extreme endpoints of their minimizer intervals.
Every minimizer of $H_\beta(x,\cdot,\lambda)$ lies in $\mathcal A=[\min_i\underline\alpha^*_i,\max_i\overline\alpha^*_i]$ , and the minimum over $\mathbb R$ is attained in $\mathcal A$ .
Lemma 1, the minimax equality for convex–concave functions on compact convex sets.
(55): $\max_\lambda\min_{\mathbb R}H_\beta=\max_\lambda\min_{\mathcal A}H_\beta=\min_{\mathcal A}\max_\lambda H_\beta$ .
(56)–(57): $\mathrm{WCVaR}_\beta(x)=\min_{\alpha\in\mathbb R}\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)$ .
(58)–(59): $\max_{\lambda\in\Lambda}\sum_i\lambda_iF^i_\beta(x,\alpha)=\max_iF^i_\beta(x,\alpha)$ .

An additional item states Corollary 1: $(x^*,\alpha^*)$ minimizes $F^{\mathcal L}_\beta$ over $\mathcal X\times\mathbb R$ exactly when $x^*$ minimizes $\mathrm{WCVaR}_\beta$ over $\mathcal X$ and $\alpha^*$ minimizes $F^{\mathcal L}_\beta(x^*,\cdot)$ .

Significance

The result. Theorem 1 makes worst-case CVaR under mixture uncertainty no harder to optimize than ordinary CVaR. Since each $F^i_\beta$ is jointly convex in $(x,\alpha)$ when $f$ is convex in $x$ , $F^{\mathcal L}_\beta$ is convex, and Corollary 1 turns robust CVaR minimization into one convex program in $(x,\alpha)$ ; with sampled scenarios it is a linear program (the paper's (10)–(15)). It is the starting point for the paper's robust portfolio models (§3), whose ambiguity sets are mixtures of a few estimated return distributions.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof contributes a measure-theoretic treatment of the Rockafellar–Uryasev function for arbitrary distributions (the paper argues with densities and appeals to Remark 1 for the general case), a reusable statement that the minimizer set of $F_\beta$ is a compact interval, and a worked instance of the minimax theorem in Mathlib (Sion) applied to a problem with an unbounded variable.

Difficulty

The obvious argument is to exchange $\sup_\lambda$ and $\min_\alpha$ in $\sup_\lambda\min_\alpha\sum_i\lambda_iF^i_\beta(x,\alpha)$ , since the function is convex in $\alpha$ and affine in $\lambda$ . Minimax theorems for this exchange need compactness of one of the two sets, and the variable $\alpha$ ranges over all of $\mathbb R$ . The step that has to be supplied is a localization: all minimizers in $\alpha$ , for every $\lambda$ at once, lie in one compact interval $\mathcal A$ determined by the minimizer sets of the components. This in turn requires knowing that each $F^i_\beta(x,\cdot)$ has a nonempty bounded minimizer set, which uses $0<\beta<1$ and integrability of the loss: at $\beta=0$ the minimizer set can be a half-line and the localization fails. A second point is attainment: the outer supremum over $\Lambda$ is a maximum only because the inner minimum depends continuously on $\lambda$ .

Formalization scope

Distributions are probability measures on Fin m → ℝ (not densities); Remark 1 of the paper extends all results to general distributions, and a density is a special case. Decisions are Fin n → ℝ, the loss is f : (Fin n → ℝ) → (Fin m → ℝ) → ℝ, and the likelihood distributions are P : Fin l → Measure (Fin m → ℝ) with indices zero-based and [NeZero l].
Every theorem assumes $0<\beta<1$ , that each $P^i$ is a probability measure, and that $f(x,\cdot)$ is integrable under each $P^i$ (the paper's $E|f(x,y)|<\infty$ ).
CVaR is defined by (2) as the infimum of the values of $F_\beta(x,\cdot)$ ; the tail-mean definition and the Rockafellar–Uryasev identity between the two are not part of the mission. The mixture is the finite sum of measures $\sum_i\lambda_iP^i$ , $\Lambda$ is Mathlib's stdSimplex, and WCVaR is the supremum of the image of $\Lambda$ .
Every min and max in the paper is stated as attained, with an explicit minimizer or as IsGreatest/IsLeast; no real sInf or sSup is evaluated on an empty or unbounded set, so no statement can hold through Lean's junk value $0$ .
Lemma 1 is stated with lower semicontinuity in $x$ and upper semicontinuity in $y$ , which the printed statement omits and without which the extrema need not exist.
The definitions $F_\beta$ , CVaR, mixture and WCVaR are reusable for any risk-measure development; the interval property of $\arg\min F_\beta$ is of independent use. Proofs of any milestone, and lemmas on the Rockafellar–Uryasev function for general measures, are welcome.

Selected references

S. Zhu and M. Fukushima, Worst-Case Conditional Value-at-Risk with Application to Robust Portfolio Management, Operations Research 57(5):1155–1168, 2009. https://doi.org/10.1287/opre.1080.0684
R. T. Rockafellar and S. Uryasev, Optimization of conditional value-at-risk, Journal of Risk 2(3):21–41, 2000. https://doi.org/10.21314/JOR.2000.038
R. T. Rockafellar and S. Uryasev, Conditional value-at-risk for general loss distributions, Journal of Banking & Finance 26(7):1443–1471, 2002. https://doi.org/10.1016/S0378-4266(02)00271-6
K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1):42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068

11 thms2 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

Fast Rates for Support Vector Machines Using Gaussian Kernels 1: Under Tsybakov and Geometric Noise, Gaussian-Kernel SVMs Reach Excess Risk Cx²n^{−β+ε} with Probability 1 − e^{−x}Research Paper

Motivation

Support vector machines classify observations by choosing a real-valued function from a reproducing kernel Hilbert space and using its sign as the predicted label. The Gaussian kernel is widely used because it gives a flexible class of functions, but that flexibility alone does not explain how quickly classification error approaches the best possible error as the training sample grows. Steinwart and Scovel's 2007 paper identifies distributional conditions under which a Gaussian-kernel SVM achieves a polynomial, and sometimes nearly linear, excess-risk rate. The conditions describe both ambiguity in the labels and the location of data relative to the decision boundary.

The article's result is already proved mathematically. This mission asks for machine-checked statements and proofs of its finite-geometric-exponent, no-offset rate and selected supporting results. It uses arXiv:0708.1838v1, the electronic reprint of the Annals of Statistics article. Its printed page number equals its PDF page number throughout; all page references below use those numbers.

Setting

Let $X$ be the closed unit ball of $\mathbb R^d$ , where $d>0$ , and let the label set be $Y=\{-1,1\}$ . A distribution $P$ on $X\times Y$ has input marginal $\mu=P_X$ and a measurable regression function $\eta(x)=P(y=1\mid x)$ . In the Lean representation, $\mu$ and one version of $\eta$ are carried explicitly; the joint law gives conditional masses $\eta(x)$ and $1-\eta(x)$ to the two labels. Classification predicts $\operatorname{sign}f(x)$ , with $\operatorname{sign}(0)=1$ . Write $R_P(f)$ for its error probability and $R_P$ for the smallest such risk over measurable decision functions.

The hinge loss is $\ell(y,t)=\max\{0,1-yt\}$ . The Gaussian kernel with parameter $\sigma>0$ is $k_\sigma(x,x')=\exp(-\sigma^2\|x-x'\|^2)$ , and $H_\sigma(X)$ is its restricted RKHS. Given a sample $T$ of size $n$ , an SVM without offset minimizes $\lambda\|f\|^2_{H_\sigma(X)}+R_{\ell,T}(f)$ over that space. The approximation error $a_\sigma(\lambda)$ is the infimum of the corresponding population objective minus the unrestricted Bayes hinge risk; equation (6) uses that unrestricted baseline.

Two assumptions describe the distribution. It has Tsybakov noise exponent $q\in[0,\infty]$ if, for sufficiently small $t>0$ , $\mu\{|2\eta-1|\le t\}\le C t^q$ for some $C>0$ . To define geometric noise exponent $\alpha>0$ , partition $X$ according to whether $\eta$ is below, above, or equal to $1/2$ . The distance $\tau_x$ goes from a point in either strict class to the opposite strict class together with the equal-probability class. The geometric condition is

\int_X |2\eta(x)-1|\exp(-\tau_x^2/t)\,d\mu(x) \le C t^{\alpha d/2}\qquad(t>0).

These are Definitions 2.2 and 2.3 and equation (7) of the paper.

Formalization targets

The goal is the finite- $\alpha$ , no-offset clause of Theorem 2.8. With the paper's two-case exponent $\beta=\beta(\alpha,q)$ , set $\lambda_n=n^{-(\alpha+1)\beta/\alpha}$ and $\sigma_n=n^{\beta/(\alpha d)}$ . For every $\varepsilon>0$ , one constant $C>0$ works uniformly for $x\ge1$ and $n\ge1$ :

\Pr^*\!\left\{T:R_P(f_{T,\lambda_n}) \le R_P+C x^2n^{-\beta+\varepsilon}\right\}\ge1-e^{-x}.

Here $\Pr^*$ is outer probability, and the statement applies to every empirical minimizer. The formula for $\beta$ is $\alpha/(2\alpha+1)$ in the first case, $\alpha\le(q+2)/(2q)$ , and $2\alpha(q+1)/(2\alpha(q+2)+3q+4)$ otherwise; the paper's limiting convention specifies $q=\infty$ .

Three milestones record results used on this path. Theorem 2.1 bounds empirical covering numbers of Gaussian RKHS balls, uniformly in $\sigma$ and the sample. Lemma 4.1 locates balls of radius $\tau_x$ inside the corresponding enlarged decision class. Theorem 2.7 bounds the approximation error by

a_\sigma(\lambda)\le c_d\bigl(\sigma^d\lambda+C(2d)^{\alpha d/2}\sigma^{-\alpha d}\bigr),

where $c_d$ depends only on dimension. Their exact source text and page positions appear in the milestone list.

Significance

Theorem 2.8 gives a quantitative guarantee for classification risk, rather than only convergence of the regularized hinge objective. The rate responds to both the label-noise exponent and the concentration of input mass near the decision boundary. In the regimes discussed after the theorem, the exponent can approach one; the paper's Remark 2.9 compares it with the $n^{-1/2}$ benchmark.

Formalizing this result adds a concrete Gaussian RKHS norm compatible with a kernel parameter that changes with $n$ , an explicit binary-law model, extended-valued risks and covering numbers, and source-indexed bounds on approximation and complexity. Those objects can be reused in later SVM and kernel-learning statements. The paper's argument is a published proof; the Lean theorem files here are open proof obligations, while the definition files have compiled bodies. No claim of a machine-checked proof of the rate is made.

Difficulty

It is not enough to combine a general consistency theorem with the noise assumptions. The kernel parameter grows with sample size, so the relevant hypothesis class changes with $n$ ; a complexity estimate for one fixed class gives no uniform rate. Geometric noise controls approximation error, while Tsybakov noise controls a different fluctuation quantity, and neither by itself supplies the stated exponent. The probability statement also concerns an event defined by empirical minimizers, whose measurability the source deliberately avoids by using outer probability. These are the points at which a direct fixed-class or ordinary-probability statement would fail to match Theorem 2.8.

Formalization scope

Lean represents functions on all of $\mathbb R^d$ but uses only their restrictions to $X$ . The joint distribution is built from a probability marginal and a fixed measurable $\eta:\mathbb R^d\to[0,1]$ . This makes the paper's choice of regression-function version explicit. The Gaussian RKHS squared norm is the supremum over finite normalized kernel-section combinations; it is $+\infty$ outside the RKHS. A covering number is the least positive finite cardinality of a cover with centers in the ambient empirical function space, or $+\infty$ if there is no such cover. Hinge and classification risks are extended nonnegative integrals, and Bayes risks range over measurable functions.

The assumptions $d>0$ and $n\ge1$ give the divisions and powers their intended domains. For $q=\infty$ , the small- $t$ noise bound uses zero on the right, as in the source convention. The paper leaves distance to an empty set unstated; this mission pins $d(x,\varnothing)=0$ . With the infinite-distance convention, Lemma 4.1 and Theorem 2.7 fail for a one-class regression function. The proof display (25) has a volume-factor slip in high dimension; Theorem 2.7 is stated with its printed conclusion, and the issue is recorded in the moderation notes. The goal event includes existence of an empirical minimizer, a fact stated in the paper's setup, and quantifies over every minimizer. This excludes a vacuous SVM predicate. The constant $C$ is chosen before $x$ and $n$ .

The clauses for $\alpha=\infty$ and an SVM with offset are outside this mission. The separate series mission addresses the implication from an envelope assumption to geometric noise. Further contributions toward the §5 empirical-process estimates, §6 variance estimates, and §7 shrinking and general-rate theorems are welcome; they are not asserted as milestones in this draft.

Selected references

Ingo Steinwart and Clint Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 2007, 575–607. arXiv:0708.1838v1, DOI:10.1214/009053606000001226.

11 thms2 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Negative Dynamic Programming II: With Non-Positive Rewards on Borel Spaces, the Optimal Return Satisfies the Optimality EquationResearch Paper

Motivation

Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.

Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.

Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, $(p,\varepsilon)$ -optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation $J^* = T(J^*)$ under (P), (N) and (D).

Setting

The states $S$ and actions $A$ are non-empty Borel sets. A law of motion $q(\cdot\mid s,a)$ is a probability kernel from $S\times A$ to $S$ . The return $r(s,a,t)$ is a Borel function with $-\infty < r \le 0$ whose expectation $\int r(s,a,t)\,dq(t\mid s,a)$ is finite for every $(s,a)$ . A policy $\pi = (\pi_1,\pi_2,\dots)$ draws the $n$ th action from a kernel $\pi_n(\cdot\mid s_1,a_1,\dots,s_n)$ that may depend on the whole history. A Markov policy $(f_1,f_2,\dots)$ uses measurable maps $f_n:S\to A$ , and a stationary policy $f^{(\infty)}$ uses one map at every stage. The expected return from the initial state $s$ is

I(\pi)(s) = \sum_{n\ge1} E^\pi_s\, r(s_n,a_n,s_{n+1}) \in [-\infty,0],

and the optimal return is

v^*(s) = \sup_\pi I(\pi)(s),

the supremum over all policies. Write $M(S)$ for the non-positive, extended real-valued Borel functions on $S$ . For $u\in M(S)$ and an action $a$ ,

T_a u(s) = \int \big[r(s,a,t) + u(t)\big]\,dq(t\mid s,a).

$T$ denotes the same operator for a measurable rule $f$ in place of $a$ , and $U = \sup_n T_n$ for a Markov policy $(f_1,f_2,\dots)$ . A policy $\pi^*$ is $(p,\varepsilon)$ -optimal, for a probability $p$ on $S$ , if $p\{I(\pi^*) \ge v^* - \varepsilon\} = 1$ . The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.

Formalization targets

Goal: the optimality equation (Theorem 8.2, negative case)

v^*(s) = \sup_{a\in A} T_a v^*(s) \qquad\text{for all } s\in S.

The equation involves no constants and no regularity hypotheses on $v^*$ .

Milestones

Theorem 5.2 (a)–(g): monotonicity, translation, sup-, limit- and selection properties of $U$ .
Theorem 6.1: if $Uv\ge v$ for $v\in M(S)$ , some Markov policy generated from $\hat\pi$ has $I(\pi)\ge v-\varepsilon$ .
Lemma 6.2: $U$ conserves $\sup_n I({}^n\pi)$ and $\lim_n U^n \sup_n I({}^n\pi)$ .
Theorem 6.2: one Markov policy comes within $\varepsilon$ of the supremum of the returns of countably many Markov policies.
Lemma 7.1, Lemma 7.2: measurability of $(s,\nu)\mapsto\int u(s,x)\,d\nu(x)$ , and Borel measurability of the set of pairs $(s, e_\pi(s))$ , where $e_\pi(s)$ is the law of the future under $\pi$ .
Theorem 7.1: $v^*$ is absolutely measurable.
Theorem 8.1: for every $p$ and $\varepsilon>0$ a $(p,\varepsilon)$ -optimal Markov policy exists.

Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).

Significance

The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in $\sup_a T_a v^*$ can be tested for optimality. Value iteration and policy improvement can be compared with $v^*$ . The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case $v^*$ satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that $v^*$ is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.

Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.

Difficulty

Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state $t$ , a policy that is $\varepsilon$ -optimal from $t$ and concatenates. Without measurable selection this concatenation is not a policy. The set of $t$ where a given policy is $\varepsilon$ -optimal need not be Borel, and $v^*$ itself need not be Borel measurable, so even $\int v^*\,dq$ needs justification. Second, the contraction argument of the discounted case is unavailable. $U$ does not contract, it conserves $v+c$ along with $v$ , and value iteration from $0$ can converge to a function strictly above $v^*$ . The paper's Example 6.1 shows that the limit of $U^n0$ , the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.

Formalization scope

States and actions are non-empty standard Borel types. Policies are the published Blackwell plans (DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from $0$ (Lean's π.κ n is the paper's $\pi_{n+1}$ ). Markov policies are MarkovPlan; " $\pi$ -generated" and $G(\hat\pi)$ are the published IsGenerated and IsGeneratedPlan.
Only the negative case is formalized: $r\le0$ real-valued, $qr$ integrable, $\beta=1$ . The discounted and positive parts of Theorems 5.2, 7.1, 8.1 and 8.2, including the uniqueness and minimality clauses of Theorem 8.2, are not stated.
Returns take values in EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map $-\infty$ to $0$ and make the goal false or vacuous.
$v^*$ is the supremum over all plans. It is not assumed measurable and is never replaced by a measurable modification. $T_a v^*$ is a lintegral of a possibly non-measurable function, which equals the completion integral because $v^*$ is absolutely measurable (Theorem 7.1).
Explicit readings of the page: the hypothesis $u\in M(S)$ of each operator statement is IsNegM u. Theorem 5.2(b) assumes $u+c\in M(S)$ . " $U$ conserves $v$ " includes $v\in M(S)$ . Lemma 6.2 asserts that the limit defining $v_\pi$ exists. Theorem 6.2 states $\ge$ everywhere and $>$ where $\sup_j I(\pi^j) > -\infty$ (the printed $>$ fails where the supremum is $-\infty$ ). $(p,\varepsilon)$ -optimality is " $p$ -almost everywhere". Absolute measurability is NullMeasurable for every probability measure. $P(X)$ carries the Giry σ-field. The extra Theorem 8.4 reads the printed " $I(\pi) < u$ " as " $\le$ " (the strict reading is false).
Reusable infrastructure: the negative model, the Ionescu-Tulcea law of the future (futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.

Selected references

R. E. Strauch, Negative Dynamic Programming, Ann. Math. Statist. 37(4) (1966) 871–890. https://doi.org/10.1214/aoms/1177699369
D. Blackwell, Discounted Dynamic Programming, Ann. Math. Statist. 36(1) (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
D. Blackwell, Positive Dynamic Programming, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1 (1967) 415–418. https://projecteuclid.org/euclid.bsmsp/1200512999
L. E. Dubins and L. J. Savage, How to Gamble If You Must, McGraw-Hill, 1965.
D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/soc.html

21 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Understanding the Efficiency of Multi-Server Service Systems I: With Poisson Arrivals and Finitely Many Service-Time Values of Mean 1, the Number of Busy Servers in M/G/∞ Is Poisson(λ)Research Paper

Motivation

Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate $\lambda$ , how many servers $s$ are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule

s = \lambda + \gamma\sqrt{\lambda},

where the grade of service $\gamma > 0$ sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.

Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers $N$ in the IS model is Poisson with mean $\lambda$ , its mean and variance are both $\lambda$ , so the event "more than $s$ servers busy" has roughly constant probability when $s - \lambda$ is a fixed multiple of $\sqrt\lambda$ . The Poisson law of $N$ is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean $1$ (M/G/∞ with finite support).

Timeline:

The stationary number in system of M/G/∞ is classically known to be Poisson with mean $\lambda \cdot E[S]$ for general service-time laws (Palm's theorem; see Gross et al., Fundamentals of Queueing Theory).
Halfin and Whitt (Operations Research 29, 1981) proved the heavy-traffic limit theorem that justifies square-root staffing for GI/M/s queues.
Whitt (1992) gave the elementary IS derivation formalized here, with the finite-support M/G/∞ case argued through splitting a Poisson stream into independent class streams.

Setting

Time is measured in units of the mean service time. Let $T_0, T_1, T_2, \dots$ be i.i.d. exponential random variables with rate $\lambda > 0$ , the interarrival times, and let $\tau_n = T_0 + \cdots + T_{n-1}$ be the $n$ -th arrival epoch. The arrival counting process $A(t)$ is the number of $n \ge 1$ with $\tau_n \le t$ , the number of arrivals in $(0, t]$ . This is a Poisson process of rate $\lambda$ .

Customers are numbered $k = 0, 1, 2, \dots$ ; customer $k$ arrives at $\tau_{k+1}$ , is served at once, and has service time $D_k$ . Following the paper (proof of Proposition 2.3, p. 712), an arrival at time $t$ is counted and a departure at time $t$ is not, so customer $k$ is present at $t$ iff $\tau_{k+1} \le t < \tau_{k+1} + D_k$ . The number of busy servers is

N(t) = \#\{k : \tau_{k+1} \le t < \tau_{k+1} + D_k\}.

For the M/G/∞ case fix $m \ge 1$ classes with probabilities $p_1, \dots, p_m$ and values $d_1, \dots, d_m \ge 0$ . Each customer carries a class label $J_k$ , the labels are i.i.d. with $P(J_k = i) = p_i$ and independent of the interarrival times, and $D_k = d_{J_k}$ . The class- $i$ busy count is $N_i(t) = \#\{k : J_k = i,\ \tau_{k+1} \le t < \tau_{k+1} + d_i\}$ .

Formalization targets

Goal: the M/G/∞ claim (§2.5, p. 713)

If $\sum_{i=1}^m p_i d_i = 1$ and $t > \max_i d_i$ , then

P\big(N(t) = k\big) = e^{-\lambda}\frac{\lambda^k}{k!}, \qquad k = 0, 1, 2, \dots

The law depends on the service-time distribution only through its mean.

Milestones

Proposition 2.3 (p. 712): with unit service times, $N(t) = A(t) - A(t-1)$ , pathwise.
Proof of Proposition 2.4 (p. 712): for $t \ge 1$ , $A(t) - A(t-1)$ has the same law as $A(1)$ .
Proposition 2.4 (p. 712): in M/D/∞ with unit service times, $N(t) \sim \mathrm{Poisson}(\lambda)$ for each $t > 1$ .
§2.5, splitting (p. 713): the class- $i$ arrivals form independent Poisson streams of rates $\lambda p_i$ ; stated as independence and Poisson laws of the class counts in one window $(a_i, b_i]$ per class.
§2.5, "Hence" (p. 713): for $t > \max_i d_i$ , the $N_i(t)$ are independent, $N_i(t) \sim \mathrm{Poisson}(\lambda p_i d_i)$ , and $N(t) = \sum_i N_i(t)$ almost surely.

A companion item, Proposition 2.1 (p. 710), states that (2) implies $\lambda = s + \gamma^2/2 - \gamma\sqrt{s + \gamma^2/4}$ and $s - \gamma\sqrt s \le \lambda \le s - \gamma\sqrt s + \gamma^2/2$ , connecting (2) to the utilization equation $\lambda = s - \gamma\sqrt s$ .

Significance

The goal is the step that turns the IS heuristic from a special case into a statement about general service: since $N(t)$ is Poisson with mean $\lambda$ whatever the finite service-time law of mean $1$ , the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that $s$ -server congestion is nearly insensitive to the service distribution beyond its mean when $s$ is large.

The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:

a Poisson process built from exponential interarrival times, with the stationary-increment property derived rather than assumed;
Poisson splitting (thinning by i.i.d. labels) with independence of the class streams, a tool reused throughout queueing and inventory theory;
the M/G/∞ Poisson law for discrete service times, complementing the open platform items ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.

The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law $A(t) \sim \mathrm{Poisson}(\lambda t)$ ) is related but distinct from milestone 2, which concerns the increment over $(t-1, t]$ .

Difficulty

The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time $t - 1$ : the residual time to the next arrival after $t-1$ must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by $t-1$ ), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows $(t - d_i, t]$ of different classes make this unavoidable.

Formalization scope

The arrival process is the published definition QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.
The model IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.
Counts are Set.ncard, which is $0$ on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by $t$ , and the decomposition $N(t) = \sum_i N_i(t)$ is stated almost surely. Poisson laws are stated pointwise, $P(X = k) = e^{-c}c^k/k!$ , avoiding pushforwards of possibly non-measurable maps.
Standing conventions: service rate $1$ ; the system starts empty at time $0$ ; arrival counted at $t$ , departure not; "steady state" means the law at each fixed $t > \max_i d_i$ , with no limit $t \to \infty$ ; the paper's $1 \le i \le n$ is Fin m. The constraint $\sum_i p_i d_i = 1$ forces $m \ge 1$ , and the label law forces $p_i \ge 0$ and $\sum_i p_i = 1$ . Added hypotheses: $d_i \ge 0$ (service times are nonnegative) and, in Proposition 2.1, $\gamma > 0$ (the paper's grade of service).
Infrastructure welcome: memorylessness of the Poisson process at a fixed time, Poisson thinning with independent marks, and the finite-sum version of Mathlib's IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.

Selected references

W. Whitt, Understanding the efficiency of multi-server service systems, Management Science 38(5):708–723, 1992. https://doi.org/10.1287/mnsc.38.5.708
S. Halfin and W. Whitt, Heavy-traffic limits for queues with many exponential servers, Operations Research 29(3):567–588, 1981. https://doi.org/10.1287/opre.29.3.567
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968.
D. Gross, J. F. Shortle, J. M. Thompson and C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008. https://doi.org/10.1002/9781118625651

8 thms2 active usersReviewed

Markov Chain Stochastic Systems·Captain: mikedeng1

Random Walks in a Random Environment 3: With One-Way Mirrors σ ∈ {0, θ}, X_n/(n/log_θ n) → ½ in Probability if γθ = 1, and n^(−1/ρ)X_n Has Limit Laws Along Subsequences if γθ > 1Research Paper

Why the walk slows down

A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.

The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after $n$ steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.

The walk and its mirror environment

Let $(\Omega,\mathcal F,P)$ be a probability space and let $\alpha_j$ , $j\in\mathbb Z$ , be independent, identically distributed random variables in $[0,1]$ . The environment is the complete sequence $\alpha=(\alpha_j)_{j\in\mathbb Z}$ . Conditional on a fixed environment, a nearest-neighbour walk starts at $X_0=0$ and, from site $j$ , moves to $j+1$ with probability $\alpha_j$ and to $j-1$ with probability $1-\alpha_j$ . The annealed probability $P$ averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between $X$ and $\alpha$ .

Fix $\theta>1$ and $0<\gamma<1$ . Solomon’s example has $\alpha_j=1$ with probability $1-\gamma$ and $\alpha_j=(1+\theta)^{-1}$ with probability $\gamma$ . Equivalently, the left-to-right odds ratio $\sigma_j=(1-\alpha_j)/\alpha_j$ takes values $0$ and $\theta$ . A site with $\sigma_j=0$ is a one-way mirror. Write $V_0=0$ and let $V_n$ be the position of the $n$ th mirror strictly to the right of zero. Let $T_j$ be the first time the walk reaches site $j$ , with $T_j=\infty$ if it never does. For $b>0$ , $\log_b x$ means the logarithm in base $b$ , and $\{x\}=x-\lfloor x\rfloor$ is the fractional part.

The parameters used below are

\nu=\frac{2\theta}{(\theta-1)^2},\qquad K=\frac{1-\gamma}{\gamma}\nu,\qquad \rho=\log_{1/\gamma}\theta.

When $\gamma\theta>1$ , the paper specifies a probability law $F_\varepsilon$ on $[0,\infty)$ by its Laplace transform

\int_0^\infty e^{-ux}\,dF_\varepsilon(x)=\exp\left[-Ku\sum_{j\in\mathbb Z}\frac{(\gamma\theta)^{j-\varepsilon}}{1+\nu u\theta^{j-\varepsilon}}\right],\qquad u>0.

Here $F_\varepsilon(t)$ also denotes that law’s distribution function at $t$ . The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on $(-\infty,t]$ .

Formalization targets

The first clause of Theorem (2.20) is the critical growth law. If $\gamma\theta=1$ , then

\frac{X_n}{n/\log_\theta n}\xrightarrow{P}\frac12.

The second clause describes the supercritical case. If $\gamma\theta>1$ , $n_k\to\infty$ , and $\{\log_\theta n_k\}\to\varepsilon$ , then for each $x>0$ ,

P\!\left(n_k^{-1/\rho}X_{n_k}<x\right)\longrightarrow 1-F_{\lambda(x)}\!\left(((1-\gamma)x)^{-\rho}\right), \qquad \lambda(x)=\varepsilon+\log_{1/\gamma}((1-\gamma)x).

Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base $\theta$ ; the two passage-time results use base $1/\gamma$ , exactly as printed Solomon 1975, pp. 12–19.

What the result gives

The critical law identifies the constant in the growth scale $n/\log_\theta n$ . The supercritical law shows that a single power normalization $n^{1/\rho}$ does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position $X_n$ itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).

The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.

Where the difficulty lies

The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At $\gamma\theta=1$ , their accumulation produces a logarithmic correction; at $\gamma\theta>1$ , the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions $V_n$ does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.

Formalization scope

The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is $\theta>1$ , $0<\gamma<1$ , $\gamma\theta\ge1$ . The strict bounds on $\gamma$ make both atom probabilities meaningful and the logarithm base $1/\gamma$ valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.

First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on $[0,\infty)$ with the exact transform (2.12), preventing a degenerate or unrelated choice of $F$ .

A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.

Selected references

Fred Solomon, Random Walks in a Random Environment, The Annals of Probability 3(1):1–31, 1975. DOI: 10.1214/aop/1176996444.

9 thms2 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 2: The Ergodic Theorem — a Cumulative Process Satisfies w_t/t → κ₁/μ₁ with Probability OneResearch Paper

Motivation

Many quantities in operations research accumulate over time in a system that periodically starts afresh: the cost incurred by an inventory system that returns to the same stock level, the work completed by a server between successive moments it empties, the reward collected by a machine between repairs. The basic question about such a quantity is its long-run rate: does the amount accumulated by time $t$ , divided by $t$ , settle down, and to what?

W. L. Smith's 1955 paper Regenerative stochastic processes (DOI 10.1098/rspa.1955.0198) introduced the class of cumulative processes to answer this question, and §5·3 of the paper proves the answer, Theorem 7, which Smith calls "the ergodic theorem": the long-run rate equals the expected accumulation per cycle divided by the expected cycle length. In later textbooks this is the renewal–reward theorem, the standard tool for computing long-run averages of regenerative systems in queueing, inventory and reliability models.

Timeline. Doob (1948) proved the strong law $n_t/t \to 1/\mu_1$ for renewal counting processes (Trans. AMS 63). Smith (1955) defined cumulative processes by conditions (C1)–(C2) and proved Theorem 7 under a first-moment condition on the variation per cycle, together with central limit theorems (Theorems 9–10) for the same processes.

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ .

A renewal process is a sequence $t_1, t_2, \dots$ of independent, identically distributed, non-negative random variables that are not zero with probability one, i.e. $P\{t_1 = 0\} < 1$ . Write $\mu_1 = E t_1$ . In this mission the delay is $t_0 = 0$ , the regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ , and the counting variable

n_t = \#\{k \ge 0 : T_k \le t\}

is the number of regenerations in $[0, t]$ (the paper's "greatest integer $k$ such that $T_{k-1} \le t$ "). The forward variable $Z_t = \sum_{i=1}^{n_t+1} t_i - t$ measures how far $t$ is from the regeneration epoch $T_{n_t+1}$ .

Let $w = (w_t)$ be a real-valued process with $w_0 = 0$ . Its cycle increments are $y_n = w_{T_n} - w_{T_{n-1}}$ , $n \ge 1$ , and $\kappa_1 = E y_1$ . On a path of bounded variation on every finite interval, the variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ is the total variation of the path over $[0, t]$ ; the cycle variations are $\tilde y_n = \tilde w_{T_n} - \tilde w_{T_{n-1}}$ , and $\tilde\kappa_p = E \tilde y_1^{\,p}$ .

The process $w$ is a cumulative process when

(C1) $y_1, y_2, \dots$ are independent and identically distributed, and
(C2) with probability one, $w$ is of bounded variation in every finite interval.

Formalization targets

Goal: Theorem 7 (the ergodic theorem)

If $w$ is a cumulative process, $\mu_1 < \infty$ , $\tilde\kappa_1 < \infty$ , $t_0 = 0$ and $w_0 = 0$ , then

\lim_{t \to \infty} \frac{w_t}{t} = \frac{\kappa_1}{\mu_1} \quad \text{with probability one.}

The statement fixes no rate and no constant; it is the exact limit of the paper.

Milestones, in the order the proof uses them

Lemma 7. For i.i.d. $x_n$ with $E|x_n|^p < \infty$ , $p > 0$ : $x_n / n^{1/p} \to 0$ with probability one.
Renewal strong law (proof of Lemma 8): $n_t / t \to 1/\mu_1$ with probability one when $\mu_1 < \infty$ .
Lemma 8. If $t_0 = 0$ , $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$ ( $p > 0$ ), then

\lim_{t \to \infty} \frac{w_{t+Z_t} - w_t}{t^{1/p}} = 0 \quad \text{with probability one.}

(5·3·4). $\sum_{i=1}^{n_t+1} y_i / (n_t + 1) \to \kappa_1$ with probability one.
The limit along regeneration epochs. $w_{t+Z_t} / t \to \kappa_1/\mu_1$ with probability one.

Significance

The ergodic theorem turns a question about a whole sample path into a question about one cycle. Once a system is shown to regenerate, its long-run average cost, throughput or utilization is the ratio of two one-cycle expectations, which can often be computed in closed form. This is how long-run averages are evaluated for $M/G/1$ -type queues, $(s,S)$ inventory policies and alternating-renewal reliability models, and it is the first step in average-cost analyses of regenerative Markov decision processes. Lemma 8, with $p > 1$ , also controls the error term in Smith's central limit theorem for cumulative processes.

The result is classical and proved. As far as the platform and Mathlib are concerned, it is not formalized: Mathlib has the strong law of large numbers for i.i.d. sequences (ProbabilityTheory.strong_law_ae) but no renewal counting process, no renewal strong law, and no renewal–reward theorem. A complete development gives machine-checked versions of all three, stated for real time and for cycle lengths that may vanish with positive probability.

Difficulty

The obvious argument writes $w_t / t$ as $\big(\sum_{i \le n_t} y_i / n_t\big) \cdot (n_t / t)$ and applies the strong law to each factor. This fails in two places. First, $w_t$ is not a sum of whole cycles: the cycle containing $t$ is only partly completed, and its contribution has to be shown negligible. The increment $y_n$ does not control it, because $w$ may oscillate inside a cycle and return; it is the variation $\tilde y_n$ that bounds the partial contribution, which is why the hypothesis is on $\tilde\kappa_1$ rather than on $\kappa_1$ . Second, the strong law is a statement about a deterministic index $n \to \infty$ , while here the index $n_t$ is random and depends on the cycle lengths, which need not be independent of the increments. Transferring almost-sure convergence through the random index requires $n_t \to \infty$ almost surely, which in turn uses $P\{t_1 = 0\} < 1$ .

Formalization scope

Time is real: every limit is along $t \to \infty$ in $\mathbb R$ (Filter.atTop on ℝ), and "with probability one" is an almost-everywhere statement placed outside the limit. Random variables are real-valued. The renewal process is the structure IsRenewalProcess (cycle lengths measurable, mutually independent, identically distributed, non-negative everywhere, $P\{t_1 = 0\} < 1$ ); $t_0 = 0$ and $w_0 = 0$ are explicit hypotheses holding at every sample point. Moments are Bochner integrals guarded by integrability hypotheses: $\mu_1 < \infty$ is integrability of $t_1$ , $\tilde\kappa_p < \infty$ is integrability of $\tilde y_1^{\,p}$ . The positivity $\mu_1 > 0$ is never assumed; it follows from $P\{t_1 = 0\} < 1$ .

The count $n_t$ is a cardinality; on the null event where infinitely many epochs lie below $t$ it takes the value $0$ , and finiteness is never assumed. The variation process is Mathlib's eVariationOn of the path over $[0, t]$ , set to $0$ on paths that are not of bounded variation, exactly as the paper prescribes.

Condition (C1) is read literally: only the increments $y_n$ are i.i.d., and no independence between cycle lengths and increments is assumed. In addition the cycle variations $\tilde y_n$ are assumed identically distributed; the paper's notation $\tilde\kappa_p$ presupposes this. The statement is not trivialized by a stronger model: taking $w$ to be a Lévy process, or a deterministic multiple of $t$ , would make the theorem immediate and is not what is formalized.

Two misprints of the paper are corrected in the formal statements and kept in the verbatim milestone text: (5·3·4) prints the limit as $\nu_1$ , which must be $\kappa_1$ ; and the proof bound (5·3·1) uses $\tilde y_{n_t+1}$ alone, where the interval $[t, t+Z_t]$ also meets cycle $n_t$ .

Needed infrastructure: a renewal counting process in continuous time with its strong law; a lemma that almost-sure convergence of a sequence passes to a random index tending to infinity; the comparison $|w_b - w_a| \le \tilde w_b - \tilde w_a$ for paths of bounded variation. All three are reusable well beyond this mission (renewal–reward arguments, regenerative simulation, average-cost Markov decision processes). Contributions of any milestone, and of these general lemmas as separate theorems, are welcome.

Selected references

W. L. Smith, Regenerative stochastic processes, Proceedings of the Royal Society of London, Series A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
J. L. Doob, Renewal theory from the point of view of the theory of probability, Transactions of the American Mathematical Society 63(3):422–438, 1948. https://doi.org/10.1090/S0002-9947-1948-0025098-8

9 thms2 active usersReviewed

Operations Research Stochastic Systems·Captain: mikedeng1

Regenerative Stochastic Processes 4: Cumulative Processes on the Same Regeneration Points Are Jointly Asymptotically NormalResearch Paper

Motivation

Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time $t$ , the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.

Timeline:

1949. Feller proves the central limit theorem for the renewal counting process.
1952. Anscombe proves that a central limit theorem survives replacing the number of summands by a random index $m_t$ with $m_t/\psi(t)\to 1$ in probability, without independence between the index and the summands (Anscombe, Proc. Camb. Phil. Soc. 48, 1952).
1955. Smith extends Anscombe's theorem to random vectors and deduces the univariate (Theorem 9, Corollary 9·1) and multivariate (Theorem 10) central limit theorems for cumulative processes (Smith 1955).

Setting

On a probability space $(\Omega, P)$ , let $t_1, t_2, \dots$ be independent, identically distributed, non-negative random variables with $P\{t_1 = 0\} < 1$ (a renewal process), and $t_0 = 0$ . The regeneration epochs are $T_k = t_0 + t_1 + \dots + t_k$ ( $k \ge 0$ ), and $n_t$ is the number of epochs in $[0,t]$ (in Smith's words, the greatest $k$ with $T_{k-1} \le t$ , where $T_{-1} = 0$ ). Write $\mu_r = E t_1^r$ .

A real process $w_t$ with $w_0 = 0$ is a cumulative process if (C1) its cycle increments $y_n = \Delta_n w_t = w_{T_n} - w_{T_{n-1}}$ , $n \ge 1$ , are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process $\tilde w_t = \int_0^t |\mathrm d w_t|$ has increments $\tilde y_n = \Delta_n \tilde w_t$ . Moments are written $\kappa_r = E y_n^r$ and $\tilde\kappa_r = E \tilde y_n^{\,r}$ .

$M$ cumulative processes $w^{(1)}_t, \dots, w^{(M)}_t$ are based on the same sequence of regeneration points when the cycle vectors $(t_n, y^{(1)}_n, \dots, y^{(M)}_n, \tilde y^{(1)}_n, \dots, \tilde y^{(M)}_n)$ are i.i.d. in $n$ . Put $\kappa^{(i)}_1 = E y^{(i)}_1$ . The covariance matrices are

a_{kl} = \operatorname{cov}(y^{(k)}_1, y^{(l)}_1), \qquad b_{kl} = \operatorname{cov}\Big(y^{(k)}_1 - \tfrac{\kappa^{(k)}_1}{\mu_1} t_1,\; y^{(l)}_1 - \tfrac{\kappa^{(l)}_1}{\mu_1} t_1\Big).

Formalization targets

Goal: Theorem 10

If $\mu_1 < \infty$ and $E(\tilde y^{(i)}_1)^2 < \infty$ for every $i$ , then as $t \to \infty$

\left(\frac{w^{(i)}_t - \kappa^{(i)}_1 n_t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, a),

and if in addition $\mu_2 < \infty$ ,

\left(\frac{w^{(i)}_t - (\kappa^{(i)}_1/\mu_1)\,t}{(t/\mu_1)^{1/2}}\right)_{i=1}^M \xrightarrow{\ d\ } \mathcal N(0, b).

Milestones

The renewal strong law $n_t/t \to 1/\mu_1$ almost surely (§5·3).
Lemma 8: if $\mu_1 < \infty$ and $\tilde\kappa_p < \infty$ , then $(w_{t+Z_t} - w_t)/t^{1/p} \to 0$ almost surely, where $Z_t = \sum_1^{n_t+1} t_i - t$ .
Theorem B (Anscombe): $P\{\sum_1^{m_t} y_i/(\sigma\psi(t)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ for i.i.d. centred $y_i$ with variance $\sigma^2 > 0$ and $m_t/\psi(t) \to 1$ in probability.
Its $M$ -dimensional form (§5·4): $\psi(t)^{-1/2}\sum_1^{m_t} \mathbf y_j \xrightarrow{d} \mathcal N(0, a)$ for i.i.d. centred random vectors.
Theorem 9: if $E y_1 = 0$ and $\operatorname{var} y_1 = \sigma^2 > 0$ , then $P\{w_t/(\sigma(t/\mu_1)^{1/2}) \le \alpha\} \to \Phi(\alpha)$ .
Corollary 9·1: the univariate forms of both assertions of the goal, with normalisations $\sigma = (\kappa_2 - \kappa_1^2)^{1/2}$ and $\gamma = \operatorname{var}(y_1 - (\kappa_1/\mu_1)t_1)$ .

Significance

Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with $M = 2$ and the delta method gives the asymptotic normality of ratio estimators $w^{(1)}_t / w^{(2)}_t$ , the basis of the regenerative method of simulation output analysis. With $w_t = n_t$ , Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring $\kappa_1 n_t$ , needs only $\mu_1 < \infty$ , which matters for heavy-tailed cycle lengths.

The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.

Difficulty

The obvious argument writes $w_t$ as the sum of the first $n_t$ cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands $n_t$ is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on $n_t$ destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around $t/\mu_1$ , not at a single index. Second, the remainder over the incomplete cycle at time $t$ must be shown negligible on the scale $\sqrt t$ using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in $\mathbb R^M$ with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis $\sigma > 0$ can fail along some directions.

Formalization scope

Time is real; every limit is along $t \to \infty$ in $\mathbb R$ . Processes are functions $w : \mathbb R \to \Omega \to \mathbb R$ (or a family indexed by Fin M); cycle lengths are a sequence $\mathbb N \to \Omega \to \mathbb R$ with $t_0 = 0$ .
$n_t$ is a natural number, the number of epochs $T_j \le t$ ; on the null event where infinitely many epochs are $\le t$ it is $0$ . Finiteness is never assumed.
$\tilde w_t$ is the total variation (eVariationOn) of the path on $[0,t]$ , set to $0$ for all $t$ on paths of infinite variation, as Smith allows.
Condition (C1) is read for the whole cycle vector $(t_n, y_n, \tilde y_n)$ . No independence between components is assumed. Assuming the cycle length independent of the rewards, or the components independent, would make $a$ diagonal or force $b$ into a special form; that trivialization is ruled out.
"Jointly normally distributed with covariance matrix $a$ " is TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices $a$ and $b$ are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.
The scalar statements keep the paper's form: convergence of $P\{\cdot \le \alpha\}$ to $\Phi(\alpha) =$ cdf (gaussianReal 0 1) α for every real $\alpha$ . The paper's implicit $\sigma > 0$ and $\gamma > 0$ are explicit hypotheses; without them the quotients are $0$ in Lean and the statements would be false.
$\mu_1 < \infty$ , $\mu_2 < \infty$ and $E\tilde y^2 < \infty$ are Integrable hypotheses, never encoded through the value of an integral.

Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for $n_t$ and $\tilde w_t$ ; the Cramér–Wold step.

Selected references

W. L. Smith, Regenerative stochastic processes, Proc. R. Soc. Lond. A 232(1188):6–31, 1955. https://doi.org/10.1098/rspa.1955.0198
F. J. Anscombe, Large-sample theory of sequential estimation, Proc. Cambridge Philos. Soc. 48, 600, 1952 (cited in Smith 1955, p. 31).
W. Feller, Fluctuation theory of recurrent events, Trans. Amer. Math. Soc. 67, 98, 1949 (cited in Smith 1955, p. 31).
J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63, 422, 1948 (cited in Smith 1955, p. 31).

9 thms2 active usersReviewed

Machine Learning Statistics·Captain: mikedeng1

Empirical Bernstein Bounds and Sample Variance Penalization: Sample Variance Penalization Has Excess Risk at Most √(32V(f*,μ)ln(3M(n)/δ)/n) + 22ln(3M(n)/δ)/(n−1) (Theorem 15)Research Paper

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$ , but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.

Let $\mu$ be a probability distribution on a set $\mathcal X$ , and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$ . For $f\in\mathcal F$ , its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$ , with $X\sim\mu$ . For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$ , $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$ .

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$ , and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$ -balls centred in $A$ that cover $A$ . Then

\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).

For $\lambda\ge0$ , sample variance penalization selects

SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$ , $n\ge2$ , $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$ . With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$ ,

P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$ , so it covers an optimal one when one exists.

Milestones

In the order of the proof:

the fourth-moment inequality (Lemma 8, Corollary 9);
the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
the comparison $W\le\mathbb EV_n$ of (7)–(9);
Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
the uniform bound, Theorem 6:

\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$ ; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$ . The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$ -normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$ , and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
Indices $i=1,\dots,n$ are i : Fin n.
A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$ " have laws giving zero mass outside $[0,1]$ .
"With probability at least $1-\delta$ , $A$ " is written as $\mu^n\{\neg A\}\le\delta$ . For a set that is not measurable this is the outer measure.
$P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$ ).
$\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
$SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
- Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
- Lemma 13: the function is measurable.
- Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$ . With an infinite value the printed bound is vacuous.
Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$ . Theorem 3 and Bennett's display add $n\ge1$ . Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$ .
Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

SVP is not defined as the comparator $f^*$ .
$\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$ .
$V_n$ is the sample variance, not the true variance.
No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

the entropy method for self-bounding functions (Theorem 7);
Bennett's inequality for independent non-identical bounded variables;
product-measure symmetrization;
covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

21 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments I: An Optimal Assortment Always Consists of the k Most Popular Variants for Some kResearch Paper

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

(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)$ .
(8): under trend-following demand, stocking $\lambda$ exactly when $pq_j\ge c$ is optimal and the optimal profit is $\pi_T(S,v)$ .
Mangasarian (1969): a convex function divided by a positive affine function is quasiconvex.
Appendix: $g_I$ and $g_T$ are convex in $\delta$ on $[0,v_1]$ .
Lemma 1: $h_I$ and $h_T$ are quasi-convex on $[0,v_1]$ .
§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.

9 thms2 active usersReviewed

Combinatorics Markov Chain·Captain: mikedeng1

Coalescents With Multiple Collisions 1: A Coalescent on Partitions of ℕ With k-Fold Merger Rates λ_{b,k} Exists Iff λ_{b,k} = ∫ x^{k−2}(1−x)^{b−k} Λ(dx)Research Paper

Motivation

A coalescent models a collection of ancestral lineages merging as time runs backward. If every event joins exactly two lineages, a single pairwise merger rate describes the finite system. Pitman’s 1999 paper asks which rates permit an event to join any number of blocks, while still giving one process on partitions of all positive integers. This matters when a sample of any finite size must be a restriction of the same population model: specifying a chain separately at every sample size is insufficient unless the chains agree when labels are removed. The paper supplies an exact answer in terms of a finite measure on the unit interval. See Pitman (1999), Theorem 1 and §3.1.

Setting

Let $\mathcal P_n$ be the partitions of $[n]=\{1,\ldots,n\}$ and $\mathcal P_\infty$ the partitions of the positive integers. A partition records which labels belong to the same block. The map $R_n$ restricts a partition to $[n]$ . A partition $\pi$ refines $\pi'$ when every block of $\pi$ is contained in a block of $\pi'$ . Thus blocks can merge as time grows, but never split.

A $\mathcal P_\infty$ -valued process is a coalescent here when its paths refine with time and each finite restriction $R_n$ has right-continuous step-function paths. For a partition of $[n]$ with $b$ blocks, each unordered choice of $k$ blocks, $2\le k\le b$ , merges into one block at rate $\lambda_{b,k}$ . Different choices are different possible transitions, each with that rate; the rate is not multiplied by the number of choices. The finite chain’s generator $Q_n$ records these transition rates, with each diagonal entry the negative sum of the other entries in its row. Its transition matrix after time $t$ is $\exp(tQ_n)$ .

An array $(\lambda_{b,k})$ is consistent when, for every $n<m$ and every initial partition of $[m]$ , restricting the $m$ -label chain to $[n]$ gives the same process law as the $n$ -label chain started at the restricted partition. A finite nonnegative Borel measure $\Lambda$ on $[0,1]$ supplies a rate array through an integral. The point mass at zero is included: because $0^0=1$ for natural powers, it gives pairwise mergers while higher-order merger rates vanish. These definitions follow Pitman (1999), pp. 1871–1872 and Lemma 18.

Formalization targets

Characterization of admissible rates

The goal is the existence-and-rates part of Theorem 1. For every nonnegative array $(\lambda_{b,k}:2\le k\le b)$ , a coalescent with these finite-chain merger rates exists from every $\pi\in\mathcal P_\infty$ if and only if there is a finite nonnegative measure $\Lambda$ on $[0,1]$ such that

\lambda_{b,k}=\int_{[0,1]}x^{k-2}(1-x)^{b-k}\,\Lambda(dx) \qquad(2\le k\le b).

The statement asks for one measure representing every rate in the infinite array, and a process from every initial partition. It fixes neither a particular measure nor a sample size. This is Theorem 1, equation (1).

Supporting claims

The milestone list follows §3.1: adjacent-size restrictions suffice to check consistency; consistency is equivalent to

\lambda_{b,k}=\lambda_{b+1,k}+\lambda_{b+1,k+1} \qquad(2\le k\le b);

and the nonnegative normalized array relation

\mu_{i,j}=\mu_{i+1,j}+\mu_{i,j+1},\qquad \mu_{0,0}=1,

is equivalent to a representation $\mu_{i,j}=\mathbb E[X^i(1-X)^j]$ for $X\in[0,1]$ . The final milestone states the uniqueness as well as the existence of the representing measure: equation (1) is a bijection between consistent arrays and finite measures. These are the claims in Lemma 18 and its proof, p. 1882.

Significance

The characterization turns an infinite family of nonnegative rates into one finite measure, and says exactly when finite chains at different sample sizes can be restrictions of a common partition process. The bijection also makes the measure identifiable from the rates. Without consistency, a chain specified at one size can change its law when an unobserved extra label is added; there would be no single process on $\mathcal P_\infty$ with those restrictions.

Pitman proved these results in 1999. The mission concerns machine-checking their statements and, eventually, their proofs. The current Lean items are open theorems with compiled statements; they do not yet have machine-checked proofs. The reusable part of a complete development would include finite partition generators, restriction of continuous-time Markov chains, and the moment representation for normalized nonnegative arrays. These tools also apply to other consistent families of random combinatorial structures.

Difficulty

Checking that each $Q_n$ defines a finite-state chain does not by itself construct a process on partitions of all integers. Deleting one label can change which apparent merger occurs in the smaller chain, so the rates must satisfy a precise identity across adjacent sizes. Even once those identities hold, the conclusion requires one joint law whose finite restrictions agree for all sizes and times, with right-continuous paths. The representation step must recover a genuine finite measure, including possible mass at zero, and must prove uniqueness; a mere numerical fit for finitely many entries cannot establish the theorem.

Formalization scope

The Lean partition type is Setoid (Fin n) at finite size and a type synonym of Setoid ℕ at infinite size. The paper’s positive labels are shifted to zero-based labels, preserving their order. The measurable structure on infinite partitions is generated by pairwise equivalence coordinates, equivalently by finite restrictions; finite partition spaces use the discrete measurable structure. The process path predicate requires refinement at every pair of ordered times and right continuity of every finite restriction. Finite-chain laws are specified at all finite collections of times through $\exp(tQ_n)$ , so a process cannot qualify merely by having the right initial state or a single marginal.

The measure is represented on $\mathbb R$ with zero mass outside $[0,1]`; integrals are over$ [0,1] $. Finiteness is explicit, preventing a nonintegrable Bochner integral from acquiring Lean’s default value. Natural-number exponents retain$ x^0=1 $at$ x=0 $. The rate array is read only for$ 2\le k\le b$, and the zero measure is allowed. The Fin 0 restriction is an additional tautological boundary case introduced by Lean’s natural numbers. The process sample space is a small Lean type, and the law is a probability measure on it.

Only the characterization sentence of Theorem 1 is targeted. Its later assertions about the strong Markov property, Feller semigroup, Skorohod path-space law, and weak continuity of the law map are outside this mission. Contributions toward those properties would need further path-space infrastructure. The formalized foundations and milestones can also support the paper’s Poisson construction and its later results, but those are separate targets.

Selected references

Jim Pitman, Coalescents with multiple collisions, Annals of Probability 27(4), 1870–1902, 1999. DOI: 10.1214/aop/1022874819.

7 thms2 active usersReviewed

Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 2: Wendel's Formula E[exp(−λ/V_n)] = e^{−λ} φ_α(λ)^{n−1} ψ_α(λ)^{−n} for PD(α, 0)Research Paper

Motivation

A random discrete distribution is a random sequence of nonnegative numbers summing to $1$ . Ranked in decreasing order, $V_1\ge V_2\ge\cdots$ , such sequences model the relative sizes of species in a population, of cycles of a random permutation, of excursion intervals of a Markov process, and of atoms of random measures used as priors in Bayesian nonparametrics. The two-parameter Poisson–Dirichlet family $\mathrm{PD}(\alpha,\theta)$ is the main family of such laws; Pitman and Yor (Ann. Probab. 1997) derived its properties from a stable subordinator.

The special case $\mathrm{PD}(\alpha,0)$ , $0<\alpha<1$ , describes the ranked lengths of the excursion intervals of a stable( $\alpha$ ) subordinator's range, or of a Bessel process away from zero, up to time $1$ . A basic question about it is the law of a single ranked term $V_n$ . The answer goes through the Laplace transform of $1/V_n$ :

Darling (1952) found the characteristic function of the limit of $S_n/X_{(n,1)}$ (sum over maximum of i.i.d. heavy-tailed variables), which is that of $1/V_1$ .
Lamperti (1961) derived the corresponding Laplace transform from renewal theory, for $n=1$ .
Wendel (1964) obtained the transform for every $n\ge2$ from the range of a stable subordinator.
Pitman and Yor (1997), Proposition 11, explained the formula through an exact decomposition of $1/V_n$ into independent, infinitely divisible pieces.

Setting

Fix $0<\alpha<1$ . Let $\tilde Y_1,\tilde Y_2,\dots$ be independent, with $\tilde Y_n$ having the beta distribution $\mathrm{beta}(1-\alpha,n\alpha)$ on $(0,1)$ . Form the stick-breaking sequence $\tilde V_1=\tilde Y_1$ and $\tilde V_n=(1-\tilde Y_1)\cdots(1-\tilde Y_{n-1})\tilde Y_n$ for $n\ge2$ , and let $V_1\ge V_2\ge\cdots$ be its terms in decreasing order. The law of $(V_n)$ is $\mathrm{PD}(\alpha,0)$ (Definition 1 of the paper, with $\theta=0$ ).

From $(V_n)$ define $R_n=V_{n+1}/V_n$ , $A_0=0$ and, for $n\ge1$ ,

A_n=\frac{V_1+\cdots+V_n}{V_{n+1}},\qquad \Sigma_n=\frac{V_{n+1}+V_{n+2}+\cdots}{V_n}.

For $\lambda\ge0$ the paper's two Laplace exponents are

\phi_\alpha(\lambda)=\alpha\int_1^\infty e^{-\lambda x}x^{-\alpha-1}\,dx,\qquad \psi_\alpha(\lambda)=1+\alpha\int_0^1\left(1-e^{-\lambda x}\right)x^{-\alpha-1}\,dx,

and $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

The proof represents $(V_n)$ through a Poisson random measure (PRM) $\Lambda_\alpha$ on $(0,\infty)$ with $\Lambda_\alpha(x,\infty)=Cx^{-\alpha}$ : its ranked points $\Delta_1>\Delta_2>\cdots$ satisfy $X_n:=C\Delta_n^{-\alpha}=\varepsilon_1+\cdots+\varepsilon_n$ with $\varepsilon_i$ i.i.d. standard exponential, and $V_n=\Delta_n/\sum_m\Delta_m$ .

Formalization targets

Goal: Proposition 11

For every $n\ge1$ ,

\frac1{V_n}=1+A_{n-1}+\Sigma_n\quad\text{a.s.},

where (i) $A_{n-1}$ is distributed as the sum of $n-1$ independent copies of $A_1$ , with $E[e^{-\lambda A_{n-1}}]=\phi_\alpha(\lambda)^{n-1}$ ; (ii) $\Sigma_n$ is distributed as the sum of $n$ independent copies of $\Sigma_1$ , with $E[e^{-\lambda\Sigma_n}]=\psi_\alpha(\lambda)^{-n}$ ; (iii) $A_{n-1}$ and $\Sigma_n$ are independent.

Milestones

Proposition 10 (iii): $X_n=LV_n^{-\alpha}$ , with $L=\lim nV_n^\alpha$ , are the arrival times of a unit Poisson process, and $V_n=X_n^{-1/\alpha}/\sum_mX_m^{-1/\alpha}$ .
Lemma 24 (i)–(ii): $C\Delta_n^{-\alpha}$ is gamma $(n)$ ; the ratios $\Delta_i/\Delta_n$ , $i<n$ , are the order statistics of $n-1$ i.i.d. variables of density $\alpha x^{-\alpha-1}$ on $(1,\infty)$ , independent of $(\Delta_n,\Delta_{n+1},\dots)$ .
(66): $P(A_1\in dx)=\alpha x^{-\alpha-1}dx\,1(x>1)$ .
(67): $E[e^{-\lambda\Sigma_n}\mid\Delta_1,\dots,\Delta_n]=\exp\left(-\Delta_n^{-\alpha}\int_0^1(1-e^{-\lambda u})\Lambda_\alpha(du)\right)$ .
Proposition 8: the $R_n$ are independent and $R_n\sim\mathrm{beta}(n\alpha,1)$ .
(34): $\psi_\alpha(\lambda)=\Gamma(1-\alpha)\lambda^\alpha+\phi_\alpha(\lambda)$ .

Consequence: Corollary 12 (Wendel's formula)

E\left[\exp(-\lambda/V_n)\right]=e^{-\lambda}\,\phi_\alpha(\lambda)^{n-1}\,\psi_\alpha(\lambda)^{-n}\qquad(\lambda\ge0).

Significance

The result. Proposition 11 turns $1/V_n$ into the sum of the constant $1$ and two independent variables, each a sum of i.i.d. pieces with explicit Laplace exponents. Wendel's formula (38) is a one-line consequence, and since $1/V_n>0$ it determines the law of $V_n$ . The same decomposition is reused later in the paper: Proposition 26 combines (35) and (67) into a conditional form of (38) given $R_1,\dots,R_{n-1}$ and $X_n$ , which the paper uses in later calculations.

Formalizing it. All results here are proved in the paper; none is machine-checked. A formal proof needs the Poisson representation of $\mathrm{PD}(\alpha,0)$ (Proposition 10, itself resting on Perman–Pitman–Yor 1992), elementary but non-trivial facts about Poisson arrival times (gamma laws, order statistics, independence of ratios), and a conditional Laplace functional of a Poisson process. Each milestone is a self-contained target; Lemma 24 and (67) are statements about Poisson arrival times only and do not mention Poisson–Dirichlet laws.

Difficulty

The identity $1/V_n=1+A_{n-1}+\Sigma_n$ is algebra once $\sum_mV_m=1$ . The content is in the laws. On the stick-breaking side, the $V_n$ are the order statistics of a dependent sequence, and neither $A_{n-1}$ nor $\Sigma_n$ has an evident structure: the ranking destroys the independence of the $\tilde Y_n$ . The proof passes to the Poisson side, where the ranked points of a PRM have tractable conditional laws, and then must transport the conclusions back through a representation that holds only in distribution. Part (ii) requires a conditional computation (67) given $n$ points, followed by integration against a gamma law; part (iii) requires the mutual independence of all the ratios $R_n$ , an infinite family.

Formalization scope

The Lean development lives in namespace PoissonDirichlet.Wendel; its definitions file contains every object above.

Sequences are 0-based: V ω k is $V_{k+1}$ , Aseq (V ω) k is $A_k$ , Sigseq (V ω) k is $\Sigma_{k+1}$ , ratio (V ω) k is $R_{k+1}$ . Exponents $n-1$ and $n$ become k and k + 1.
$\mathrm{PD}(\alpha,0)$ is Definition 1 with $\theta=0$ . The law of $(\tilde Y_n)$ is a probability measure on sequences with independent coordinates of the stated beta laws. " $V$ has law $\mathrm{PD}(\alpha,0)$ " means $P(V\in s)$ equals the mass of the preimage of $s$ under the ranked stick-breaking map, for every measurable $s$ . Ranked values are defined with the extended cardinal Set.encard.
$A_n$ and $\Sigma_n$ are the $V$ -quotients of (31)–(32), not the $R$ -expressions; $\phi_\alpha,\psi_\alpha$ are the integrals (33)–(34), not Laplace transforms.
"Distributed as the sum of $m$ independent copies of $X$ " is equality with the $m$ -fold convolution power of the law of $X$ , the Dirac mass at $0$ when $m=0$ .
Every statement carries $0<\alpha<1$ except Lemma 24, which holds for all $\alpha>0$ .
The local time $L$ of (24) is a random variable with the hypothesis that $nV_n^\alpha\to L$ almost surely; this is its definition.
The PRM is used only through its ranked points, encoded by arrival times: $\Delta_n=(C/X_n)^{1/\alpha}$ with $X_n=\varepsilon_1+\cdots+\varepsilon_n$ , $\varepsilon_i$ i.i.d. standard exponential. This is the paper's own (27)–(28). In (67) the $\varepsilon_i$ are also assumed measurable, so that the conditioning $\sigma$ -algebra is a sub- $\sigma$ -algebra.
Lemma 24 (iii) is not stated; its only use is (67), which is stated. Corollary 12 states only the formula (38).

The formalization does not use Measure.map of a possibly non-measurable map in any definition: every equality of laws for such maps is stated through preimages. It does not use Set.ncard or limUnder. Every Laplace transform is the integral of a function with values in $(0,1]$ , and both exponent integrals are integrable under the stated parameter range, so no statement holds because an integral takes the junk value $0$ .

Useful infrastructure beyond this mission: arrival times of a Poisson process and their gamma and order-statistic laws; convolution powers of measures on $\mathbb R$ ; the Laplace functional of a Poisson random measure. Contributions of any of these as standalone lemmas are welcome.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Ann. Probab. 25(2):855–900, 1997. https://doi.org/10.1214/aop/1024404422
M. Perman, J. Pitman and M. Yor, Size-biased sampling of Poisson point processes and excursions, Probab. Theory Related Fields 92:21–39, 1992.
J. G. Wendel, Zero-free intervals of semi-stable Markov processes, Math. Scand. 14:21–34, 1964.
J. Lamperti, A contribution to renewal theory, Proc. Amer. Math. Soc. 12:724–731, 1961.
D. A. Darling, The influence of the maximum term in the addition of independent random variables, Trans. Amer. Math. Soc. 73:95–107, 1952.

9 thms2 active usersReviewed

Stochastic Systems·Captain: mikedeng1

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 1: Under PD(α, 0) the Ratios V_{n+1}/V_n Are Independent with beta(nα, 1) LawsResearch Paper

Motivation

Random partitions describe a population split into species, clusters, or types. If the species frequencies are put in decreasing order, the first frequency is the largest species, the second is the next largest, and so on. The Poisson–Dirichlet distribution gives a family of laws for these ranked frequencies. Its two parameters connect different random partition models, while the one-parameter case $\mathrm{PD}(\alpha,0)$ has a particularly direct description through ratios of neighboring frequencies. Pitman and Yor state that these ratios are independent and have explicit beta distributions, even though the ranked frequencies themselves have a complicated joint law (Pitman and Yor 1997, Proposition 8).

The result matters when a statistic of a random partition depends on the relative sizes of its largest components. A ratio $V_{n+1}/V_n$ describes the gap between two successive ranked species without requiring their total scale. An independent sequence of such ratios also gives a way to generate the entire ranked sequence. The paper records this converse immediately after Proposition 8 as Corollary 9 (Pitman and Yor 1997, p. 862).

Setting

Fix $0<\alpha<1$ . A beta $(a,b)$ distribution is a probability distribution on $(0,1)$ with density proportional to $x^{a-1}(1-x)^{b-1}$ . Let $\widetilde Y_n$ , for $n=1,2,\ldots$ , be independent beta $(1-\alpha,n\alpha)$ random variables. They break an initial mass of one into successive stick lengths

\widetilde V_n=\widetilde Y_n\prod_{i=1}^{n-1}(1-\widetilde Y_i).

Sort these lengths in decreasing order, counting repeated values separately, and write the resulting sequence as $V_1\geq V_2\geq\cdots$ . The law of this ranked sequence is $\mathrm{PD}(\alpha,0)$ , the $\theta=0$ case of Definition 1 in the paper (Pitman and Yor 1997, p. 857). The paper's broader definition takes $0\leq\alpha<1$ and $\theta>-\alpha$ , with beta $(1-\alpha,\theta+n\alpha)$ stick factors. This mission retains that general definition so later statements use the same object, but its theorems concern $\theta=0$ and $0<\alpha<1$ .

Define the adjacent ranked ratio $R_n=V_{n+1}/V_n$ . The source proves that the ranked masses are strictly positive almost surely under the Poisson–Dirichlet law, so these ratios have their ordinary probabilistic meaning (Pitman and Yor 1997, Proposition 2). The random sequence $R_1,R_2,\ldots$ is different from the independent stick factors $\widetilde Y_n$ : the latter are defined before ranking, whereas each $R_n$ compares consecutive masses after ranking.

Formalization targets

Goal: Proposition 8

For a sequence $(V_n)$ with $\mathrm{PD}(\alpha,0)$ law, the variables $R_n=V_{n+1}/V_n$ are mutually independent, and each has beta $(n\alpha,1)$ distribution. The equivalent cumulative distribution formula is part of the target:

\mathbb P(R_n\leq r)=r^{n\alpha}\qquad(n\geq1,\ 0\leq r\leq1).

The exponent and beta parameter use the paper's one-based $n$ . Independence concerns the full infinite family, rather than only pairs of ratios (Pitman and Yor 1997, Proposition 8, equations (21)–(22)).

Supporting targets

Proposition 10(i) establishes a local-time limit $L=\lim_{n\to\infty}nV_n^\alpha$ , both almost surely and in $L^p$ for every real $p\geq1$ . Proposition 10(iii) identifies the transformed sequence $X_n=LV_n^{-\alpha}$ with the arrival times of a unit-rate Poisson process: it has the joint law of partial sums of independent standard exponential variables. The proposition also recovers $V_n$ by normalizing $X_n^{-1/\alpha}$ . Finally, the proof of Proposition 8 states that consecutive Poisson arrival ratios $X_n/X_{n+1}$ are independent beta $(n,1)$ variables (Pitman and Yor 1997, pp. 862, 870). These are the three curated milestones. Corollary 9 is included as a companion: independent beta $(n\alpha,1)$ ratios, inserted into the paper's convergent series and finite products, produce a $\mathrm{PD}(\alpha,0)$ sequence.

Significance

Proposition 8 converts a statement about the order statistics of infinitely many dependent masses into an explicit product law for their ratios. It gives direct distributional information about every neighboring pair in a Poisson–Dirichlet partition. Together with Corollary 9, it specifies both how to read the ratios from a ranked partition and how to reconstruct a ranked partition from ratios. The formulas can therefore serve as a common interface for calculations and simulation involving $\mathrm{PD}(\alpha,0)$ (Pitman and Yor 1997, Propositions 8–10).

The mathematical results in this mission were proved in the 1997 paper; the open work here is a machine-checked Lean proof of their stated forms. Such a development would add reusable facts about infinite beta sequences, ranked stick lengths, Poisson arrival times, and their joint laws. The independent-arrival-ratio statement is useful beyond the Poisson–Dirichlet setting because its assumptions only concern standard exponential increments.

Difficulty

The stick factors are independent before their lengths are sorted, but sorting is a global operation: a particular ranked mass may have come from any stick index. Their independence therefore does not directly give independence of adjacent ranked ratios. Even a marginal calculation for one ratio does not establish mutual independence of the entire sequence. The local-time and arrival-time assertions in Proposition 10 encode the extra structure needed to state the joint result. The real technical burden is to relate the distribution obtained from ranked stick lengths to the distribution of an infinite Poisson arrival sequence, while retaining the almost-sure limits and normalization stated by the authors.

Formalization scope

Lean represents every sequence as a function $\mathbb N\to\mathbb R$ , with index $k=0$ denoting the paper's first index $n=1$ . stick implements equation (4); ranked defines the $(k+1)$ -st largest nonnegative length by upper-level-set cardinality, counted with multiplicity. It uses extended cardinality so an infinite upper-level set cannot be assigned cardinality zero. IsStickLaw records independence and the beta $(1-\alpha,\theta+(k+1)\alpha)$ coordinate laws. HasPD describes the distribution of the ranked stick sequence by probabilities of measurable preimages. This commits the mission to Definition 1 rather than a ratio construction of $\mathrm{PD}(\alpha,0)$ .

All mission theorems require $0<\alpha<1$ , and every source probability space is a probability measure. Ratios and negative real powers occur only as random quantities whose bases are positive almost surely under that law. Their exceptional values on null sets do not affect the distributional claims. The local time is identified by its almost-sure defining limit, rather than by a default value assigned when a limit fails. The $L^p$ clause uses the norm of the approximation error. The Poisson arrival law is stated jointly on measurable sets of infinite real sequences; it is not reduced to one-dimensional exponential marginals. These choices rule out vacuous interpretations through a nonmeasurable Measure.map, a finite-cardinality default on an infinite set, a junk integral, limUnder at a nonexistent limit, or a dropped parameter range.

The development needs Mathlib's beta and exponential measures, infinite product and independence APIs, measurable sequence spaces, real powers, infinite sums, and $L^p$ norms. Results about ranked values and arrival ratios would be reusable in later Poisson–Dirichlet missions. Contributions that establish these source statements at full strength, or their necessary measurable and summability infrastructure, fit the scope.

Selected references

J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator, Annals of Probability 25(2):855–900, 1997. DOI: 10.1214/aop/1024404422.

5 thms2 active usersReviewed

Completed

Captain: mikedeng1

Large Deviations of Sums of Independent Random Variables 1: The Fuk–Nagaev Inequality P(S_n ≥ x) ≤ ΣP(X_i > y_i) + P_4, P_5 or P_6 for Truncated Moments of Order t ≥ 2Research Paper

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

16 thms2 active usersReviewed

Machine Learning Operations Research Optimization·Captain: mikedeng1

A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand 2: Without a Bound on y^NV, Expanding-Projection AIM Has Regret ≤ max{b,h}(T^{δ−1/2} + T^{−1/2} + (y^NV)^{1+2/δ}/T)Research Paper

Motivation

A retailer who restocks a product every period must pick an order-up-to level without knowing the demand distribution. When a period ends with an empty shelf, the retailer records only its sales, so the true demand above the stock level is censored. The classical newsvendor solution, the critical fractile of the demand distribution, cannot be computed. Huh and Rusmevichientong (Math. Oper. Res., 2009) treat this as an online convex optimization problem: the expected one-period cost is convex in the stock level, and its derivative can be estimated without bias from the censored observation alone. Their Adaptive Inventory Management (AIM) algorithm is a projected stochastic subgradient method in the style of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). Its average expected cost converges to the newsvendor cost at rate $O(1/\sqrt T)$ .

That analysis assumes that the manager knows an upper bound $\bar y$ on the newsvendor quantity, and the algorithm projects onto $[0,\bar y]$ . This mission formalizes §3.1 of the paper, which removes the assumption. The projection interval grows with time, and the regret bound is explicit in the unknown newsvendor quantity. Earlier adaptive schemes for censored newsvendor problems include Godfrey and Powell (2001) and Burnetas and Smith (2000).

Setting

Periods are $t = 1, 2, \dots$ . Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with finite mean and distribution function $F$ . Inventory is perishable: every period starts empty, so the stock level is exactly the order-up-to level. With holding cost $h > 0$ per unit left over and shortage cost $b > 0$ per unit of unmet demand, the expected one-period cost at level $y \ge 0$ is

Q(y) = h\,E[y-D]^+ + b\,E[D-y]^+ .

The newsvendor quantity is $y^{NV} = \inf\{y \ge 0 : F(y) \ge b/(b+h)\}$ , the minimizer of $Q$ .

Write $\bar B = \max\{b,h\}$ and $P_{[0,a]}(z) = \max\{\min\{z,a\},0\}$ . After period $t$ , the manager observes whether demand fell short of the stock level and forms the signal

H_t(y) = \begin{cases} h, & D_t < y,\\ -b, & D_t \ge y.\end{cases}

Fix $\delta \in (0, 1/2)$ . The modified AIM algorithm starts from a level $\hat y^\delta_1 \in [0,1]$ and updates

\hat y^\delta_{t+1} = P_{[0,\,t^{\delta/2}]}\!\left(\hat y^\delta_t - \epsilon_t H_t(\hat y^\delta_t)\right), \qquad \epsilon_t = \frac{1}{\bar B\sqrt t}.

Neither the step size nor the projection interval uses any bound on $y^{NV}$ . The level $\hat y^\delta_t$ depends only on $D_1, \dots, D_{t-1}$ , and only through the censored observations.

Formalization targets

Goal: Theorem 7 (p. 11)

For every $\delta \in (0, 1/2)$ and every $T \ge 1$ ,

E\left[\frac1T\sum_{t=1}^T Q(\hat y^\delta_t)\right] - Q(y^{NV}) \le \max\{b,h\}\left[\frac{1}{T^{0.5-\delta}} + \frac{1}{T^{0.5}} + \frac{(y^{NV})^{1+2/\delta}}{T}\right].

The bound holds uniformly over all demand laws with finite mean. The price of not knowing $\bar y$ is the slower rate $T^{\delta - 1/2}$ and a transient term in which $y^{NV}$ enters polynomially.

Milestones (proof of Theorem 7, p. 12)

One-step inequality, the instance of Eq. (15) (Appendix A, p. 16) used in the proof. For each $t$ with $y^{NV} \le t^{\delta/2}$ ,

E[Q(\hat y^\delta_t) - Q(y^{NV})] \le \frac{E|\hat y^\delta_t - y^{NV}|^2}{2\epsilon_t} - \frac{E|\hat y^\delta_{t+1} - y^{NV}|^2}{2\epsilon_t} + \frac{\epsilon_t}{2} E|H_t(\hat y^\delta_t)|^2 .

Eq. (10): early rounds, where the projection interval has not yet reached $y^{NV}$ :

E\Big[\sum_{1 \le t \le T,\ t < (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\,(y^{NV})^{1+2/\delta}.

Eq. (11): late rounds:

E\Big[\sum_{1 \le t \le T,\ t \ge (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\, T^{0.5+\delta} + \bar B\, T^{0.5}.

Significance

The result. Theorem 7 shows that a distribution-free, censored-data policy can be asymptotically optimal without any prior bound on the optimal stock level. The only inputs are $b$ , $h$ and the tuning parameter $\delta$ . The explicit constant separates two effects. A transient cost grows with $y^{NV}$ and vanishes like $1/T$ . A steady-state rate $T^{\delta-1/2}$ approaches the known-bound rate $T^{-1/2}$ as $\delta \to 0$ , at the cost of a larger transient. The expanding-projection device applies to other stochastic subgradient methods whose feasible region is unbounded.

Formalizing it. The theorem is proved in the paper, but as far as is known it has no machine-checked proof. The mission produces the modified algorithm as an explicit function of the demand path, the per-step stochastic gradient inequality with a time-varying projection, and the two-phase regret decomposition. The per-step inequality with a varying domain is reusable for other growing-domain online methods.

Difficulty

The standard projected-gradient analysis compares every iterate with a fixed minimizer in a fixed compact set, and it bounds the telescoping distance terms by the diameter of that set. Neither applies here. In the early rounds the projection interval does not contain $y^{NV}$ , so the distance to $y^{NV}$ can grow from step to step. Once the interval contains $y^{NV}$ , the diameter that controls the telescoping sum grows with $t$ . The step sizes and the growing radii must be traded against each other through Abel summation. The bound on $E[H_t(\hat y^\delta_t)(\hat y^\delta_t - y^{NV})]$ needs the conditional-expectation argument that $H_t$ is an unbiased subgradient of $Q$ at a random point independent of $D_t$ . Applying the known-bound theorem with $\bar y$ replaced by $T^{\delta/2}$ does not work, because the algorithm is not given $T$ and the projection radius changes at every step.

Formalization scope

Demand: CappedBaseStock.DemandLaw (a probability law on $\mathbb R_{\ge 0}$ with finite and strictly positive mean) and the i.i.d. path demandPathLaw (Measure.infinitePi), from the published definition CappedBaseStock_Model. The path is zero-based: the paper's $D_t$ is coordinate $t-1$ . The positive-mean field is not needed by Theorem 7. It excludes only $D = 0$ almost surely.
$Q$ and $y^{NV}$ : backorderCost and newsvendorLevel from the published definition LostSalesOrderUpTo.Asymptotic.Backorder. Real levels are passed through Real.toNNReal, and the levels involved are always nonnegative.
The algorithm modAimTarget δ b h ŷ₁ d t is a deterministic recursion on the demand path, and expectations are Bochner integrals over the path measure. All integrands are bounded and measurable, so no non-integrability default enters.
Explicit readings of the paper's loose phrases:
- the first level, which the paper leaves unspecified, is assumed to satisfy $\hat y^\delta_1 \in [0,1]$ ; the theorem fails without it;
- $0 < b$ and $0 < h$ are assumed;
- the sums in (10) and (11) are restricted to $1 \le t \le T$ ;
- when $y^{NV} = 0$ , the sum in (11) starts at $t = 1$ ;
- all powers are real powers, with $0^p = 0$ for $p > 0$ ;
- "the manager does not know any upper bound" is not a hypothesis, because the algorithm uses none.
Trivializing formalizations are ruled out. The statements concern the algorithm's own iterates, not an arbitrary sequence of levels. The constants are the printed ones. The hypotheses are satisfiable, for example with $\hat y^\delta_1 = 0$ .
Useful contributions:
- convexity and Lipschitz continuity of $Q$ with constant $\max\{b,h\}$ ;
- the subgradient identity $E[H_t(y)] = (b+h)F(y^-) - b$ ;
- measurability and boundedness of the iterates;
- independence of $D_t$ from $\hat y^\delta_t$ under the product measure;
- the projected-step inequality.

Selected references

W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1), 2009. https://doi.org/10.1287/moor.1080.0355
M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
A. D. Flaxman, A. T. Kalai and H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
G. A. Godfrey and W. B. Powell, An Adaptive, Distribution-Free Algorithm for the Newsvendor Problem with Censored Demands, Management Science 47(8), 2001. https://doi.org/10.1287/mnsc.47.8.1101.10231
A. N. Burnetas and C. E. Smith, Adaptive Ordering and Pricing for Perishable Products, Operations Research 48(3), 2000. https://doi.org/10.1287/opre.48.3.436.12437

7 thms2 active usersReviewed

Missions

On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments II: Optimal Variety Rises with Price and Store Volume and Falls as the No-Purchase Preference VanishesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 1504)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Coalescents With Multiple Collisions 2: Coagulating an (α, θ) Partition by (β, θ/α) Equals Fragmenting an (αβ, θ) Partition by (α, −αβ)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 4: The Density of V_1 under PD(α, θ) Is Determined by the PD(α, α + θ) Law of V_1Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 19, identity (52)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Large Deviations of Sums of Independent Random Variables 3: For Centered Summands and x ≥ 2B_n, P(S_n ≥ x) ≥ ½ΣP(X_j ≥ 2x)Research Paper

Motivation

Setting

Formalization targets

Goal: the lower bound (p. 759, after (1.58))

Milestones (in the paper's order)

Significance

Difficulty

Formalization scope

Selected references

The Two-Parameter Poisson–Dirichlet Distribution Derived from a Stable Subordinator 3: Moments E_{α,θ}(V_n^p) of the n-th Largest PD(α, θ) Frequency as One Integral of φ_α and ψ_αResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 17

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Implicit Renewal Theory and Tails of Solutions of Random Equations 3: Rate of Approach — t^κP(R > t) Equals C₊ Minus a Contour Integral Plus O(t^{−β/2})Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Backward-Forward Stochastic Differential Equations 3: A Linear Backward-Forward System with Lipschitz Constant 1 Has No Solution on a Horizon T ≥ 1Research Paper

Motivation

Setting

Formalization targets

Main goal

Intermediate targets

Significance

Difficulty

Formalization scope

Selected references

Reflected Solutions of Backward SDE's, and Related Obstacle Problems for PDE's 2: With a Concave Coefficient, the Reflected BSDE Is the Value of a Minimax Optimal Stopping–Control ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7.2 (p. 725)

Milestones

Significance

Difficulty

Theorem 3.9: a single heat-operator estimate bounds $\alpha$