Stochastic Systems

Motivation

Measurements of Ethernet and Web traffic in the 1990s showed burstiness at every time scale, long-range dependence, and file sizes and transmission times with tails like $x^{-\alpha}$, $1<\alpha<2$ (Leland, Taqqu, Willinger and Wilson, 1994; Crovella and Bestavros, 1997). The standard explanation models each user as an ON/OFF source that alternates between transmitting at unit rate and staying silent, with heavy-tailed period lengths. Many such sources are superposed and time is rescaled. Taqqu, Willinger and Sherman (1997) showed that the limit is fractional Brownian motion when the number of sources is sent to infinity first. That limit is the basis of Gaussian queueing models of network buffers.

Mikosch, Resnick, Rootzén and Stegeman (2002) asked what happens when the number of sources $M$ and the time scale $T$ grow together. The answer depends on how fast $M=M(T)$ grows. Under fast growth the limit is fractional Brownian motion; this is Theorem 4 of the paper and a separate mission. Under slow growth the limit is an α-stable Lévy motion: it has independent increments and infinite variance, and its sample paths jump. This mission formalizes the slow growth result, Theorem 2. The two answers lead to different buffer and dimensioning models, so the dichotomy matters for traffic engineering.

Setting

Period laws. ON-periods have law $F_{\mathrm{on}}$ and OFF-periods have law $F_{\mathrm{off}}$; both are laws of non-negative random variables. Their means are $\mu_{\mathrm{on}}$ and $\mu_{\mathrm{off}}$, and $\mu=\mu_{\mathrm{on}}+\mu_{\mathrm{off}}$. Their right tails $\bar F=1-F$ satisfy (2.1)–(2.2):

$$\bar F_{\mathrm{on}}(x)=x^{-\alpha}L_{\mathrm{on}}(x),\qquad \bar F_{\mathrm{off}}(x)=x^{-\alpha_{\mathrm{off}}}L_{\mathrm{off}}(x),\qquad 1<\alpha<\alpha_{\mathrm{off}}<2,$$

where $L_{\mathrm{on}}$ and $L_{\mathrm{off}}$ are slowly varying: $L(cx)/L(x)\to1$ for every $c>0$. The ON-periods therefore have the heavier tail.

One source. Let $X_1,X_2,\dots$ be iid $F_{\mathrm{on}}$ and $Y_{\mathrm{off}},Y_1,Y_2,\dots$ iid $F_{\mathrm{off}}$. Let $B$ be Bernoulli with $P(B=1)=\mu_{\mathrm{on}}/\mu$. Let $X^{(0)}_{\mathrm{on}}$ and $Y^{(0)}_{\mathrm{off}}$ have the integrated-tail laws $F^{(0)}(x)=\mu_F^{-1}\int_0^x\bar F(s)\,ds$. All of these variables are independent. Put $Z_i=X_i+Y_i$. The delay is $T_0=B(X^{(0)}_{\mathrm{on}}+Y_{\mathrm{off}})+(1-B)Y^{(0)}_{\mathrm{off}}$, and the renewal epochs are $T_n=T_0+\sum_{i=1}^nZ_i$. The source is ON at time $t$ when

$$W_t=B\,\mathbf 1_{[0,X^{(0)}_{\mathrm{on}})}(t)+\sum_{n\ge0}\mathbf 1_{[T_n,T_n+X_{n+1})}(t)=1 .$$

This construction makes $W$ stationary.

Superposition. $M$ iid sources $W^{(1)},\dots,W^{(M)}$ feed a server. $N(t)=\sum_mW^{(m)}_t$ is the number of active sources, and $A(t)=\int_0^tN(s)\,ds$ is the cumulative input; its mean is $EA(t)=M\mu^{-1}\mu_{\mathrm{on}}t$.

Growth. $b(t)=(1/\bar F_{\mathrm{on}})^{\leftarrow}(t)$ is the quantile function (2.9). $M=M(T)$ is integer valued, non-decreasing and tends to infinity. Slow Growth Condition 1 is $b(MT)/T\to0$.

Stable laws. $S_\alpha(\sigma,\beta,\mu)$ is the law with characteristic function $\exp\{-\sigma^\alpha|\theta|^\alpha(1-i\beta\,\mathrm{sign}(\theta)\tan\frac{\pi\alpha}2)+i\mu\theta\}$ for $\alpha\neq1$. The α-stable Lévy motion $X_{\alpha,\sigma,\beta}$ has independent stationary increments, and $X(t)\sim S_\alpha(\sigma t^{1/\alpha},\beta,0)$.

Formalization targets

Goal: Theorem 2 (p. 40)

With $C_\alpha=\dfrac{1-\alpha}{\Gamma(2-\alpha)\cos(\pi\alpha/2)}$, $\sigma=C_\alpha^{-1/\alpha}$ and $c=\mu_{\mathrm{off}}/\mu^{1+1/\alpha}$, under Condition 1

$$\frac{A(T\cdot)-TM\mu^{-1}\mu_{\mathrm{on}}(\cdot)}{b(MT)}\xrightarrow{\ fidi\ }c\,X_{\alpha,\sigma,1}(\cdot).$$

Every constant is stated as printed. The normalisation is the paper's $b(MT)$ and the limit is the totally skewed ($\beta=1$) Lévy motion.

Milestones (§5, in the order of the proof)

• Lemmas 3 and 6: the initial ON-periods ($A_1$) and the overshoots beyond $T$ ($A_3$) are negligible at scale $b(MT)$.
• Lemmas 4 and 5: the per-source renewal count $\xi_T$ concentrates around $\mu_T=T/\mu$ with probability $1-o(1/M)$, plus a truncated-overshoot bound.
• Lemmas 7, 8 and 9: the left tails of the centred sums $S_n=\sum_{k\le n}J_k$ are negligible, and replacing $\xi_T$ by $[\mu_T]$ is harmless. Here $J_k=r_{\mathrm{on}}(X_k-\mu_{\mathrm{on}})-r_{\mathrm{off}}(Y_k-\mu_{\mathrm{off}})$.
• Lemma 10: $[b(MT)]^{-1}A_{21}\to cX_{\alpha,\sigma,1}(1)$ in distribution.
• Lemmas 11 and 12: tails of linear combinations of increments, and the two-dimensional limit.

Significance

Theorem 2 identifies the limit regime where the Gaussian heavy-traffic picture fails for ON/OFF traffic. When few sources are observed over long horizons, the aggregate input has infinite-variance, independent-increment fluctuations of size $b(MT)\approx(MT)^{1/\alpha}$. Read together with Theorem 4, the result says the growth rate of $M$ relative to $T$ decides between the two classical models of network input. The proof turns the ON/OFF superposition into row-wise iid random sums and uses a heavy-tailed large-deviation estimate for random walks (Cline and Hsing). That technique carries over to other renewal-reward processes with regularly varying rewards.

The result is proved in the paper. No machine-checked version exists, either of the theorem or of the probabilistic substrate it rests on. Formalization would produce:

• a stationary alternating renewal process in Lean;
• a usable notion of regular variation with the quantile function $b$;
• stable laws given by characteristic functions;
• the infinitely divisible convergence criterion (Petrov's conditions (A)–(C)) that the proof cites for row-wise iid sums.

Correction. Lemma 12 as printed omits the normalisation $[b(MT)]^{-1}$ on its left-hand side. Its proof and its use in Theorem 2 both have it, and without it the claim fails because the left-hand side grows. The mission states Lemma 12 with the normalisation. Lemma 11's upper summation limits $\mu_{Tt}$ are read as integer parts, as elsewhere in §5.

Difficulty

The natural first idea is to treat $A(T)$ as a sum of $M$ iid terms and apply the stable central limit theorem for triangular arrays. This fails as stated: each source's contribution $A^{(m)}(T)$ is itself a random sum $\sum_{k\le\xi_T}X_k$, and its count $\xi_T$ depends strongly on the $X_k$. Moreover, $M$ grows too slowly for a law-of-large-numbers smoothing across sources. The count must be replaced by its mean simultaneously for all $M$ sources, with an error probability $o(1/M)$, uniformly as $T\to\infty$. This requires the two-sided large-deviation estimate of Lemma 4. Its lower tail rests on the Cline–Hsing asymptotics $P(S_n>x)\sim n\bar F(x)$ for heavy-tailed random walks; its upper tail rests on a Cramér bound. Then Petrov's conditions must be checked at the exact scale $b(MT)$. That needs Potter bounds for the slowly varying factors and a non-uniform Berry–Esseen estimate for the truncated sums. None of these tools is in Mathlib.

Formalization scope

All declarations are in the namespace NetTraffic.OnOffStable, in one definitions file.

Conventions.

• Each time scale $T$ has its own probability space $(\Omega_T,P_T)$, which carries $M(T)$ independent sources indexed $0,\dots,M(T)-1$. Only laws matter, and the statements quantify over every such family.
• Lean's X n and Y n are the paper's $X_{n+1}$ and $Y_{n+1}$.
• $\xi_T$ is a Set.ncard (junk $0$ on a null event). $W$ is a tsum of indicators, and $A$ is an interval integral.
• $b(t)=\inf\{x>0:t\bar F_{\mathrm{on}}(x)\le1\}$. This set is non-empty for $t>0$, so $b$ is never the junk value $0$, and $b(MT)/T\to0$ is a real condition.
• $L_{\mathrm{on}}(x)=x^\alpha\bar F_{\mathrm{on}}(x)$ is assumed slowly varying, which is equivalent to (2.1).
• Fidi convergence is stated with sorted times: for each $k$ there is a probability measure on EuclideanSpace ℝ (Fin k) whose characteristic function is that of $c(X(t_1),\dots,X(t_k))$, and the laws of the normalised input vectors converge weakly to it. The characteristic function pins the limit down. Its existence is part of the claim, because Mathlib has no stable laws.
• Convergence in probability means $P_T(|Y_T|>\eta)\to0$ for every $\eta>0$.
• The lemmas that use $EA_3$ and $E X_{\xi_T}\mathbf 1[\cdot]$ also assert integrability, so Bochner junk values cannot trivialise them.

Ruled out. None of the following is acceptable: an encoding in which $b$, $N$ or $A$ collapses to a junk value; a model hypothesis that no family satisfies (the period laws must be genuine probability laws with finite means, which holds because $\alpha>1$); a limit "law" not pinned by its characteristic function; or convergence of one-dimensional laws only.

Needed infrastructure.

• Regular variation: Karamata's theorem and Potter bounds (Proposition 2, App. B).
• Large deviations for heavy-tailed random walks (Corollary 1, App. A).
• Renewal theory for delayed alternating renewal processes.
• Stable laws and the convergence criterion for row-wise iid sums.

The regular-variation and stable-law layers are reusable well beyond this mission. Formalizations of any milestone, of those general tools, or of alternative proofs of the one-dimensional limit are welcome.

Selected references

• T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman, Is network traffic approximated by stable Lévy motion or fractional Brownian motion?, Ann. Appl. Probab. 12(1):23–68, 2002. https://doi.org/10.1214/aoap/1015961155
• M. S. Taqqu, W. Willinger and R. Sherman, Proof of a fundamental result in self-similar traffic modeling, Computer Communication Review 27:5–23, 1997. https://doi.org/10.1145/251007.251012
• W. E. Leland, M. S. Taqqu, W. Willinger and D. V. Wilson, On the self-similar nature of Ethernet traffic (extended version), IEEE/ACM Trans. Networking 2(1):1–15, 1994. https://doi.org/10.1109/90.282603
• M. E. Crovella and A. Bestavros, Self-similarity in World Wide Web traffic: evidence and possible causes, IEEE/ACM Trans. Networking 5(6):835–846, 1997. https://doi.org/10.1109/90.650143
• D. B. H. Cline and T. Hsing, Large deviation probabilities for sums of random variables with heavy or subexponential tails, Technical report, Texas A&M University, 1991.
• G. Samorodnitsky and M. S. Taqqu, Stable Non-Gaussian Random Processes, Chapman and Hall, 1994. https://doi.org/10.1201/9780203738818

Why heavy-tailed input matters

Measurements of Ethernet and Internet traffic in the 1990s showed that cumulative traffic is self-similar and long-range dependent: correlations of the input rate decay so slowly that they are not summable, and fluctuations at large time scales do not average out the way Poisson-type models predict. A widely accepted explanation is that the lengths of individual transmissions (file sizes, session durations) are heavy tailed, with infinite variance. Queueing and capacity-planning calculations then depend on which stochastic process approximates the cumulative input over long horizons.

Two candidate approximations had been proposed: fractional Brownian motion, a Gaussian self-similar process with dependent increments (Taqqu, Willinger and Sherman, 1997; Leland, Taqqu, Willinger and Wilson, 1994), and α-stable Lévy motion, a heavy-tailed process with independent increments. Mikosch, Resnick, Rootzén and Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both arise from the same model, and that the answer depends on how fast the connection rate grows relative to the time scale. This mission formalizes their Gaussian answer for the infinite source Poisson model: Theorem 3.

• 1994–1997: Leland et al. measure self-similarity in Ethernet traffic; Willinger, Taqqu, Sherman and Wilson derive fractional Brownian motion from ON/OFF sources with heavy-tailed periods, in an iterated limit (first the number of sources, then time).
• 2002: Mikosch, Resnick, Rootzén and Stegeman take both limits simultaneously and identify a slow-growth regime (stable Lévy limit) and a fast-growth regime (fractional Brownian limit), for both the ON/OFF and the infinite source Poisson model.

The infinite source Poisson model

Connections start at the points $(\Gamma_k)_{k\in\mathbb Z}$ of a homogeneous Poisson process on $\mathbb R$ with rate $\lambda$, labelled so that $\Gamma_0<0<\Gamma_1$; equivalently, $-\Gamma_0$, $\Gamma_1$ and $\Gamma_{k+1}-\Gamma_k$ ($k\neq0$) are iid exponential with parameter $\lambda$. Connection $k$ transmits at unit rate for a length $X_k$; the $X_k$ are iid with law $F_{\mathrm{on}}$ on $[0,\infty)$ and independent of $(\Gamma_k)$. The tail $\bar F_{\mathrm{on}}(x)=P(X_k>x)$ is regularly varying:

$$\bar F_{\mathrm{on}}(x)=x^{-\alpha}L(x),\qquad x>0,\quad 1<\alpha<2,\tag{2.8}$$

with $L$ slowly varying ($L(cx)/L(x)\to1$ for every $c>0$). The mean $\mu_{\mathrm{on}}$ is finite and the variance infinite. The number of active connections and the cumulative input are

$$N(t)=\sum_k\mathbf 1[\Gamma_k\le t<\Gamma_k+X_k],\qquad A(t)=\int_0^tN(s)\,ds .$$

The model is indexed by a time scale $T\to\infty$, with a connection rate $\lambda=\lambda(T)$ that is non-decreasing in $T$. With the quantile function $b(t)=(1/\bar F_{\mathrm{on}})^{\leftarrow}(t)=\inf\{x>0:1/\bar F_{\mathrm{on}}(x)\ge t\}$, the fast growth Condition 2 is

$$\lim_{T\to\infty}\frac{b(\lambda T)}{T}=\infty ,$$

equivalently $\lambda T\bar F_{\mathrm{on}}(T)\to\infty$: many transmissions longer than the observation window start in it. With $\sigma_T^2(1)=\lambda T^3\bar F_{\mathrm{on}}(T)$ the normalised input is

$$G_T(t)=\frac{A(Tt)-\lambda\mu_{\mathrm{on}}Tt}{[\sigma_T^2(1)\,\sigma^2]^{1/2}},\qquad t\ge0 .$$

Standard fractional Brownian motion $B_H$ with Hurst index $H\in(0,1)$ is a mean-zero Gaussian process on $[0,\infty)$ with a.s. continuous paths and $\mathrm{Cov}(B_H(t),B_H(s))=\tfrac12\big(t^{2H}+s^{2H}-|t-s|^{2H}\big)$.

Formalization targets

Goal: Theorem 3 (corrected)

Under (2.8), $\lambda$ non-decreasing and Condition 2,

$$G_T(\cdot)\xrightarrow{d}B_H(\cdot)\quad\text{in }(\mathbb D[0,\infty),J_1),\qquad H=\frac{3-\alpha}2,\qquad \sigma^2=\frac{2}{(\alpha-1)(2-\alpha)(3-\alpha)} .$$

On the constant. The paper takes $\sigma^2$ from its display (6.6), $\sigma^2=\frac1{3-\alpha}\big[\frac{\alpha}{2-\alpha}+\frac2{\mu_{\mathrm{on}}}\big]$. With that value the theorem is false. Two terms are lost in the variance bookkeeping of the proof: (6.4) omits the factor $\lambda m_2\sim\lambda m_3\sim\lambda\mu_{\mathrm{on}}$ in the variances of the second and third regional sums, each of which contributes $1/(3-\alpha)$, and (6.2) discards $(P_4-EP_4)T$ by an argument valid only under slow growth; under Condition 2 its variance is $\sim\lambda T^3\bar F_{\mathrm{on}}(T)/(\alpha-1)$. The sum $\frac{\alpha}{(2-\alpha)(3-\alpha)}+\frac2{3-\alpha}+\frac1{\alpha-1}$ equals $\frac2{(\alpha-1)(2-\alpha)(3-\alpha)}$, which is also what $\mathrm{Var}A(T)=2\int_0^T(T-h)\,\lambda\int_h^\infty\bar F_{\mathrm{on}}(v)\,dv\,dh$ and Karamata's theorem give. Since $\mathrm{Var}B_H(1)=1$, only this value makes the limit standard. All other constants are those of the paper.

Intermediate targets

The milestones follow the proof: Lemma 1 (Condition 2 ⇔ $\lambda T\bar F_{\mathrm{on}}(T)\to\infty$ ⇔ $\mathrm{Cov}(N_T(0),N_T(T))\to\infty$), Lemma 2 (fast part), the covariance identity (2.14), the moment asymptotics (4.9) and (4.14), the central limit theorem (6.3) for the first regional sum, the one-dimensional limit (6.5) with the corrected variance, stationarity of the increments of $G_T$, and the fourth-moment bounds (6.8) and $E(G_T(t+u)-G_T(t))^4\le cu^2$ that give tightness.

Significance

The theorem identifies the fast-growth regime of the infinite source Poisson model (the M/G/∞ input model) with fractional Brownian motion, so that Gaussian long-range-dependent models of network traffic are limits of a mechanistic model, not postulates; together with Theorem 1 it shows that the choice between Gaussian and stable approximations is decided by a single growth condition, $b(\lambda T)/T\to0$ or $\to\infty$. Queueing analyses of fluid queues fed by fractional Brownian motion inherit their justification from limits of this kind.

The result is proved in the paper, apart from the constant discussed above; it is not formalized anywhere. A formalization adds a machine-checked statement with the correct normalisation and a reusable development of regularly varying tails, Poisson marked point processes on $\mathbb R\times[0,\infty)$, fractional Brownian motion, and Skorokhod's $J_1$ topology on $\mathbb D[0,\infty)$.

Difficulty

The obvious argument is a central limit theorem for $A(T)$, but $A(T)$ is not a sum of independent terms of bounded variance: transmissions that straddle the window are long and heavy tailed, and their contribution is of the same order as the bulk. The proof splits the points into four regions according to where a transmission starts and ends, and each region needs its own moment asymptotics through Karamata's theorem; the bookkeeping is exactly where the printed constant goes wrong. The functional statement then needs tightness in $\mathbb D[0,\infty)$: a fourth-moment bound on increments that is uniform in $T$ and in the position of the increment, which requires Potter-type bounds on $\bar F_{\mathrm{on}}(uT)/\bar F_{\mathrm{on}}(T)$ for small $u$. Convergence of finite-dimensional distributions alone does not give the theorem.

Formalization scope

• Time and models. $T\to\infty$ along atTop on $\mathbb R$. Each model $T$ has its own probability space; the theorems hold for every family of models with the stated rate and length law. Time in $G_T$ runs over $\mathbb R_{\ge0}$.
• Standing hypotheses. $F_{\mathrm{on}}$ is a probability measure with $F_{\mathrm{on}}((-\infty,0))=0$ (lengths are non-negative, implicit on the page); (2.8) is stated as "$x\mapsto x^\alpha\bar F_{\mathrm{on}}(x)$ is slowly varying", $1<\alpha<2$; $\lambda(T)>0$ and $\lambda$ is non-decreasing (§3.1); Condition 2. No other hypothesis is added.
• Junk values ruled out. $b$ is an infimum over $\{x>0:t\bar F_{\mathrm{on}}(x)\le1\}$, never a division by zero; $N$ is a cardinality and $A_1$ a sum of non-negative terms, whose junk values ($0$ on an infinite set) occur only on null events; fourth moments are asserted together with integrability; equalities of laws are asserted together with measurability. The limit is pinned completely: Gaussian, mean zero, the covariance above with $\sigma_H=1$, $H=(3-\alpha)/2$, continuous paths. Fidi convergence in place of the functional limit, a free scale in the limit, or a limit identified only by its marginals would each be a different, weaker theorem.
• Weak convergence is stated in coupling form: for every sequence $T_n\to\infty$ there is one probability space with copies $Y_n$ of the laws of $G_{T_n}$ (all finite-dimensional distributions) and a standard fractional Brownian motion $Y'$ such that $Y_n\to Y'$ in $J_1$ almost surely, càdlàg paths included. On the Polish space $\mathbb D[0,\infty)$ this is equivalent to weak convergence. Because $A(T\cdot)$ and $B_H$ have continuous paths, $J_1$ convergence here coincides with locally uniform convergence.
• Infrastructure needed: Karamata's theorem and Potter bounds for regularly varying functions; the Poisson random measure of the marked points and its restriction to disjoint regions; a Lyapunov central limit theorem for Poisson sums; fractional Brownian motion and its existence; Billingsley's moment criterion for tightness in $\mathbb D[0,K]$. The regular-variation and Skorokhod-space material is reusable well beyond this mission; contributions of any of these pieces, and of any milestone, are welcome.

Selected references

• T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman, Is network traffic approximated by stable Lévy motion or fractional Brownian motion?, Ann. Appl. Probab. 12(1) (2002), 23–68. https://doi.org/10.1214/aoap/1015961155
• W. E. Leland, M. S. Taqqu, W. Willinger and D. V. Wilson, On the self-similar nature of Ethernet traffic (extended version), IEEE/ACM Trans. Networking 2 (1994), 1–15. https://doi.org/10.1109/90.282603
• W. Willinger, M. S. Taqqu, R. Sherman and D. V. Wilson, Self-similarity through high-variability: statistical analysis of Ethernet LAN traffic at the source level, IEEE/ACM Trans. Networking 5 (1997), 71–86. https://doi.org/10.1109/90.554723
• N. H. Bingham, C. M. Goldie and J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 12.3, moment criterion for tightness).

Motivation

Asset prices observed at high frequency show two kinds of discontinuity: jumps in the price itself and abrupt changes in its volatility. Whether the two occur at the same times matters for modelling. Many stochastic volatility models used in option pricing let the price and the volatility jump together (for example the affine jump-diffusion models of Duffie, Pan and Singleton, Econometrica 2000), while others make them jump independently or not at all, and the choice affects pricing, hedging and risk management. Jean Jacod and Viktor Todorov (Do price and volatility jump together?, Ann. Appl. Probab. 20 (2010)) built statistical tests of this question that use only discretely observed prices. The tests rest on a law of large numbers, Theorem 3.1 of the paper, and this mission formalizes it.

Setting

The price is an Itô semimartingale $X$ on a filtered probability space $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},\mathbb P)$:

$$X_t=X_0+\int_0^t b_s\,ds+\int_0^t\sigma_s\,dW_s+\int_0^t\!\!\int_E\delta(s,z)1_{\{|\delta(s,z)|\le1\}}(\mu-\nu)(ds,dz)+\int_0^t\!\!\int_E\delta(s,z)1_{\{|\delta(s,z)|>1\}}\mu(ds,dz),$$

where $W$ is a Brownian motion, $\mu$ is a Poisson random measure on $\mathbb R_+\times E$ with compensator $\nu(ds,dz)=ds\otimes\lambda(dz)$, and $\delta(\omega,s,z)$ is the jump size produced by an atom $(s,z)$ of $\mu$. The volatility is $c_t=\sigma_t^2$, and $\Delta X_s=X_s-X_{s-}$ is the jump of $X$ at time $s$.

Two assumptions are imposed. (H-$r$), $0\le r<2$: the drift $b$ is locally bounded, $\sigma$ is càdlàg with $\sigma_t\ne0$ and $\sigma_{t-}\ne0$, and $|\delta(\omega,t,z)|\le\Gamma_t(\omega)\gamma(z)$ with $\Gamma$ locally bounded and $\int_E(\gamma^r\wedge1)\,d\lambda<\infty$; smaller $r$ means fewer small jumps, and $r=0$ means finitely many jumps on bounded intervals. (K-$v$), $0<v\le1$: $\sigma_t=\Sigma(Z_t,\overline Z_t)$ for a $C^1$ function $\Sigma$, where $Z$ is itself an Itô semimartingale with controlled jumps and $\overline Z$ is Hölder of order $v$ in the sense $|\overline Z_{t+s}-\overline Z_t|\le\Gamma'_{t+s}s^v$ for $0<s\le1$.

For a test function $F(x,y,z)$, the unobservable target is the jump functional

$$U(F)_t=\sum_{s\le t}F(\Delta X_s,c_{s-},c_s)\,1_{\{\Delta X_s\ne0\}},$$

which compares, at each price jump, the volatility just before and just after it. The data are the values $X_{i\Delta_n}$ on a grid of mesh $\Delta_n\to0$, with increments $\Delta^n_iX=X_{i\Delta_n}-X_{(i-1)\Delta_n}$. With a truncation level $u_n$ and a window size $k_n$, the local volatility estimator is

$$\widehat c(k_n)_i=\frac1{k_n\Delta_n}\sum_{j=1}^{k_n}|\Delta^n_{i+j}X|^2\,1_{\{|\Delta^n_{i+j}X|\le u_n\}},$$

and the observable statistic is

$$U(F,k_n)_t=\sum_{i=k_n+1}^{[t/\Delta_n]-k_n}F\big(\Delta^n_iX,\widehat c(k_n)_{i-k_n-1},\widehat c(k_n)_i\big)\,1_{\{|\Delta^n_iX|>u_n\}}.$$

The tuning (3.3) is $u_n\asymp\Delta_n^{\varpi}$ and $k_n\asymp\Delta_n^{-\rho}$ with $0<\varpi<\tfrac12$ and $0<\rho<1$. Finally, $\mathcal R$ is the family of open sets $R\subseteq\mathbb R$ with finite complement that contain every value $x$ with $\mathbb P(\exists s>0:\Delta X_s=x)>0$.

Formalization targets

Goal: Theorem 3.1

Let $F$ be Borel, continuous at each point of $R\times(0,\infty)^2$ for some $R\in\mathcal R$, and assume one of (a) $F(x,y,z)=0$ for $|x|\le\varepsilon$; (b) $r=0$; (c) $|F(x,y,z)|\le K|x|^r(1+y+z)$ for $|x|\le\varepsilon$. Then $U(F)$ is a.s. well defined and

$$U(F,k_n)\xrightarrow{\ \mathbb P\ }U(F)\qquad\text{for the Skorokhod topology}.$$

Milestones

They follow the proof of §8, in which the coefficients are bounded by a constant (the localized bound (8.3)):

• (8.4): with probability tending to one, the big jumps up to time $t$ lie in distinct sampling windows;
• (8.11) and (8.14): $\mathbb E(|\Delta^n_iX|^2\mid\mathcal F_{(i-1)\Delta_n})\le K\Delta_n$ and $\mathbb E(\widehat c(k_n)_i\mid\mathcal F_{i\Delta_n})\le K$, with $K$ uniform;
• Lemma 8.1, (8.18): $\widehat c(k_n)_i\to c_S$ and $\widehat c(k_n)_{i-k_n-1}\to c_{S-}$ in probability on the events where no big jump falls in the corresponding window;
• (8.27): the part of $U(F,k_n)$ carried by the big jumps converges to the corresponding part of $U(F)$;
• (8.29): the remainder driven by the small jumps vanishes in mean, uniformly in $n$, as the jump threshold goes to zero;
• Theorem 3.1 under the localized bound (8.3), which §8.4 proves directly.

Significance

Theorem 3.1 makes $U(F,k_n)_T$ a consistent estimator of $U(F)_T$. Choosing $F$ nonnegative with $F(x,y,y)=0$ makes $U(F)_T>0$ exactly when $X$ and $c$ jump together on $[0,T]$, and the tests of §4 of the paper (Theorems 4.1–4.5), together with the central limit theorems 3.2 and 3.3, are built on this. The same truncated local volatility estimators appear throughout high-frequency econometrics, so their consistency (Lemma 8.1) is reusable on its own.

The result is proved in the paper. No machine-checked proof of it, or of any of its steps, is known to exist. A formal development would also produce a reusable layer for Itô semimartingales with Poisson jumps: the representation (2.1), compensated jump integrals, and convergence in probability in the Skorokhod space. None of these is currently available in Mathlib.

Difficulty

The obvious argument treats each increment $\Delta^n_iX$ and replaces the estimators $\widehat c(k_n)_i$ by $c_{(i-1)\Delta_n}$. This fails in two places. First, $U(F,k_n)$ has about $t/\Delta_n$ summands, so errors of each summand that vanish in probability need not sum to something small. The infinitely many small jumps must be controlled in mean, through the moment bounds of §8.2 and the growth condition of case (c), and the cutoff $u_n$ must separate jumps from Brownian increments. Second, the estimators look at windows of $k_n$ increments that may contain a jump of $X$ or of $c$. Consistency holds only away from the big jumps, and the jump times are random, so conditioning has to be done with respect to the enlarged filtrations $\mathcal F^{(m)}_t$ that know the big jumps in advance. Finally, the limit is in the Skorokhod topology: the jumps of $U(F,k_n)$ occur at grid times close to, but not equal to, those of $U(F)$, so uniform convergence fails.

Formalization scope

Time is $\mathbb R_{\ge0}$ and processes are functions ℝ≥0 → Ω → ℝ. The Poisson random measure is given by its atoms $N(\omega)\subseteq\mathbb R_+\times E$, with at most one atom at each time. The Brownian integrals use the published EthierKurtz.HasBrownianItoIntegral. The compensated jump integral is characterized by the Lévy–Itô limit of compensated truncated sums. Càdlàg paths and Skorokhod convergence are the published KurtzProtter91.Integrals definitions. Convergence in probability for the Skorokhod topology is the subsequence criterion: every subsequence has a further subsequence converging almost surely. The identity (2.1) and the path properties hold almost surely, for each $t$.

The conventions are the following.

• Following §8.1, $Z$ is written with the same Poisson measure as $X$ and a second Brownian motion $W'$ independent of $W$.
• Clause (b) of (H-·) is not imposed on $Z$.
• $\gamma^0$ means $1_{\{\gamma>0\}}$.
• Increments have integer indices, with $\Delta^n_iX=0$ for $i\le0$.
• $A_0=E$.
• $\Delta_n\to0$ is added to (3.3), as the paper's standing regime.
• The localized bound (8.3) omits the term $|X_t|$: together with the other bounds it cannot hold for all $t$, and keeping it would make the §8 statements vacuous.

The conclusion of Theorem 3.1 includes the a.s. summability of $U(F)_t$. A formalization in which the infinite sum takes a default value, the expectations are junk values of non-integrable variables, or the hypotheses cannot be met is ruled out: $X=W$ with $\sigma\equiv1$ and no jumps satisfies every hypothesis with $r=0$ and $v=1$.

A complete development needs stochastic integration against Brownian motion and compensated Poisson measures, Burkholder-type moment bounds, and the Skorokhod topology on $D[0,\infty)$. These are reusable well beyond this mission. Contributions to any of them, and proofs of individual milestones, are welcome.

Selected references

• J. Jacod, V. Todorov, Do price and volatility jump together?, Ann. Appl. Probab. 20(4) (2010) 1425–1469. arXiv:1010.4990, doi:10.1214/09-AAP654
• J. Jacod, A. N. Shiryaev, Limit Theorems for Stochastic Processes, 2nd ed., Springer, 2003. doi:10.1007/978-3-662-05265-5
• D. Duffie, J. Pan, K. Singleton, Transform analysis and asset pricing for affine jump-diffusions, Econometrica 68 (2000) 1343–1376. doi:10.1111/1468-0262.00164
• T. G. Kurtz, P. Protter, Weak limit theorems for stochastic integrals and stochastic differential equations, Ann. Probab. 19 (1991) 1035–1070. doi:10.1214/aop/1176990334

Motivation

An insurance company that collects premiums and pays random claims is ruined when its surplus becomes negative. The probability of ultimate ruin is the classical solvency criterion of risk theory, going back to Lundberg and Cramér. Real insurers have two levers on this probability: they can invest part of the surplus in a risky asset, and they can cede part of every claim to a reinsurer, at a price. The question of how to use both levers dynamically, as a function of the current surplus, so as to make the probability of ruin as small as possible, is a stochastic control problem for a jump-diffusion.

H. Schmidli, On minimizing the ruin probability by investment and reinsurance, Ann. Appl. Probab. 12 (2002), solves this problem for the Cramér–Lundberg model with proportional reinsurance and investment in a Black–Scholes asset. The main results are a verification theorem (Theorem 1, the subject of this mission) and an existence theorem for the associated integral equation (Theorem 2, the companion mission).

Timeline. Hipp and Plum (2000) treated investment in the Cramér–Lundberg model through the Hamilton–Jacobi–Bellman equation, assuming a bounded solution. Schmidli (2001) treated optimal proportional reinsurance alone. The 2002 paper combines investment and reinsurance, and proves the verification theorem without assuming the solution to be bounded.

Setting

Claims arrive at the jumps $T_1<T_2<\dots$ of a Poisson process $N$ with rate $\lambda>0$; the claim sizes $Y_1,Y_2,\dots$ are i.i.d. with continuous distribution function $G$, $G(0)=0$, independent of $N$. The insurer receives premiums at rate $c>0$. A risky asset $Z_t=\exp\{\sigma W_t+(\mu-\frac12\sigma^2)t\}$, with $\mu,\sigma>0$ and $W$ a standard Brownian motion independent of the claims, is available.

A strategy is a pair of processes $(A_t,b_t)$, predictable for the smallest right-continuous filtration generated by the claims and $W$: $A_t\in\mathbb R$ is the amount invested in the risky asset (locally bounded), and $b_t\in[0,1]$ is the retention level, meaning the insurer pays $b_tY$ of a claim $Y$ occurring at time $t$, at a reinsurance premium rate $c(b_t)$. The surplus $X=X^{Ab}$ starting from $u\ge0$ solves

$$dX_t=\big(c-c(b_t)+\mu A_t\big)\,dt+\sigma A_t\,dW_t-b_t\,dS_t,\qquad X_0=u,$$

where $S_t=\sum_{i\le N_t}Y_i$ is the aggregate claims process. The ruin time is $\tau=\inf\{t\ge0:X_t<0\}$, the survival probability is $\delta^{Ab}(u)=\mathbb P[\tau=\infty]$, and the value function is $\delta(u)=\sup_{A,b}\delta^{Ab}(u)$.

The premium function $c(b)$ is decreasing and continuous on $[0,1]$, $c(1)=0$, $\liminf_{b\uparrow1}c(b)/(1-b)>0$, and there is $\underline b>0$ with $c(b)>c$ for $b<\underline b$ and $c(b)\le c$ for $b\ge\underline b$ (full reinsurance is too expensive).

The Hamilton–Jacobi–Bellman equation for $\delta$ is, with the convention $f(u)=0$ for $u<0$,

$$\sup_{b\in[0,1]}\sup_{A\ge0}\Big[\tfrac12\sigma^2A^2f''(u)+\big(c-c(b)+\mu A\big)f'(u)+\lambda\big(\mathbb E[f(u-bY)]-f(u)\big)\Big]=0.\tag{1}$$

For strictly concave $f$ the maximum over $A$ is attained at $A^*(u)=-\mu f'(u)/(\sigma^2f''(u))$ (equation (2)); $b^*(u)$ denotes a measurable maximiser in $b$.

Formalization targets

Goal: Theorem 1 (p. 896)

Let $f$ be strictly increasing and nonnegative on $[0,\infty)$, continuous there, twice continuously differentiable on $(0,\infty)$, zero on $(-\infty,0)$, and a solution of (1) at every $u>0$. Then $f$ is bounded, $f(\infty)=\lim_{x\to\infty}f(x)\in(0,\infty)$,

$$\delta(u)=\frac{f(u)}{f(\infty)}\qquad(u\ge0),$$

and every surplus process from $u>0$ following $A_t=A^*(X_{t-})$, $b_t=b^*(X_{t-})$ has survival probability $\delta(u)$.

Milestones

The proof of Theorem 1 runs through: Lemma 3 (for small surplus the optimal retention is $b^*=1$); the identity $\mathbb E[f(X^*_{\tau^*\wedge t})]=f(u)$ along the feedback strategy; the inequality $\mathbb E[f(X_{t\wedge\tau})]\le f(u)$ for every strategy; Lemma 1 (almost surely, either ruin occurs or $X_t\to\infty$); the existence of a strategy with $\mathbb P[\tau=\infty]>0$; the comparison $\delta^{Ab}(u)\le f(u)/f(\infty)$ with equality for the feedback strategy; and the absence of ruin by creeping, $\mathbb P[\tau^*<\infty,X^*_{\tau^*}=0]=0$.

Companion statements

The second sentence of Theorem 1 (that $f(x)=1+\int_0^xg(z)\,dz$ satisfies the hypotheses whenever $g$ is a decreasing solution of the integral equation (5)) and its last sentence (at most one such solution of (1) with $f(0)=1$) are separate items.

Significance

Theorem 1 reduces a control problem over all predictable strategies to an analytic question: find one increasing smooth solution of (1). Combined with Theorem 2 (existence of a solution of (5)), it shows that the optimal survival probability is $f(u)/f(\infty)$ and that the optimal strategy is a Markov feedback rule in the current surplus. It also yields that this solution is bounded, which Hipp and Plum (2000) had to assume, and closes the gap they left open on ruin by creeping (Remark (iii), p. 897). Numerical procedures for the optimal strategy (§5 of the paper) rest on this identification.

The theorem is proved in the paper; nothing in it is formalized. The mission produces a machine-checked verification theorem for a controlled jump-diffusion with an Itô integral against Brownian motion, a Poisson claim stream and a predictable control, together with a formal model of the Cramér–Lundberg process with investment and reinsurance that later results in risk theory can reuse.

Difficulty

The standard verification argument applies Itô's formula to $f(X_t)$ and uses (1) to show that $f(X_{t\wedge\tau})$ is a supermartingale, and a martingale under the feedback strategy. Here $f$ is not $C^2$ at $0$ ($f''(0+)=-\infty$), is discontinuous at $0$ after the extension by $0$, and is not assumed bounded, so the stochastic integral is only a local martingale and the passage $t\to\infty$ needs both Lemma 1 and a separate argument that the feedback process does not creep through $0$. Lemma 1 itself is only sketched in the paper ("We will just describe the argument"). The optimality part needs a surplus process following the feedback rule; its existence is not proved in the paper.

Formalization scope

The model is formalized on a measurable space with a probability measure: i.i.d. exponential interarrival times (realising the Poisson process), i.i.d. claim sizes with law $\nu$, and a real Brownian motion (IsBrownianReal), the three families mutually independent. Independence of $W$ from the claims is not printed in the paper but is used by (1) and its proof; it is a disclosed standing assumption. The filtration is $\mathcal F_t=\bigcap_{s>t}\sigma(S_r,W_r:r\le s)$, not completed. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and its paths are required to be continuous, so that the pathwise ruin event is well defined. The surplus equation holds for every $t$ and every sample point.

Conventions: the premium $c(b)$ is real valued (so $c(0)<\infty$, which the paper allows to fail when $\mathbb E[Y]<\infty$); the supremum in (1) is stated as a least upper bound equal to $0$, so an unbounded family never counts as a solution; $f$ is $C^2$ on $(0,\infty)$ and (1) is required for $u>0$; $\delta$ is a supremum over all admissible triples (strategy and surplus process); the controls of the feedback rule at non-positive pre-jump surplus are left free, and optimality is stated for $u>0$. Expectations of $f(X_{t\wedge\tau})$ are lower Lebesgue integrals of nonnegative functions, so no default value of a non-integrable expectation satisfies an inequality. The optimality clause is stated for every process following the feedback rule; it would be vacuous if no such process existed, and its existence is not part of the target.

Infrastructure needed: Itô's formula for a semimartingale with Brownian and compound-Poisson parts, the compensator of the compound Poisson random measure, localisation, and optional stopping. The model definitions, the HJB predicate and the comparison lemmas are reusable for other ruin-minimisation and dividend problems. Contributions to any milestone, and to general stochastic-calculus lemmas they need, are welcome.

Selected references

• H. Schmidli, On minimizing the ruin probability by investment and reinsurance, Ann. Appl. Probab. 12(3) (2002), 890–907. https://doi.org/10.1214/aoap/1031863173
• C. Hipp, M. Plum, Optimal investment for insurers, Insurance Math. Econom. 27 (2000), 215–228. https://doi.org/10.1016/S0167-6687(00)00049-4
• H. Schmidli, Optimal proportional reinsurance policies in a dynamic setting, Scand. Actuar. J. (2001), 55–68. https://doi.org/10.1080/034612301750077338
• P. Brémaud, Point Processes and Queues: Martingale Dynamics, Springer (1981). https://doi.org/10.1007/978-1-4684-9477-8

Motivation

Measurements of Ethernet and Internet traffic in the 1990s showed that the amount of data offered to a link is bursty on every time scale and that the lengths of transmissions (file sizes, connection durations) have heavy, regularly varying tails. Two families of approximations for the cumulative input were proposed: fractional Brownian motion, which has dependent Gaussian increments, and α-stable Lévy motion, which has independent, heavy-tailed increments. The two lead to very different predictions for buffer overflow and link dimensioning.

T. Mikosch, S. Resnick, H. Rootzén and A. Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both answers are correct in different regimes, and that the regime is decided by how fast the connection rate grows relative to the time scale. This mission formalizes their result for the infinite source Poisson model under slow growth, where the limit is a totally skewed α-stable Lévy motion. Companion missions treat the ON/OFF model and the fast-growth regime with its fractional Brownian limit.

Setting

A transmission length has law $F_{\mathrm{on}}$ on $[0,\infty)$ with tail $\bar F_{\mathrm{on}}(x)=F_{\mathrm{on}}((x,\infty))$. Condition (2.8) asks

$$\bar F_{\mathrm{on}}(x)=x^{-\alpha}L(x),\qquad x>0,\quad 1<\alpha<2,$$

with $L$ slowly varying ($L(cx)/L(x)\to1$ for every $c>0$). The mean $\mu_{\mathrm{on}}$ is finite and the variance infinite. The quantile function (2.9) is $b(t)=(1/\bar F_{\mathrm{on}})^{\leftarrow}(t)=\inf\{x:1/\bar F_{\mathrm{on}}(x)\ge t\}$.

In the $T$-th model, connections start at the points $(\Gamma_k)_{k\in\mathbb Z}$ of a homogeneous Poisson process on $\mathbb R$ with rate $\lambda=\lambda(T)$, labelled so that $\Gamma_0<0<\Gamma_1$. Connection $k$ transmits at unit rate for a time $X_k$; the $X_k$ are iid with law $F_{\mathrm{on}}$ and independent of the $\Gamma_k$. The number of active connections and the cumulative input are

$$N(t)=\sum_{k\in\mathbb Z}\mathbf 1[\Gamma_k\le t<\Gamma_k+X_k],\qquad A(t)=\int_0^tN(s)\,ds .$$

The rate $\lambda(T)$ is a positive non-decreasing function of $T$. Slow Growth Condition 1 is

$$\lim_{T\to\infty}\frac{b(\lambda T)}{T}=0,$$

where $b(\lambda T)$ is $b$ evaluated at $\lambda(T)\,T$.

The stable law $S_\alpha(\sigma,\beta,\mu)$ is the law with characteristic function $\exp\{-\sigma^\alpha|\theta|^\alpha(1-i\beta\,\mathrm{sign}(\theta)\tan(\pi\alpha/2))+i\mu\theta\}$ for $\alpha\ne1$. α-stable Lévy motion $X_{\alpha,\sigma,\beta}$ has independent stationary increments with $X(t)-X(s)\sim S_\alpha(\sigma(t-s)^{1/\alpha},\beta,0)$. Write

$$C_\alpha=\frac{1-\alpha}{\Gamma(2-\alpha)\cos(\pi\alpha/2)}\quad(5.1).$$

Formalization targets

Goal: Theorem 1 (corrected scale)

Under (2.8) and Condition 1,

$$\frac{A(T\cdot)-T\lambda\mu_{\mathrm{on}}(\cdot)}{b(\lambda T)}\xrightarrow{\ fidi\ }X_{\alpha,C_\alpha^{-1/\alpha},1}(\cdot),$$

convergence of the finite-dimensional distributions to a totally skewed ($\beta=1$) α-stable Lévy motion.

On the scale. The paper prints the limit $X_{\alpha,1,1}$. Its own proof establishes $\lambda T\,P(j_1>b(\lambda T)x)\to x^{-\alpha}$ (pp. 37–38), which makes $\alpha x^{-\alpha-1}dx$ the Lévy measure of the limit. The totally skewed stable law with that Lévy measure has $\sigma^\alpha=\Gamma(1-\alpha)\cos(\pi\alpha/2)=C_\alpha^{-1}$ (Samorodnitsky–Taqqu, Property 1.2.15; also the paper's own criterion on p. 47 with $c=1$, and the $\sigma$ the paper prints in Theorem 2). Since $C_\alpha$ decreases from $2/\pi$ to $0$ on $(1,2)$ ($C_{1.5}\approx0.399$), the printed limit has the wrong scale and the theorem as printed is false. The goal states the corrected scale $C_\alpha^{-1/\alpha}$; milestones quote the page as printed.

Milestones, in attack order

(2.14), the covariance of $N$; Lemma 1 part 1 (Condition 1 $\iff\lambda T\bar F_{\mathrm{on}}(T)\to0\iff\mathrm{Cov}(N_T(0),N_T(T))\to0$); Lemma 2, slow part ($\lambda T^2\bar F_{\mathrm{on}}(T)/b(\lambda T)\to0$); (4.15), negligibility of the boundary pieces $A_2,A_3,A_4$; the tail limit of $j_1$; (4.17), $A_{12}=O_P([\lambda T]^{1/2})=o_P(b(\lambda T))$; (4.20)–(4.21), $A_{13}=o(b(\lambda T))$; (4.19), corrected, the stable limit of $A_{11}$; the corrected one-dimensional limit of $A(T)$; and $EA_{22}=o(b(\lambda T))$ of §4.5, which reduces the fidi convergence to the one-dimensional one.

Significance

The theorem shows that under slow connection growth the cumulative input is asymptotically a process with independent, infinite-variance increments. Long-range dependence present in each model (the covariance (2.14) decays like $h^{-(\alpha-1)}L(h)$) disappears on the time scale $T$, and the heavy tail of the transmission lengths dominates. Together with the fast-growth result (fractional Brownian motion) it explains why both approximations are found in measured traffic, and it identifies the critical quantity $b(\lambda T)/T$.

The result is proved in the paper, modulo the scale. No part of it is machine-checked. The mission produces a formal statement of the infinite source Poisson model with its marked point process structure, a formal statement of stable laws and stable Lévy motion through their characteristic functions, and machine-checked versions of the paper's estimates. Correcting the printed scale is part of the output.

Difficulty

The pieces $A_2,A_3,A_4,A_{12},A_{13},A_{22}$ are controlled by first moments, regular variation and Lemma 2. The central step is the stable limit of $A_{11}$: a sum of a Poisson number of iid, heavy-tailed summands whose law changes with $T$. A classical central limit theorem does not apply because the variance is infinite, and the summands form a triangular array. The paper cites a point-process limit (Resnick's Exercise 4.4.2.8) for this step; a formal proof needs a convergence theorem for row-wise iid triangular arrays to stable laws, with the constant $C_\alpha$ computed exactly.

Formalization scope

Each $T$ has its own probability space carrying the $T$-th model, and every statement quantifies over all such families. The Poisson points are given by their iid exponential spacings $-\Gamma_0,\Gamma_1,\Gamma_{k+1}-\Gamma_k$ $(k\ne0)$, indexed by $\mathbb Z$. (2.8) is stated as "$x\mapsto x^\alpha\bar F_{\mathrm{on}}(x)$ is slowly varying", with lengths non-negative. $b(t)$ is $\inf\{x>0:t\bar F_{\mathrm{on}}(x)\le1\}$, which equals the page's generalized inverse for $t>0$. $N(t)$ is a cardinality and the region sums are sums of non-negative terms; their junk values (an infinite set, a non-summable family) occur only on null events. $A$ is an interval integral. The growth hypothesis is: $\lambda>0$, non-decreasing, Condition 1. No other hypothesis is added.

The fidi limit is pinned by its characteristic function on $\mathbb R^k$ for sorted times $0\le t_1\le\dots\le t_k$: the product of the characteristic functions of $S_\alpha(\sigma(t_j-t_{j-1})^{1/\alpha},1,0)$ evaluated at $\theta_j+\dots+\theta_k$. The existence of the limit law is part of the claim. One-dimensional limits are stated the same way on $\mathbb R$. Convergence in probability to $0$ is $P_T(|Y_T|>\eta)\to0$ for every $\eta>0$.

Trivializing formalizations are excluded:

• $b$ is never the junk value $0$, since its defining set is nonempty and bounded below.
• The model hypothesis is satisfiable for every rate and length law; a sanity file builds it from product measures, together with a Pareto law satisfying (2.8) and a rate satisfying Condition 1.
• The limit object is fixed by its characteristic function, not merely asserted to exist.
• Only fidi convergence is claimed, as on the page. Convergence in the Skorokhod $J_1$ topology fails for this model (Remark after Theorem 1).

A complete development needs regular variation (Karamata's theorem, Potter bounds, generalized inverses), the Poisson random measure of the marked points, and stable limits for triangular arrays. All three are reusable beyond this mission. Proofs of the milestones are welcome separately, as are general Mathlib-style lemmas on regular variation.

Selected references

• T. Mikosch, S. Resnick, H. Rootzén, A. Stegeman, Is network traffic approximated by stable Lévy motion or fractional Brownian motion?, Ann. Appl. Probab. 12(1) (2002) 23–68. https://doi.org/10.1214/aoap/1015961155
• G. Samorodnitsky, M. S. Taqqu, Stable Non-Gaussian Random Processes, Chapman & Hall, 1994. https://doi.org/10.1201/9780203738818
• N. H. Bingham, C. M. Goldie, J. L. Teugels, Regular Variation, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511721434
• S. I. Resnick, Extreme Values, Regular Variation, and Point Processes, Springer, 1987. https://doi.org/10.1007/978-0-387-75953-1