Statistics

Motivation

Nonlinear filtering asks for the conditional law of an unobserved Markov process given noisy partial observations of it. It is the computational core of data assimilation in weather forecasting, oceanography and geophysics, of target tracking, and of inference in large networked systems. The standard numerical method, the particle filter, replaces the conditional law by a cloud of $N$ weighted samples. Its error is well understood in fixed dimension, but in practice it degrades exponentially in the dimension of the state: the number of particles needed for a fixed accuracy grows exponentially with the number of variables. This phenomenon, the curse of dimensionality of particle filters, has been documented empirically and analysed by Bickel, Li and Bengtsson and by Snyder et al. (Bickel–Li–Bengtsson 2008; Snyder et al. 2008), and it is a main obstacle to their use in high-dimensional data assimilation.

Rebeschini and van Handel (arXiv:1301.6585v2, Ann. Appl. Probab. 25(5), 2015) gave the first rigorous proof that a local variant of the particle filter, the block particle filter, has an approximation error that does not depend on the model dimension, for models with local interactions above a mixing threshold. The result is the standard theoretical reference for localization in sequential Monte Carlo.

Setting

Let $G=(V,E)$ be a finite graph with graph distance $d$, and fix a neighbourhood size $r\ge1$. The $r$-neighbourhood of a vertex is $N(v)=\{v':d(v,v')\le r\}$, and the $r$-inner boundary of $J\subseteq V$ is $\partial J=\{v\in J:N(v)\not\subseteq J\}$. Each vertex carries a Polish state space $\mathbb X^v$ with a reference measure $\psi^v$, and an observation space $\mathbb Y^v$; write $\mathbb X=\prod_v\mathbb X^v$ and $\psi=\bigotimes_v\psi^v$.

The hidden process $(X_n)_{n\ge0}$ is a Markov chain on $\mathbb X$ with transition density $p(x,z)=\prod_{v}p^v(x,z^v)$ with respect to $\psi$, where each $p^v(x,z^v)$ depends on $x$ only through $x^{N(v)}$ (locality). The observation $Y_n$ has density $g(x,y)=\prod_v g^v(x^v,y^v)$ given $X_n=x$. For a fixed observation sequence, the filter is the recursion

$$\pi_0=\delta_x,\qquad \pi_n=\mathsf C_n\mathsf P\pi_{n-1},$$

where $\mathsf P$ applies the transition kernel and $\mathsf C_n$ reweights by $g(\cdot,Y_n)$ and renormalizes (the Bayes formula).

A partition $\mathcal K$ of $V$ into blocks defines the blocking operator $\mathsf B\rho=\bigotimes_{K\in\mathcal K}\mathsf B^K\rho$, which replaces a measure by the product of its block marginals. The block particle filter with $N$ particles is

$$\hat\pi_n=\mathsf C_n\mathsf B\mathsf S^N\mathsf P\hat\pi_{n-1},$$

where $\mathsf S^N$ replaces a measure by the empirical measure of $N$ i.i.d. samples from it. The local quantities are $|\mathcal K|_\infty=\max_K\operatorname{card}K$, $\Delta=\max_v\operatorname{card}N(v)$, and $\Delta_{\mathcal K}=\max_K\operatorname{card}\{K':d(K,K')\le r\}$. The error is measured locally:

$$|||\rho-\rho'|||_J=\sup_{f\in\mathbb X^J,\,|f|\le1}\mathbf E\big[|\rho(f)-\rho'(f)|^2\big]^{1/2},$$

where $\mathbb X^J$ is the class of measurable functions depending only on the coordinates in $J$.

Formalization targets

Goal: Theorem 2.1

There is $0<\varepsilon_0<1$ depending only on $(\Delta,\Delta_{\mathcal K})$ such that, if $\varepsilon_0<\varepsilon<1$, $0<\kappa<1$, $\varepsilon\le p^v\le\varepsilon^{-1}$ and $\kappa\le g^v\le\kappa^{-1}$, then for all $n\ge0$, $x\in\mathbb X$, $K\in\mathcal K$, $J\subseteq K$,

$$|||\pi^x_n-\hat\pi^x_n|||_J\le\alpha\operatorname{card}J\Big[e^{-\beta_1d(J,\partial K)}+\frac{e^{\beta_2|\mathcal K|_\infty}}{\sqrt N}\Big],$$

with $0<\alpha,\beta_1,\beta_2<\infty$ depending only on $(\varepsilon,\kappa,r,\Delta,\Delta_{\mathcal K})$. The goal states the constants existentially, as the paper does, so that it survives any improvement of them.

Milestones

The proof splits the error through the block filter $\tilde\pi_n=\mathsf C_n\mathsf B\mathsf P\tilde\pi_{n-1}$:

1. elementary lemmas: Lemma 4.1 (minorization), Lemma 4.2 (reweighting), Lemma 4.3 (weighted Neumann series);
2. Theorem 3.1, the Dobrushin comparison theorem;
3. Theorem 4.14, the bias term $\|\pi^x_n-\tilde\pi^x_n\|_J\le\frac{8e^{-\beta}}{1-e^{-\beta}}(1-\varepsilon^{2\Delta})\operatorname{card}J\,e^{-\beta d(J,\partial K)}$;
4. Proposition 4.17, stability of the block filter from product initial laws;
5. Lemma 4.19, Lemma 4.20 (products of empirical measures) and Proposition 4.22, the one-step sampling errors;
6. Theorem 4.23, the variance term $|||\tilde\pi^x_n-\hat\pi^x_n|||_J\le\operatorname{card}J\,\frac{64\Delta_{\mathcal K}e^\beta}{1-e^{-\beta}}\frac{\varepsilon^{-4|\mathcal K|_\infty}\kappa^{-4|\mathcal K|_\infty\Delta_{\mathcal K}}}{\sqrt N}$.

Theorems 4.14 and 4.23 together give Theorem 2.1 by the triangle inequality.

Significance

The theorem shows that the error of a local particle filter can be controlled by quantities that are local in the graph: neither the assumptions nor the bound depend on the time horizon or on $\operatorname{card}V$. On a square lattice, choosing blocks of side length of order $\log N$ balances the two terms and gives a local error, at most locations, that tends to zero as $N\to\infty$ uniformly in time and in the lattice size (the paper's Corollary 2.5, which is not part of this mission): the number of particles needed for a given local accuracy does not grow with the dimension. The result identifies decay of correlations of the filter, established through the Dobrushin comparison theorem, as the mechanism that makes localization work, and it underlies later work on local particle filters and their spatial bias.

The result is proved on paper. No part of it is formalized, and the formal library has no nonlinear filter, no particle filter and no Dobrushin comparison theorem. The mission produces machine-checked statements of the main theorem and of the intermediate results of its proof, with explicit constants for the two halves; proofs of any milestone, or of the goal from Theorems 4.14 and 4.23, are the remaining work.

Difficulty

The obvious argument fails in two places. First, the standard particle filter error bound is uniform in time only through filter stability, and its constants are exponential in the dimension, because the reweighting step compares likelihoods over all of $V$ at once. Localizing the sampling (blocking) removes this, but introduces a bias at block boundaries that must not accumulate over time. Controlling that bias requires showing that the filter has decay of correlations uniformly in time, which is a statement about conditional distributions of a high-dimensional measure, not about its marginals. Second, the sampling error must be propagated through the block filter dynamics in a norm strong enough to compose: the weak $|||\cdot|||$ norm does not contract under the block filter, which is why the paper measures one-step errors in total variation after one further step of dynamics.

Formalization scope

The Lean development is in the namespace LocalPF.Block. Committed conventions:

• the graph distance takes values in $\mathbb N\cup\{\infty\}$, and $e^{-\beta d}=0$ for $d=\infty$; the partition is a surjective block label map;
• the filter, block filter and block particle filter are defined by their recursions for a fixed observation sequence, and every statement holds for every observation sequence (Remark 2.4); the reference measure of the observations is omitted;
• the block particle filter is represented by the law of its particle array at each step, built with the Giry monad bind, and the step-$n$ estimate as a function of that array;
• total variation norms $\|\cdot\|$, $\|\cdot\|_J$ are suprema in $[0,\infty]$; $|||\cdot|||_J\le B$ is stated as $\mathbf E[|\rho(f)-\rho'(f)|^2]\le B^2$ for every test function, with lower Lebesgue integrals;
• $r\ge1$ and $N\ge1$; reference measures are $\sigma$-finite.

Added or changed hypotheses, each disclosed in the item: strict positivity and integrability of $g^v$ in Theorem 4.14 and Proposition 4.17 (the paper assumes no bounds on $g$ there; without them the Bayes formula is undefined); explicit bounds $0<a\le\Lambda\le b$ in Lemma 4.2, whose $|||\cdot|||$ clause is stated for Giry-measurable random probability measures; $\varepsilon<1$ in Theorem 4.23, excluding only the case where the paper's bound is $+\infty$; Lemma 4.19 and Proposition 4.22 are stated for every deterministic probability measure in place of the random previous estimate, which is stronger.

The statement admits no trivializing reading: the constants of Theorem 2.1 are quantified before the graph and the model, so they cannot depend on $\operatorname{card}V$; the goal and Theorem 4.23 assert that the particle-array law is a probability measure, so a zero law cannot make the expectation vanish; test functions are measurable and bounded, so the integrals are not junk values; $N\ge1$ excludes division by $\sqrt0$; and the correction step's normalizer is positive and finite under the stated hypotheses.

Needed infrastructure: product measures over finite index sets and their marginals, the Giry monad and measurability of the maps it composes, conditional distributions on products of Polish spaces, and matrix Neumann series. The Dobrushin comparison theorem and the V-statistic bound (Lemma 4.20) are reusable beyond filtering. Proofs of any milestone are welcome, and so are formal statements of the remaining results of §4 (Propositions 4.4, 4.8, 4.9, Corollary 4.13).

Selected references

• P. Rebeschini and R. van Handel, Can local particle filters beat the curse of dimensionality?, Ann. Appl. Probab. 25(5), 2809–2866, 2015. arXiv:1301.6585, doi:10.1214/14-AAP1061
• P. Bickel, B. Li and T. Bengtsson, Sharp failure rates for the bootstrap particle filter in high dimensions, IMS Collections 3, 318–329, 2008. doi:10.1214/074921708000000228
• C. Snyder, T. Bengtsson, P. Bickel and J. Anderson, Obstacles to high-dimensional particle filtering, Monthly Weather Review 136(12), 4629–4640, 2008. doi:10.1175/2008MWR2529.1
• H.-O. Georgii, Gibbs Measures and Phase Transitions, de Gruyter, 2nd ed., 2011 (Theorem 8.20, the Dobrushin comparison theorem). doi:10.1515/9783110250329

Decisions with covariate information

In many operational problems the decision $z$ is taken after observing covariates $x$ (weather, calendar, prices) that carry information about an uncertain quantity $Y$ (demand, yield, return). The target is the conditional stochastic program: minimize $\mathbb E[c(z,Y)\mid X=x]$ over a feasible set $\mathcal Z$. Kannan, Bayraksan and Luedtke (Math. Program. 2023) approach it in two steps: fit a regression model of $Y$ on $X$, then use the regression residuals as scenarios of the uncertainty at the new covariate $x$. Their earlier work (Kannan, Bayraksan, Luedtke, arXiv:2207.13554) analysed the sample average approximation built in this way (ER-SAA). The 2023 paper wraps the same scenarios in a distributionally robust problem, to protect against the small-sample error of the regression and of the residuals.

This mission formalizes the paper's rate of convergence for a family of ambiguity sets that contains sample robust optimization and reweighting (φ-divergence, CVaR) sets as special cases.

Setting

Responses $Y\in\mathbb R^{d_y}$ follow $Y=f^*(X)+\varepsilon$, with regression function $f^*$ and error $\varepsilon$ of law $P_\varepsilon$. A known nonempty closed convex set $\mathcal Y$ contains the range of $Y$, with orthogonal projection $\mathrm{proj}_{\mathcal Y}$. From data $\mathcal D_n=\{(y^i,x^i)\}_{i=1}^n$, with $\varepsilon^i=y^i-f^*(x^i)$, one computes a regression estimate $\hat f_n$ and residuals $\hat\varepsilon^i_n=y^i-\hat f_n(x^i)$. At a covariate realization $x$ the scenarios are $\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)$.

The true problem (3) is $v^*(x)=\min_{z\in\mathcal Z}g(z;x)$ with $g(z;x)=\mathbb E[c(z,f^*(x)+\varepsilon)]$, and the full-information SAA objective (4) is $g^*_n(z;x)=\frac1n\sum_i c(z,f^*(x)+\varepsilon^i)$.

The unified ambiguity family of §5 has two radii. $\mu_n(x)\ge0$ is the radius of balls $\hat{\mathcal Y}^i_n=\{y\in\mathcal Y:\|y-\mathrm{proj}_{\mathcal Y}(\hat f_n(x)+\hat\varepsilon^i_n)\|\le\mu_n(x)\}$ around each scenario. $\mathfrak P_n=\mathfrak P_n(x;\zeta_n(x))$ is a set of probability vectors that shrinks to the uniform weights. The worst-case expected cost over the distributions $\sum_ip_i\delta_{\bar y^i}$ with $p\in\mathfrak P_n$ and $\bar y^i\in\hat{\mathcal Y}^i_n$ is the ER-DRO objective

$$\hat g^{ER}_{s,n}(z;x)=\sup_{p\in\mathfrak P_n}\sum_{i=1}^n p_i\sup_{y\in\hat{\mathcal Y}^i_n}c(z,y),$$

and the ER-DRO problem (8) is $\hat v^{DRO}_n(x)=\min_{z\in\mathcal Z}\hat g^{ER}_{s,n}(z;x)$, with optimal solution $\hat z^{DRO}_n(x)$. Taking $\zeta_n\equiv0$ gives sample robust optimization; taking $\mu_n\equiv0$ gives ambiguity sets with the same support as the empirical residual distribution. The intermediate objective $g^*_{s,n}(z;x)=\sup_{p\in\mathfrak P_n}\sum_ip_i\,c(z,f^*(x)+\varepsilon^i)$ reweights the true scenarios.

Formalization targets

Goal: Theorem 17 (p. 24)

Assume the following:

• Assumption 9: $c(z,\cdot)$ is Lipschitz on $\mathcal Y$, with constants $L(z)$ bounded on $\mathcal Z$.
• Assumption 12: $\sup_{p\in\mathfrak P_n}\sum_i(p_i-\frac1n)^2=C_\zeta n^{-(1+r)}$.
• Assumption 13: a uniform weak LLN for $c^2$.
• Assumption 14: a functional CLT for $\sqrt n(g^*_n-g)$ in $C(\mathcal Z)$.
• Assumption 15: the regression rate $\|f^*(x)-\hat f_n(x)\|^2=O_p(n^{-r})$ and $\frac1n\sum_i\|f^*(x^i)-\hat f_n(x^i)\|^2=O_p(n^{-r})$ with $0<r\le1$.
• The radius is $\mu_n=C_\mu n^{-r/2}$.

Then

$$\bigl|\hat v^{DRO}_n(x)-v^*(x)\bigr|=O_p(n^{-r/2}),\qquad \bigl|g(\hat z^{DRO}_n(x);x)-v^*(x)\bigr|=O_p(n^{-r/2}).$$

Milestones

1. Lemma 14, the deterministic three-term bound (12) on $\sup_z|\hat g^{ER}_{s,n}-g|$.
2. $\sup_z|\hat g^{ER}_{s,n}-g^*_{s,n}|=O_p(n^{-r/2})$, the regression term.
3. $\sup_z|g^*_{s,n}-g^*_n|=O_p(n^{-r/2})$, the reweighting term.
4. $\sup_z|g^*_n-g|=O_p(n^{-1/2})$, the full-information term.
5. $\sup_z|\hat g^{ER}_{s,n}-g|=O_p(n^{-r/2})$, the uniform rate of the objective.

Significance

Theorem 17 shows that robustifying the residuals-based SAA costs nothing in rate. With $\rho=1+r$ the ER-DRO estimators converge at the rate $n^{-r/2}$ of the ER-SAA estimators, which is set by the regression step: $r=1$ for OLS or Lasso, and $r=C/d_x$ for kernel regression or random forests. It covers in one statement sample-robust sets, φ-divergence sets and CVaR sets around the residual scenarios. It is the template for the paper's mean-rate analogue (Theorem 18) and for the consistency results (Proposition 15, Theorem 16), which reuse Lemma 14.

The result is proved in the paper; nothing in it is machine-checked. The mission produces checked versions of the decomposition (12) and of each $O_p$ step. It also produces a reusable $O_p$ predicate, a statement of a functional CLT in $C(\mathcal Z)$ through Mathlib's convergence in distribution, and the passage from a uniform objective rate to rates for the optimal value and the out-of-sample cost.

Difficulty

The paper's proof is short, but each line hides a step. The obvious bound on the regression term uses the plain average $\frac1n\sum_i\|\tilde\varepsilon^i_n\|$. Under a reweighting $p\in\mathfrak P_n$ that average is no longer what appears, and controlling $\sum_ip_i\|\tilde\varepsilon^i_n\|$ needs the factor $(1+n\sum_i(p_i-\frac1n)^2)^{1/2}$, which stays bounded only because of the rate in Assumption 12.

The full-information term needs tightness of $\sup_z|\sqrt n(g^*_n-g)|$ from convergence in distribution in $C(\mathcal Z)$. That is a continuous-mapping and Portmanteau argument on a function space, not on $\mathbb R$.

All suprema over $z$ may be infinite for individual data realizations, and the probabilities of the events involved need not be measurable. Arithmetic with $O_p$ (sums, products with $O_p(1)$, comparing rates $n^{-1/2}\le n^{-r/2}$) must be carried out with these in mind.

Formalization scope

Carriers are the Euclidean spaces $\mathbb R^{d_x}$, $\mathbb R^{d_y}$, $\mathbb R^{d_z}$. The data are random variables on a probability space $(\Omega,P)$, and sample $i\in[n]$ is i : Fin n. The covariate $x$ is fixed, and the paper's "for a.e. $x$" assumptions are hypotheses at that $x$. No i.i.d. assumption is made. $\mathfrak P_n$ is a nonempty subset of the probability simplex. The limit clause of (9) concerns the family in the radius at fixed $n$; Theorem 17 does not use it, so it is omitted. Assumption 12 is printed as an equality for every $n$, which cannot hold at $n=1$ (there $\mathfrak P_1\subseteq\{(1)\}$), so it is required for all large $n$. $\hat g^{ER}_{s,n}$ is defined by the explicit formula of p. 20, which the paper states equals the worst-case expectation over $\hat{\mathcal P}_n(x)$. $\hat z^{DRO}_n$ and a true minimizer $z^*$ are taken as given selections of minimizers; the paper's standing assumptions guarantee they exist.

$O_p(w_n)$ means: for every $\delta>0$ there are $M>0$ and $N$ with $P(V_n>Mw_n)\le\delta$ for all $n\ge N$, for $[0,\infty]$-valued $V_n$. Every supremum over $z$ is computed in $[0,\infty]$, so an unbounded family is never read as $0$. Convergence in distribution is Mathlib's TendstoInDistribution for the Borel $\sigma$-algebra on $C(\mathcal Z)$.

The sample-robust balls are centred at the projected residual scenarios, not at the true scenarios $f^*(x)+\varepsilon^i$. Centring them at the true scenarios would make the regression term vanish and the goal close to the full-information result.

A complete development needs the Cauchy–Schwarz steps of Appendix A.6 and the nonexpansiveness of the projection onto a closed convex set (inequality (6)). It also needs a calculus of $O_p$, tightness of norms under convergence in distribution in $C(\mathcal Z)$, and the passage from uniform objective rates to optimal-value rates. The $O_p$ calculus and the tightness lemma are reusable beyond this paper. Contributions proving any milestone, or general $O_p$ lemmas as separate theorems, are welcome.

Selected references

• R. Kannan, G. Bayraksan, J. R. Luedtke, Residuals-based distributionally robust optimization with covariate information, Mathematical Programming, 2023. https://doi.org/10.1007/s10107-023-02014-7
• R. Kannan, G. Bayraksan, J. R. Luedtke, Data-driven sample average approximation with covariate information, arXiv:2207.13554 (2022). https://arxiv.org/abs/2207.13554
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• D. Bertsimas, S. Shtern, B. Sturt, Two-stage sample robust optimization, Operations Research 70(1), 2022. https://doi.org/10.1287/opre.2020.2096

Motivation

Adversarial training asks a classifier to work even after an input has been changed within a prescribed perturbation budget. Tsipras, Santurkar, Engstrom, Turner, and Mądry studied why the classifier that performs best on ordinary inputs can behave very differently under these changes. Their explicit model separates one reliably predictive feature from many individually weak features. It lets the same distribution support a highly accurate ordinary classifier and a less accurate but robust classifier Tsipras et al., §2.1–2.2. This mission formalizes the paper's comparison for soft-margin support vector machines at the population level.

The model is relevant to anyone using a training objective as a proxy for performance under perturbations. Its conclusion concerns the optimizer of an expected loss, not the effect of a particular finite sample or optimization algorithm. That distinction makes the example a direct statement about the objectives being optimized.

Setting

A label $y$ is drawn uniformly from $\{-1,+1\}$. An input $x$ has $d+1$ real coordinates. Its first coordinate, $x_1$, equals $y$ with probability $p$ and $-y$ with probability $1-p$, where $p\ge1/2$. Conditional on $y$, each of the remaining coordinates is an independent Gaussian variable with mean $\eta y$ and variance one, independently of $x_1$. Thus $x_1$ is a moderately reliable feature while the other coordinates can be weak predictors individually. These are exactly the ingredients of distribution $D$ in equation (3) Tsipras et al., p. 4.

For a weight vector $w$, the linear classifier $f_w$ assigns the sign of $w^\top x$. Its standard accuracy is the probability that $f_w(x)=y$ for a fresh pair $(x,y)$ from $D$. Its robust accuracy at radius $\varepsilon$ is the probability that this equality holds for every perturbation $\delta$ with $\|\delta\|_\infty\le\varepsilon$. Both accuracies average the two labels with probability $1/2$ each.

The soft-margin SVM objective combines expected hinge loss and quadratic regularization:

$$J_\lambda(w)=\mathbb E_D\!\left[\max\{0,1-yw^\top x\}\right] +\frac{\lambda}{2}\|w\|_2^2.$$

The distributional adversarial objective replaces the hinge loss for each observed pair by its maximum over the $\ell_\infty$ ball before taking the expectation:

$$J^{\mathrm{adv}}_{\varepsilon,\lambda}(w)= \mathbb E_D\!\left[ \max_{\|\delta\|_\infty\le\varepsilon} \max\{0,1-yw^\top(x+\delta)\}\right] +\frac{\lambda}{2}\|w\|_2^2.$$

This order follows equation (2), the distributional adversarial loss Tsipras et al., pp. 2, 16–18.

Formalization targets

The goal is Theorem 2.2 Tsipras et al., p. 6. Under $d\ge1$, $1/2\le p\le0.975$, and $\eta\ge4/\sqrt d$, a global minimizer $w^*$ of $J_\lambda$ whose squared Euclidean norm is one satisfies

$$\operatorname{StdAcc}(f_{w^*})>0.99, \qquad \operatorname{RobAcc}_{\varepsilon}(f_{w^*})<0.01 \quad\text{for every }\varepsilon\ge2\eta.$$

For a global minimizer of $J^{\mathrm{adv}}_{\varepsilon_{\mathrm{tr}},\lambda}$ with $\varepsilon_{\mathrm{tr}}\ge2\eta$ and either $\varepsilon_{\mathrm{tr}}<2p-1$ or $p=1/2$, the target is

$$\operatorname{StdAcc}(f_{w^*}) =\operatorname{RobAcc}_{\varepsilon}(f_{w^*})=p \quad\text{for every }0\le\varepsilon<1.$$

The milestone list follows Appendix D's stated claims: the Gaussian law of the pooled weak feature, Lemmas D.1–D.5, and the displayed adversarial objective identity. The lemmas give nonstrict $99\%$ and $1\%$ bounds where the theorem states strict inequalities Tsipras et al., pp. 16–18.

Significance

The result gives a concrete distribution on which the ordinary population hinge objective favors weak features enough to achieve near-perfect standard accuracy while remaining vulnerable to a small coordinatewise perturbation. The adversarial objective instead selects a classifier using the first feature, whose standard and robust accuracies are both $p$. It therefore distinguishes the behavior of the two objectives even without sampling error or a particular training algorithm.

The paper proves these claims informally. The Lean items here compile as definitions and theorem statements with open proofs; they are not yet machine-checked proofs. A completed development would supply the Gaussian probability estimates, optimizer properties, and accuracy calculations needed to close the statements. The law of a pooled Gaussian vector and the relation between $\ell_\infty$ perturbations and the $\ell_1$ weight norm are reusable beyond this example.

Difficulty

The first weak feature alone carries little information, but their normalized sum has a strong Gaussian signal. Consequently, reasoning about one coordinate at a time does not determine what the ordinary SVM minimizer predicts. The theorem also concerns every global minimizer with the stipulated norm, so testing a convenient weight vector does not settle it. The stated strict accuracy constants require quantitative Gaussian tails and an optimizer comparison at the specified $p$ and $\eta$ thresholds. In the adversarial part, the conclusion about accuracy $p$ requires more than proving that weak-feature weights vanish: the remaining first-feature coefficient must have the correct sign and be nonzero.

Formalization scope

Lean represents an input as a function on Fin (d+1); index zero is the paper's $x_1$, and index i.succ is $x_{i+2}$. The function norm is the sup norm, so $\|\delta\|\le\varepsilon$ is exactly the $\ell_\infty$ ball. Squared $\ell_2$ norm and $\ell_1$ norm of a weight vector are written as $\sum_iw_i^2$ and $\sum_i|w_i|$. The conditional law is a product of the two-point first-feature law and the independent Gaussian weak-feature law, assembled into one input vector. GaussianReal's variance argument is one. Labels and predictions are real $\pm1$, and a zero score is assigned $-1$. The tie has probability zero for the nondegenerate classifiers in the theorem.

The robust event can be outside the Borel sigma algebra. Its measure in Lean is an outer measure, agreeing with probability under completion. Gaussian affine hinge functions are integrable; the adversarial hinge has the explicit finite closed form supplied by a milestone when the radius is nonnegative. The supremum is over exactly the admissible perturbations. The mission does not reduce the target to a chosen classifier or assume any of the milestone conclusions as goal hypotheses.

Several hypotheses make implicit conditions or a necessary correction explicit. The condition $d\ge1$ prevents $4/\sqrt d$ from becoming Lean's default value at zero. Appendix D assumes that $\lambda>0$ has been tuned so an ordinary global minimizer has $\|w^*\|_2=1$; that is represented directly. Evaluation radii are nonnegative, so their balls are not empty. The upper bound $\varepsilon_{\mathrm{tr}}<2p-1$ is needed for the second claim: for larger training radii the zero vector may minimize the adversarial objective and its constant classifier has accuracy $1/2$, contrary to the printed sentence when $p>1/2$. At $p=1/2$ that constant classifier has accuracy $1/2=p$, so the case $p=1/2$ is kept for every training radius. This correction is disclosed rather than silently attributing it to the paper. Appendix D's displayed maximum outside expectation also differs from equation (2); the formalization follows (2), whose per-sample maximum has the displayed closed form. The paper's proof specializes to $\eta=4/\sqrt d$ although Theorem 2.2 states $\eta\ge4/\sqrt d$; the target retains the printed theorem's range.

Selected references

• Dimitris Tsipras, Shibani Santurkar, Logan Engstrom, Alexander Turner, and Aleksander Mądry, Robustness May Be at Odds with Accuracy, International Conference on Learning Representations, 2019. arXiv:1805.12152v5.

Motivation

Many operational decisions are linear programs whose cost vector is uncertain but partly predictable: shortest-path routing with uncertain travel times, portfolio choice with uncertain returns, shipment planning with uncertain costs. Before deciding, one observes features $X$ (traffic, market signals) correlated with the costs $Y$. Contextual linear optimization asks for a policy mapping features to decisions that minimizes the conditional expected cost, learned from past data $(X_1, Y_1), \dots, (X_n, Y_n)$.

Two families of methods compete. Estimate-then-optimize fits a regression of $Y$ on $X$ and plugs it into the optimizer. Empirical risk minimization (ERM) and its "integrated" variants choose a policy directly to minimize the empirical decision cost. A widespread view holds that the integrated approach should win because it targets the decision cost. Hu, Kallus and Mao (arXiv:2011.03030, Management Science 2022) compare the two through their regret rates. Slow, noise-independent rates of order $n^{-1/2}$ do not separate them. The separation appears under a margin (noise) condition controlling how often the problem is nearly dual-degenerate. This mission formalizes the paper's fast rate for ERM, Theorem 6.

Timeline. Margin conditions for classification go back to Mammen–Tsybakov (1999) and Tsybakov (2004); Massart–Nédélec (2006) obtained the corresponding fast rates for ERM over VC classes. El Balghiti, Elmachtoub, Grigas and Tewari (2019) gave slow generalization bounds for decision-focused losses in terms of the Natarajan dimension. Hu, Kallus and Mao (2020, revised 2021) proved the fast rate for ERM over policy classes of finite Natarajan dimension, a matching lower bound, and a faster rate for estimate-then-optimize.

Setting

The decision set is a polytope $\mathcal Z = \{z \in \mathbb R^d : Az \le b\}$, nonempty, with $\|z\| \le B$ on $\mathcal Z$ for some $B > 0$; $\mathcal Z^\angle$ is its finite set of extreme points. The pair $(X, Y) \in \mathbb R^p \times \mathbb R^d$ has $\|Y\| \le 1$, and $f^*(x) = \mathbb E[Y \mid X = x]$. The optimal set at $x$ is $\mathcal Z^*(x) = \arg\min_{z \in \mathcal Z} f^*(x)^\top z$.

A policy is a map $\pi : \mathbb R^p \to \mathcal Z^\angle$. A data-driven policy $\hat\pi$ maps a sample $\mathcal D$ of $n$ i.i.d. draws to a policy, and its regret is

$$\mathrm{Regret}(\hat\pi) = \mathbb E_{\mathcal D}\mathbb E_X\bigl[f^*(X)^\top\hat\pi(X) - \min_{z \in \mathcal Z} f^*(X)^\top z\bigr].$$

Given a class $\Pi$ of policies, $\hat\pi^{\mathrm{ERM}}_\Pi$ returns a member of $\Pi$ minimizing $\frac1n\sum_i Y_i^\top\pi(X_i)$.

The gap $\Delta(x)$ is the difference between the best value over suboptimal extreme points and the optimal value, set to $0$ when every point of $\mathcal Z$ is optimal. Assumption 2 (noise condition) with parameters $\alpha, \gamma \ge 0$ requires

$$\mathbb P_X\bigl(0 < \Delta(X) \le \delta\bigr) \le (\gamma\delta/B)^\alpha \qquad \text{for all } \delta > 0.$$

The Natarajan dimension of $\Pi$ is the largest $k$ for which there are points $x_1, \dots, x_k$ and labels $s_i \ne s'_i$ such that every pattern of choices between $s_i$ and $s'_i$ is realized by some $\pi \in \Pi$.

Formalization targets

Goal: Theorem 6

If Assumption 2 holds, $\mathbb P(|\mathcal Z^*(X)| > 1) = 0$, $\Pi$ has Natarajan dimension at most $\eta$, and $\Pi$ contains an optimal policy $\pi^*$, then for a constant $C(\alpha, \gamma)$ depending only on $\alpha, \gamma$,

$$\mathrm{Regret}(\hat\pi^{\mathrm{ERM}}_\Pi) \le C(\alpha, \gamma)\,B\left(\frac{\eta\log(|\mathcal Z^\angle| + 1)\log(n + 1)}{n}\right)^{\frac{1+\alpha}{2+\alpha}}.$$

The constant is existential and uniform over all dimensions, polytopes, distributions, classes, $\eta$ and $n$; the goal fixes no numerical value.

Milestones

With $d(\pi, \pi') = \frac1B\mathbb E_X[f^*(X)^\top(\pi'(X) - \pi(X))]$ and $d_\Delta(\pi, \pi') = \mathbb P_X(\pi(X) \ne \pi'(X))$:

1. Lemma 1: $d(\pi^*, \pi) \le 2d_\Delta(\pi^*, \pi)$ and $d_\Delta(\pi^*, \pi) \le c_1 d(\pi^*, \pi)^{\alpha/(\alpha+1)}$ with $c_1 = (\alpha\gamma^\alpha)^{-\alpha/(\alpha+1)}(\alpha+1)\gamma^\alpha$.
2. Lemma 2 (Bousquet's inequality): for a countable class bounded by $\bar H$ with second moments at most $\delta^2$, $S - \mathbb E S$ exceeds $\sqrt{2(\delta^2 + 4\bar H\mathbb E S)t/n} + 2\bar Ht/(3n)$ with probability at most $e^{-t}$.
3. Lemma 3: the localized excess-loss process satisfies $\mathbb E_{\mathcal D}[\sup_{h \in \mathcal H_\delta}(\mathbb E_n h - \mathbb E_P h)] \le (1+\sqrt2)C_0\sqrt{5\eta\log(|\mathcal Z^\angle|^2+1)\log(n+1)/n}\,\delta$ for $n$ above a threshold.
4. Tail bound (proof of Theorem 6, p. 27): for $t \ge 1$, $\mathbb P(d(\pi^*, \hat\pi^{\mathrm{ERM}}_\Pi) \ge K t(\bar V\log(n+1)/n)^{(1+\alpha)/(2+\alpha)}) \le e^{-t}$ with $\bar V = 5\eta\log(|\mathcal Z^\angle|^2+1)$ and $n \ge c\bar V\log(n+1)$.

Significance

Theorem 6 shows that the regret of ERM improves from $n^{-1/2}$ to $n^{-(1+\alpha)/(2+\alpha)}$ when the instance is rarely near dual degeneracy. With $\alpha = 1$, the generic case when $X$ has a bounded density and $f^*$ is linear, the rate is $n^{-2/3}$. Theorem 7 of the same paper (mission 2 of this series) shows that the exponent is optimal for any method that uses only the policy class. Theorem 8 (mission 3) shows that estimate-then-optimize can reach $n^{-(1+\alpha)/2}$, which is the paper's case against the conventional preference for integrated methods.

The result is proved in the paper; no machine-checked proof is known. Formalizing it adds a checked fast-rate theorem for a decision-focused learning method, a Lean statement of Bousquet's inequality in the form used throughout statistical learning theory, and a localized empirical-process bound for classes of finite Natarajan dimension.

Difficulty

The slow rate follows from uniform convergence of the empirical cost over $\Pi$. This argument cannot give more than $n^{-1/2}$: it bounds the deviation of every policy by the same worst-case amount, ignoring that near-optimal policies have small variance. The fast rate needs a variance–mean relation (Lemma 1, which is where the noise condition and the uniqueness assumption $\mathbb P(|\mathcal Z^*(X)| > 1) = 0$ enter), a concentration inequality that exploits small variance (Lemma 2), and a localized complexity bound (Lemma 3), combined over shells of the class. Lemma 2 is itself a deep result whose known proofs go through the entropy method. Lemma 3 rests on chaining and on bounding the pseudo-dimension of the excess-loss class by the Natarajan dimension, neither of which is in Mathlib.

Formalization scope

All declarations live in the namespace FastCLO.ERM. Conventions:

• Spaces are EuclideanSpace ℝ (Fin k). The polytope is a structure carrying $A$, $b$, $B > 0$, nonemptiness and the bound $\|z\| \le B$; $|\mathcal Z^\angle|$ is the cardinality of Set.extremePoints, whose finiteness is a proof obligation, not a hypothesis.
• The distribution is given by the law $\mu$ of $X$ and a Markov kernel $\kappa$ for $Y$ given $X$, with $\|Y\| \le 1$ $\kappa(x)$-almost surely for every $x$; $f^*$ is the kernel mean; data are Measure.pi of $\mu \otimes \kappa$.
• Regret is measured against the optimal value; this equals the paper's $f^*(X)^\top(\hat\pi(X) - \pi^*(X))$.
• ERM is any selection from the empirical argmin over the whole class; the paper's tie-breaking order is not encoded. The ERM rule is assumed jointly measurable in the data and the feature (an added hypothesis, so that the regret is a genuine integral).
• "$\pi^* \in \Pi$" means some member of $\Pi$ is optimal at almost every $x$; "Natarajan dimension at most $\eta$" means $\Pi$ does not shatter $\eta + 1$ points.
• Added hypotheses: $n \ge 1$ wherever the paper divides by $n$; $\bar H > 0$ in Lemma 2; measurability of the supremum in Lemma 3; $\eta \ge 1$ in the tail bound (the paper's $\epsilon_n > 0$). Constants ($C$, $C_0$, $K$, $c$) are quantified before everything they are uniform over.

A statement in which the regret integrated the empirical cost instead of $f^*$, or in which ERM minimized over a subset of the class, or in which the constant could depend on the instance, would be a different theorem; the Lean statements rule these out by construction.

Needed infrastructure: Bousquet's (or Talagrand's) inequality, symmetrization and Dudley chaining for empirical processes, packing bounds for classes of finite pseudo-dimension, and the Natarajan-to-pseudo-dimension reduction. These are reusable far beyond this mission; contributions of any of them are welcome.

Selected references

• Y. Hu, N. Kallus, X. Mao, Fast Rates for Contextual Linear Optimization, Management Science, 2022; arXiv:2011.03030v3, 2021. https://arxiv.org/abs/2011.03030
• O. Bousquet, A Bennett concentration inequality and its application to suprema of empirical processes, Comptes Rendus Mathématique 334(6), 2002. https://doi.org/10.1016/S1631-073X(02)02292-6
• P. Massart, É. Nédélec, Risk bounds for statistical learning, Annals of Statistics 34(5), 2006. https://doi.org/10.1214/009053606000000786
• A. B. Tsybakov, Optimal aggregation of classifiers in statistical learning, Annals of Statistics 32(1), 2004. https://doi.org/10.1214/aos/1079120131
• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, NeurIPS 2019; arXiv:1905.11488. https://arxiv.org/abs/1905.11488
• B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

Why prices built from self-exciting order flow

High-frequency prices move by discrete ticks, and successive moves are strongly correlated: an upward tick tends to be followed by a downward one. Bacry, Delattre, Hoffmann and Muzy (BDHM12, BDHM13b) proposed to model the upward and downward price jumps as the two components of a bidimensional Hawkes process, a pair of counting processes in which every event raises the rate of future events of both kinds. In this model the price is the difference $N^{+}-N^{-}$, and its microstructure features (discreteness, negative autocorrelation of increments) are built in. Under the stability condition $\int\phi_1+\int\phi_2<1$ on the excitation kernels, the price rescaled over long horizons converges to a Brownian motion with a constant volatility BDHM12.

Empirical calibrations of Hawkes models on financial data, however, find kernel norms (branching ratios) very close to the critical value $1$ (HBB13, FS12). Jaisson and Rosenbaum (JR15) study exactly this regime: a sequence of models whose stability condition is almost violated, observed over a time horizon of the right order. Their Theorem 3.1 shows that the rescaled price then converges to a Heston-type process, a Brownian motion time-changed by a Cox–Ingersoll–Ross (CIR) variance. This gives a microstructural foundation for stochastic volatility models of Heston type Hes93, which are standard in option pricing.

Setting

Fix $\mu>0$ and two nonnegative measurable kernels $\phi_1,\phi_2$ on $\mathbb R_+$ with $\int_0^\infty(\phi_1+\phi_2)=1$, finite mean $m=\int_0^\infty s(\phi_1+\phi_2)(s)\,ds$, $\phi_2$ nonzero on a set of positive measure, and differentiable with bounded integrable derivatives (Assumption 3). Let $(a_T)$ be positive numbers with $a_T<1$, $a_T\to1$, and set $\phi^T_i=a_T\phi_i$.

For each observation horizon $T$ (along a sequence $T\to\infty$), the bidimensional Hawkes process $(N^{T+},N^{T-})$ is a pair of counting processes started at $0$, with unit jumps and no common jumps, whose intensities with respect to their joint history are

$$\lambda^{T+}_t=\mu+\int_0^t\phi^T_1(t-s)\,dN^{T+}_s+\int_0^t\phi^T_2(t-s)\,dN^{T-}_s,\qquad \lambda^{T-}_t=\mu+\int_0^t\phi^T_2(t-s)\,dN^{T+}_s+\int_0^t\phi^T_1(t-s)\,dN^{T-}_s .$$

"Intensity" means: for $0\le a<b\le T$ and every event $A$ of the history up to time $a$, $\mathbb E[(N^{T\pm}_b-N^{T\pm}_a)\mathbf 1_A]=\mathbb E[\int_a^b\lambda^{T\pm}_s\mathbf 1_A\,ds]$.

The renormalized price is

$$P^T_t=\frac1T\big(N^{T+}_{Tt}-N^{T-}_{Tt}\big),\qquad t\in[0,1].$$

Two further conditions fix the regime. Display (3): $T(1-a_T)\to\lambda$ for some $\lambda>0$. Assumption 4: with $\psi^T_+=\sum_{k\ge1}(a_T(\phi_1+\phi_2))^{*k}$ and $\rho^T(x)=T\psi^T_+(Tx)/\|\psi^T_+\|_1$, there is $K_\rho$ with $|\rho^T(x)|\le K_\rho$ for all $x\ge0$ and all $T$. Write $\phi=\phi_1-\phi_2$ and $\|\phi\|_1=\int_0^\infty(\phi_1-\phi_2)$.

Formalization targets

Goal: Theorem 3.1

Under (3) and Assumptions 3 and 4, $P^T$ converges in law, for the Skorohod topology on $[0,1]$, to the process $P$ defined by

$$dC_t=\Big(\frac{2\mu}{\lambda}-C_t\Big)\frac{\lambda}{m}\,dt+\frac1m\sqrt{C_t}\,dB^1_t,\quad C_0=0,\qquad dP_t=\frac{1}{1-\|\phi\|_1}\sqrt{C_t}\,dB^2_t,\quad P_0=0,$$

with $(B^1,B^2)$ a two-dimensional Brownian motion. The goal asserts that this system has a solution and that $P^T$ converges in law to the $P$-coordinate of every solution.

Milestones

In the order of the proof (§4.4):

1. Display (11): $N^{T+}_t-N^{T-}_t=\int_0^t(1+\Psi^T(t-u))(dM^{T+}_u-dM^{T-}_u)$, with $\psi^T$ the resolvent of $\phi^T_1-\phi^T_2$, $\Psi^T(x)=\int_0^x\psi^T$ and $M^{T\pm}$ the compensated counting processes.
2. Lemma 4.12: $X^T_s=(\lambda^{T+}_{sT}-\lambda^{T-}_{sT})/T\to0$ uniformly in probability on $[0,1]$.
3. Lemma 4.13: the brackets of $(B^1)^T=\int_0^{\cdot T}\frac{dM^{T+}+dM^{T-}}{\sqrt{T(\lambda^{T+}+\lambda^{T-})}}$ and $(B^2)^T$ (same with $dM^{T+}-dM^{T-}$) satisfy $[(B^i)^T,(B^j)^T]_t\to t\mathbf 1_{i=j}$ in probability.
4. Lemma 4.14: $((B^1)^T,(B^2)^T)\Rightarrow(B^1,B^2)$ jointly.
5. Lemma 4.15: $(C^T,(B^2)^T)\Rightarrow(C,B^2)$ jointly, with $C^T_t=(\lambda^{T+}_{tT}+\lambda^{T-}_{tT})/T$, $C$ the CIR process above and $B^2$ independent of $C$.
6. Lemma 4.16: $R^T_t=\int_0^t\int_{T(t-u)}^\infty\psi^T\,d(\overline M^{T+}_u-\overline M^{T-}_u)\to0$ u.c.p.
7. Lemma 4.17: $\int_0^\infty\int_x^\infty\phi_i(s)\,ds\,dx<\infty$.
8. The Step 6 decomposition of $P^T_t$ into a multiple of $\overline M^{T+}_t-\overline M^{T-}_t$, minus $R^T_t$, minus a vanishing multiple of $\overline M^{T+}_t-\overline M^{T-}_t$.

Significance

The theorem identifies the scaling limit of a microstructure price model at near-criticality, and the limit is not a Brownian motion with constant volatility but a stochastic-volatility process: the variance $C$ is itself a CIR diffusion driven by a Brownian motion independent of the one driving the price. It explains, from the order-flow level, why Heston-type dynamics arise at macroscopic scales, and it identifies which features of the microscopic excitation survive in the macroscopic volatility and price diffusion.

The result is proved in the paper; nothing about it is open. It has not been formalized. A machine-checked version would formalize a complete scaling-limit argument for point processes: the resolvent calculus of Hawkes processes, the martingale central limit theorem for pure-jump martingales, joint Skorohod convergence, and the identification of the limit of stochastic integrals. Each of these is reusable well beyond this paper.

Difficulty

The price is a difference of two processes whose sum is nearly unstable. One might expect the CIR limit of the one-dimensional case (Theorem 2.2 of the same paper, applied to $N^{T+}+N^{T-}$) to give the result directly. It does not: the price is driven by the difference of the martingales, with a volatility that depends on the sum of the intensities, and the limit requires the joint convergence of the variance proxy $C^T$ and the price martingale $(B^2)^T$, with one time change for both coordinates. Marginal convergence of each coordinate is not enough to pass to the limit in $\int\sqrt{C^T}\,d(B^2)^T$. Joint convergence in turn needs the cross-bracket of $(B^1)^T$ and $(B^2)^T$ to vanish, which depends on the imbalance $X^T$ being negligible (Lemma 4.12), and the zero set of the CIR process having Lebesgue measure zero. The signed kernel $\phi_1-\phi_2$ produces a signed resolvent, for which the positivity arguments of the one-dimensional case are unavailable.

Formalization scope

• Asymptotics. $T$ runs along a sequence $T_n\to\infty$; each Hawkes pair lives on its own probability space.
• Hawkes pair. Time is real with all conditions imposed for $t\ge0$; $N^{T\pm}$ are $\mathbb N$-valued, nondecreasing, right-continuous, with unit jumps and no common jumps. The filtration is the joint natural filtration. The intensity identity is stated with lower Lebesgue integrals in $[0,\infty]$, so no integrability is assumed silently. The intensity counts jumps at $s\le t$ (cadlag); inside stochastic integrands ($(B^i)^T$, brackets) its left limit is used.
• Integrals. Integrals against $dN$ and $dM$ have deterministic or predictable integrands and are written pathwise, as sums over jump times minus Lebesgue integrals. Brackets are sums of products of jumps.
• $\|\phi\|_1$ is the signed integral $\int(\phi_1-\phi_2)$, the value the proof uses (Step 6, p. 31). It coincides with the $L^1$ norm when $\phi_1\ge\phi_2$; reading it as $\int|\phi_1-\phi_2|$ would give a different limit when $\phi_1-\phi_2$ changes sign.
• Convergence in law for the Skorohod topology on $[0,1]$ is stated in coupling form (copies of the laws converging almost surely in $D[0,1]$), equivalent to weak convergence on the Polish space $D[0,1]$. Joint statements use $\mathbb R^2$-valued paths with one time change.
• Limit SDEs use the published Ethier–Kurtz substrate (EthierKurtz.SolvesBrownianSDE, IsStandardBrownian, state space $\mathbb R^2$): strong solutions, global in time, restricted to $[0,1]$. "The process defined by" the system is encoded as existence of a solution plus convergence to every solution.

The formalization rules out the trivializing readings: the Hawkes predicate follows p. 5 clause by clause and is satisfied by a pair of independent Poisson processes when $\phi_i\equiv0$, so it is not vacuous; the kernels are $\phi^T_i=a_T\phi_i$, not $\phi_i$; the limit is pinned by its equation, its coefficients and its initial value, not "some process"; and the convergence is in the Skorohod topology, not of finite-dimensional laws only.

Needed infrastructure: convolution powers and resolvents on $\mathbb R_+$, pathwise Stieltjes integrals against counting processes, the martingale property of compensated Hawkes processes, a martingale functional CLT for pure-jump martingales, Skorohod-topology tools on $D[0,1]$, and convergence of stochastic integrals under joint convergence. The one-dimensional CIR limit (mission 2 of this series) is used inside Lemma 4.15; the definitions are restated here. The martingale functional CLT used for Lemma 4.14 is Theorem VIII.3.11 of Jacod and Shiryaev (1987), as cited in JR15. Contributions to any milestone, or to reusable lemmas they need, are welcome.

Selected references

• [JR15] T. Jaisson, M. Rosenbaum, Limit theorems for nearly unstable Hawkes processes, Ann. Appl. Probab. 25(2):600–631, 2015. arXiv:1310.2033v2, https://arxiv.org/abs/1310.2033 ; https://doi.org/10.1214/14-AAP1005
• [BDHM12] E. Bacry, S. Delattre, M. Hoffmann, J.-F. Muzy, Scaling limits for Hawkes processes and application to financial statistics, preprint, 2012. https://arxiv.org/abs/1202.0842
• [BDHM13b] E. Bacry, S. Delattre, M. Hoffmann, J.-F. Muzy, Modelling microstructure noise with mutually exciting point processes, Quant. Finance 13(1):65–77, 2013. https://doi.org/10.1080/14697688.2011.647054
• [HBB13] S. J. Hardiman, N. Bercot, J.-P. Bouchaud, Critical reflexivity in financial markets: a Hawkes process analysis, preprint, 2013. https://arxiv.org/abs/1302.1405
• [FS12] V. Filimonov, D. Sornette, Quantifying reflexivity in financial markets: toward a prediction of flash crashes, Phys. Rev. E 85:056108, 2012. https://doi.org/10.1103/PhysRevE.85.056108
• [Hes93] S. L. Heston, A closed-form solution for options with stochastic volatility with applications to bond and currency options, Rev. Financ. Stud. 6(2):327–343, 1993. https://doi.org/10.1093/rfs/6.2.327

Motivation

An event stream can raise its own future event rate. A Hawkes process models this feedback by adding to a baseline rate the effects of past arrivals. The parameter measuring total excitation can approach its stability boundary, at which long clusters make a fixed time scale an unreliable guide to the observed count. Jaisson and Rosenbaum identify a regime in which observation time and the distance to that boundary balance, leaving a stochastic limit rather than a deterministic average Jaisson and Rosenbaum, 2015. Their theorem gives a precise bridge from an event count with jumps to a continuous square-root diffusion. The paper notes a practical reason for this bridge: intermediate-scale inference can use diffusion methods to estimate the baseline rate and two aggregate kernel parameters, though it cannot recover the entire excitation kernel Jaisson and Rosenbaum, §2.4, p. 10.

Setting

For each observation horizon $T$, let $N^T_t$ count events up to time $t$, with $N^T_0=0$. The process is observed on $[0,T]$ and has intensity

$$\lambda^T_t=\mu+\int_0^t\phi^T(t-s)\,dN^T_s, \qquad \phi^T=a_T\phi,$$

where $\mu>0$ is the baseline rate. The integral against $N^T$ is a sum over its unit jumps. The nonnegative kernel $\phi$ has total mass one and finite mean $m=\int_0^\infty s\phi(s)\,ds$; its derivative is bounded and integrable. The coefficients satisfy $0<a_T<1$ and $a_T\to1$. Thus $a_T$ is the total mass of $\phi^T$, and the model approaches the stability boundary from below. The natural filtration is generated by the observed count. The intensity relation is the identity for conditional expected increments on every interval $0\le a<b\le T$ and every event observable at time $a$ Jaisson and Rosenbaum, §2.1, p. 5.

The resolvent $\psi^T=\sum_{k\ge1}(\phi^T)^{*k}$ collects excitation across repeated generations. Its rescaled density is $\rho^T(x)=T\psi^T(Tx)/\|\psi^T\|_1$. The mission uses the paper's additional bound $\sup_{T,x\ge0}|\rho^T(x)|<\infty$ and the balance condition $T(1-a_T)\to\lambda>0$. Here $\lambda$ is a fixed limiting parameter, distinct from the time-dependent intensity $\lambda^T_t$. The processes to be compared on a common interval are

$$C^T_t=(1-a_T)\lambda^T_{tT},\qquad V^T_t=\frac{1-a_T}{T}N^T_{tT},\qquad 0\le t\le1.$$

Formalization targets

The main target is Theorem 2.2, p. 10: $C^T$ converges in law in the Skorohod topology on $D[0,1]$ to the unique strong solution, started at zero, of the Cox–Ingersoll–Ross equation

$$X_t=\int_0^t(\mu-X_s)\frac{\lambda}{m}\,ds +\frac{\sqrt\lambda}{m}\int_0^t\sqrt{X_s}\,dB_s.$$

Separately, $V^T$ converges in law in the same path topology to $t\mapsto\int_0^tX_s\,ds$. These are two convergence claims, each on its own path space law. The statement also asserts that the strong solution exists, so convergence to “every solution” cannot hold merely because there are no solutions.

The supporting targets follow the paper's stated results. Lemma 4.1 and Proposition 2.1 identify the resolvent renewal identity and the intensity's resolvent form; both are supporting theorem items. Lemmas 4.2–4.5 give separation and decay estimates for the plus-sign Fourier transforms of $\phi$ and $\rho^T$, followed by $L^2$ convergence of $\rho^T$ to the exponential density $(\lambda/m)e^{-x\lambda/m}$. Lemma 4.9 gives a fourth-moment increment bound for the paper's residual process $Y^T$, and Proposition 4.1 states that $Y^T$ tends to zero uniformly in probability on $[0,1]$. The latter six are source-stated milestones, with their pages and texts recorded separately.

Significance

The theorem identifies the scale at which a nearly unstable event model retains random dynamics. It also identifies the diffusion coefficients: the drift relaxes toward $\mu$ at rate $\lambda/m$, and the noise has coefficient $\sqrt\lambda/m$ times the square root of the current intensity. The second convergence claim transfers this intensity behavior to accumulated events. Those coefficients make the limit more informative than a statement that merely names a generic continuous process Jaisson and Rosenbaum, Theorem 2.2.

The result is proved in the paper but has no matching published Hawkes formalization in the local Prove2Me index used for this mission. Machine-checked definitions for Brownian motion and strong SDE solutions from the Ethier–Kurtz development are already available and referenced here. The new formal work is the Hawkes model, its path-space convergence, the density estimates, and the limit theorem itself. Formalizing the stated milestones would also leave reusable analytic and probability interfaces for other nearly unstable point-process limits.

Difficulty

Pointwise convergence of an intensity or of finitely many observations does not control its law as a cadlag path. Excitation also couples each event to later events, so a direct independent-increment argument is unavailable. The resolvent has to be controlled at the observation scale, including its high-frequency behavior, while the stochastic remainder has to be controlled uniformly over time. The final limit is a square-root SDE: its coefficient is not globally Lipschitz at zero, and a claim about its law must keep the initial condition and Brownian driver explicit Jaisson and Rosenbaum, §§4.2–4.3.

Formalization scope

The horizon $T$ is a positive real sequence tending to infinity, as the paper's footnote specifies; $a_T$ is a sequence in $(0,1)$ tending to one. Each index may have its own probability space. The count is natural-number valued, nondecreasing, right-continuous, starts at zero, and has unit jumps. Its filtration is generated by evaluations of $N^T$. The intensity identity uses extended nonnegative integrals, avoiding an arbitrary real value for an infinite expectation. The right-continuous intensity includes an event at the current time, so $C^T$ is cadlag. Its predictable left-limit version is available for stochastic integrands. All results use the half-line kernel and $\phi^T=a_T\phi$; they never replace it by $\phi$ in the Hawkes process.

Skorohod convergence is represented by a coupling whose cadlag paths approach each other after increasing homeomorphic time changes of $[0,1]$. This is the representation form of weak convergence in $D[0,1]$ with the $J_1$ topology. The limit SDE uses the published global strong-solution predicate, then restricts its paths to $[0,1]$. Its drift is exactly $(\mu-x)\lambda/m$ and diffusion exactly $(\sqrt\lambda/m)\sqrt{x}$; Real.sqrt on negative arguments does not affect its nonnegative solution. The renewal theorem item additionally makes the unknown $f$ measurable and locally bounded so its real convolution integral has its stated meaning. Fourier denominators exclude zero explicitly, while the zero-frequency bound is stated separately. The density convergence uses an extended nonnegative squared integral, and uniform probability convergence uses an extended supremum. These choices rule out default-zero values, a vacuous Hawkes class, a free limit process, and finite-dimensional convergence in place of path convergence.

The development needs half-line convolution and summable resolvents, natural filtrations and compensated point processes, Fourier bounds, cadlag path laws, and Itô SDEs. The convolution, path-space, and point-process interfaces are suitable for reuse. Contributions should preserve the exact hypotheses, constants, and two distinct convergence conclusions of the source theorem.

Selected references

• T. Jaisson and M. Rosenbaum, Limit theorems for nearly unstable Hawkes processes, Annals of Applied Probability 25(2), 2015, arXiv:1310.2033v2. Preprint; DOI.