Statistics

Contextual bandits and the reduction to regression

A contextual bandit is a sequential decision problem: in each round a learner sees a context (a user's features, a patient's covariates), picks one of $K$ actions, and observes the reward of that action only. Applications include recommendation, dynamic pricing and adaptive clinical decisions. The difficulty is statistical and computational at once: the learner must explore to learn which action is best for which context, and the class of models it learns over is typically huge.

A long-standing question was whether contextual bandits can be solved optimally with nothing more than an offline regression oracle, a black-box supervised learning routine that fits a predictor of rewards to i.i.d. data. Earlier optimal algorithms either required a cost-sensitive classification oracle called many times per round (the "monster" of Agarwal et al., 2014) or an online regression oracle that must handle adversarially generated data (Foster and Rakhlin, 2020). Simchi-Levi and Xu (2022) answered the question with FALCON+, which calls an arbitrary offline regression oracle once per epoch, $O(\log T)$ or $O(\log\log T)$ times in total, and whose regret is governed by the oracle's estimation error.

Timeline:

• 2014: Agarwal, Hsu, Kale, Langford, Li and Schapire, Taming the Monster: optimal regret with $\tilde O(\sqrt{KT})$ calls to a classification oracle.
• 2020: Foster and Rakhlin, Beyond UCB: SquareCB, optimal regret with an online regression oracle, via inverse gap weighting.
• 2020 (arXiv) / 2022 (journal): Simchi-Levi and Xu, FALCON and FALCON+: optimal regret with an offline regression oracle.

Setting

There is a finite set $\mathcal A$ of $K$ actions and a set $\mathcal X$ of contexts. In round $t$ nature draws a context $x_t$ and a reward vector $r_t\in[0,1]^{\mathcal A}$ from a fixed unknown distribution $\mathcal D$; the learner sees $x_t$, picks $a_t$ and observes $r_t(a_t)$. The conditional mean reward is $f^*(x,a)=\mathbb E[r_t(a)\mid x_t=x]$, and $\pi_{f^*}(x)$ is an action maximizing $f^*(x,\cdot)$. The regret after $T$ rounds is

$$\sum_{t=1}^T\big(r_t(\pi_{f^*}(x_t))-r_t(a_t)\big).$$

An action selection kernel $p(a\mid x)$ gives a probability distribution over actions for each context. The offline regression oracle $\mathrm{OffReg}_{\mathcal F}$ takes $n$ samples $(x_i,a_i,r_i(a_i))$ and returns a predictor $\hat f:\mathcal X\times\mathcal A\to\mathbb R$. It satisfies Assumption 2 with error function $\mathcal E_{\mathcal F,\delta}(n)$ if, for every kernel $p$, when the samples are i.i.d. with $(x_i,r_i)\sim\mathcal D$ and $a_i\sim p(\cdot\mid x_i)$, then with probability at least $1-\delta$,

$$\mathbb E_{x\sim\mathcal D_{\mathcal X},\,a\sim p(\cdot\mid x)}\big[(\hat f(x,a)-f^*(x,a))^2\big]\le\mathcal E_{\mathcal F,\delta}(n).$$

FALCON+ runs in epochs given by a schedule $0=\tau_0<\tau_1<\tau_2<\cdots$. In epoch $m$ it sets $\gamma_1=1$ and $\gamma_m=\tfrac12\sqrt{K/\mathcal E_{\mathcal F,\delta/(2m^2)}(\tau_{m-1}-\tau_{m-2})}$ for $m\ge2$; it obtains $\hat f_m$ by feeding only the data of epoch $m-1$ to the oracle ($\hat f_1\equiv0$); and in every round $t$ of the epoch it plays

$$p_t(a)=\frac{1}{K+\gamma_m\big(\hat f_m(x_t,\hat a_t)-\hat f_m(x_t,a)\big)}\ \ (a\ne\hat a_t),\qquad p_t(\hat a_t)=1-\sum_{a\ne\hat a_t}p_t(a),$$

where $\hat a_t$ maximizes $\hat f_m(x_t,\cdot)$. The epoch of round $t$ is $m(t)=\min\{m\ge1:t\le\tau_m\}$.

Formalization targets

Goal: Theorem 2 in explicit form

If $\tau_m\ge2^m$ and $\gamma_1\le\cdots\le\gamma_{m(T)}$ for $m\le m(T)$, then for every $T\ge1$ and $\delta>0$, with probability at least $1-\delta$,

$$\sum_{t=1}^T\big(r_t(\pi_{f^*}(x_t))-r_t(a_t)\big)\le 14.3\sum_{m=2}^{m(T)}\sqrt{K\,\mathcal E_{\mathcal F,\delta/(2m^2)}(\tau_{m-1}-\tau_{m-2})}\,(\tau_m-\tau_{m-1})+\tau_1+\sqrt{8T\log(2/\delta)}.$$

The paper states Theorem 2 as an $O(\cdot)$ bound; this is the explicit inequality its proof establishes, with the additive terms kept. It holds for every oracle, error function and schedule satisfying the hypotheses, so it is the shape of the result rather than a rate for a particular class.

Milestones

In attack order: Lemma A.2 (each oracle call is accurate with probability $1-\delta/(2m^2)$; the good event $\Gamma_2$ has probability $1-\delta/2$); Lemma A.3 (the kernel $p_m$ is induced by a randomized policy $Q_m$ on $\Psi=\mathcal A^{\mathcal X}$); Lemma A.4 (the conditional expected regret of a round is the implicit regret of $Q_{m(t)}$); Lemmas A.5 and A.6 (low predicted regret and bounded divergence $V(p_m,\pi)\le K+\gamma_m\widehat{\mathrm{Reg}}(\pi)$); Lemma A.7 (prediction error of implicit rewards on $\Gamma_2$); Lemma A.8 (true and predicted implicit regret agree up to factor 2 and $5.15K/\gamma_m$); Lemma A.9 ($\sum_\pi Q_m(\pi)\mathrm{Reg}(\pi)\le7.15K/\gamma_m$); Lemma A.10 in expectation; the Azuma display (A.10); and Lemma A.10 with high probability.

Significance

Theorem 2 makes contextual bandits reducible to offline regression with no loss in rate: for any function class with an estimation-error bound, plugging that bound into the theorem gives the regret. With empirical entropy $O(\varepsilon^{-p})$ this yields $O(T^{(1+p)/(2+p)}\log T)$, matching the known lower bound, and for linear classes it improves the best known bound when $K\ll T$ (Examples 1–2 of the paper). The oracle is called once per epoch on i.i.d. data, so any off-the-shelf supervised learner can be used, with a guarantee transferred automatically.

Formalizing the result produces a machine-checked offline-to-online reduction, independent of the function class. The paper's result is proved, but it has no machine-checked proof; the platform has formal statements for the online-oracle algorithm SquareCB and for the classification-oracle algorithm of Agarwal et al., not for this reduction. The milestones isolate reusable facts about inverse-gap-weighted kernels (Lemmas A.3, A.5, A.6) and an epoch-wise induction pattern (Lemma A.8) that recur in later work on bandits and reinforcement learning with regression oracles.

Difficulty

The obvious argument fails at the regression step. A natural approach feeds all past data to the oracle, but those data are adaptively collected and not i.i.d., so an offline guarantee does not apply to them; FALCON+ uses only the previous epoch's data, which are i.i.d. given the past, and the analysis must make this conditional application of Assumption 2 rigorous on a product space (Lemma A.2). The second obstacle is that the oracle's error is measured under the kernel of the previous epoch, while regret is incurred under the current one. Transferring the error across epochs requires the divergence $V(p,\pi)$ and the two-sided comparison of true and predicted implicit regret in Lemma A.8, proved by induction on epochs with exact constants; a one-sided bound does not close the induction.

Formalization scope

Lean representation and conventions:

• Finite contexts. $\mathcal X$ is a Fintype with the discrete σ-algebra. The paper claims Theorem 2 for arbitrary $\mathcal X$, but its detailed proof (App. A.1–A.6) is "under the condition that $|\mathcal X|<\infty$"; the uncountable case (App. A.7) is not formalized. No bound depends on $|\mathcal X|$.
• Rewards in $[0,1]$, the model of §1.2 and the assumption of the proof of Theorem 2. Setup 2's heavy-tailed generality (Condition (5)) is not formalized.
• Nature's law is a context marginal $\mathcal D_{\mathcal X}$ with a Markov reward kernel; $f^*(x,a)$ is the kernel mean.
• The run lives on the canonical space $\mathbb N\to(\mathcal X\times\mathbb R^{\mathcal A})\times[0,1]$ with the i.i.d. product law of $\mathcal D\otimes\mathrm{Uniform}[0,1]$; actions are drawn by the inverse CDF from the uniform coordinate.
• Probabilities in failure form: "with probability at least $1-\delta$" is "the failure set has outer measure at most $\delta$".
• Added hypotheses (disclosed in every statement): $\mathcal E_{\mathcal F,\delta}(n)>0$ (Algorithm 2 divides by it); measurability of the oracle and of the tie-breaking rule for $\hat a_t$ (App. A.7, p. 1929, assumes such conditions directly); $\delta>0$; $T\ge1$.
• The tie-breaking rule for $\hat a_t$ and the maximizer $\pi_{f^*}$ are universally quantified.
• Quantities the paper indexes by a round $t$ are indexed by its epoch; $\Upsilon_{t-1}$ is replaced by the coordinate filtration, which contains it.

A trivializing formalization is ruled out: the goal is a bound on the realized regret of the run of Algorithm 2, whose oracle sees only $(x,a,r(a))$ samples of the previous epoch; it is not a bound for an algorithm that is handed $f^*$ or its population error, or that observes the full reward vector.

Infrastructure needed: conditional application of an i.i.d. guarantee inside a product measure (Fubini over Measure.infinitePi), Azuma–Hoeffding for bounded martingale differences (proved on the platform as bounded_diff_martingale_two_sided), and finite-sum algebra for inverse gap weighting. The kernel lemmas A.3, A.5 and A.6 are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.

Selected references

• D. Simchi-Levi and Y. Xu, Bypassing the Monster: A Faster and Simpler Optimal Algorithm for Contextual Bandits Under Realizability, Mathematics of Operations Research 47(3):1904–1931, 2022. https://doi.org/10.1287/moor.2021.1193
• D. J. Foster and A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML 2020. https://arxiv.org/abs/2002.04926
• A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li and R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014. https://arxiv.org/abs/1402.0555

Motivation

A chance-constrained program asks for a decision that satisfies uncertain constraints with high probability rather than surely:

$$\min_{x\in X} f(x) \quad\text{s.t.}\quad \mathbb P\bigl(c_j(x,\xi)\le 0,\ j=1,\dots,m\bigr)\ge 1-\alpha. \tag{1.1}$$

Such models appear in power-system operation, portfolio selection, chemical-process and reservoir management, and other settings where requiring the constraints for every realization is too conservative (Nemirovski–Shapiro 2006; the paper's introduction lists applications). The probability is rarely available in closed form, and when the distribution of $\xi$ is only accessible through samples, the feasible set of the empirical counterpart is a union of polyhedral-like pieces: it is non-smooth and non-convex, and the empirical quantile introduces many spurious local minima (Peña-Ordieres, Luedtke, Wächter 2020, §2).

Peña-Ordieres, Luedtke and Wächter replace the indicator inside the empirical probability by a smooth kernel with bandwidth $\varepsilon$, which turns the sample constraint into a differentiable one suitable for nonlinear programming solvers. This mission formalizes the paper's consistency result: as the sample size grows and the bandwidth shrinks, jointly, the optimal values and optimal solutions of the smoothed sample problem converge to those of the true problem with probability one.

Timeline. Consistency of sample approximations of chance constraints with the plain empirical cdf goes back to Pagnoncelli, Ahmed, Shapiro 2009 (reference [36] of the paper; its Propositions 2.1 and 2.2). Luedtke–Ahmed 2008 gave finite-sample feasibility guarantees for the same empirical approximation. Convergence with respect to a smoothing parameter alone was studied by Geletu, Hoffmann, Klöppel and Li (SIAM J. Optim. 27, 2017), Hong, Yang, Zhang 2011 and Hu, Hong and Zhang (IIE Trans. 45, 2013) (references [15], [25], [26] of the paper). Peña-Ordieres–Luedtke–Wächter 2020 (SIAM J. Optim. 30(3)) treat both parameters simultaneously; Theorem 3.5 of the preprint arXiv:1905.07377v2 is the result posed here.

Setting

Decisions are vectors $x\in\mathbb R^n$ restricted to a closed set $X$. The random data $\xi$ takes values in a measurable space $\Xi$ with law $\mathbb P_\xi$. The constraints are aggregated into one scalar function $C(x,\xi)=\max_j c_j(x,\xi)$, and the risk level is $\alpha\in(0,1)$.

• True distribution function. $F(t;x)=\mathbb P_\xi(C(x,\xi)\le t)$. The true feasible region is $X_\alpha=\{x\in X\mid F(0;x)\ge 1-\alpha\}$; the optimal solution set and value of (1.1) are $S$ and $v^*$.
• Smoothed indicator. For $\varepsilon>0$, $\Gamma_\varepsilon(y)$ equals $1$ for $y\le-\varepsilon$, $0$ for $y\ge\varepsilon$, and $\gamma_\varepsilon(y)$ in between, where $\gamma_\varepsilon:[-\varepsilon,\varepsilon]\to[0,1]$ is strictly decreasing, symmetric ($\gamma_\varepsilon(-y)=1-\gamma_\varepsilon(y)$), and makes $\Gamma_\varepsilon$ differentiable. The paper's concrete choice is the quartic kernel (2.6).
• Smoothed distribution functions. $F_\varepsilon(t;x)=\int\Gamma_\varepsilon(C(x,\xi)-t)\,d\mathbb P_\xi$, and, for an i.i.d. sample $\xi_1,\dots,\xi_N$,

$$F^N_\varepsilon(t;x)=\frac1N\sum_{i=1}^N\Gamma_\varepsilon\bigl(C(x,\xi_i)-t\bigr).$$

• Smoothed sample problem (2.4). $\min_{x\in X} f(x)$ subject to $F^N_\varepsilon(0;x)\ge1-\alpha$, with optimal solution set $S^N_\varepsilon$ and value $v^N_\varepsilon$.

The standing assumptions are: Assumption 3.1, for each $x\in X$ the random variable $C(x,\xi)$ has a continuous distribution; Assumption 3.2, $C$ is Carathéodory, i.e. $C(x,\cdot)$ is measurable for each $x\in X$ and $C(\cdot,\xi)$ is continuous for almost every $\xi$; Assumption 3.3, some optimal solution $\bar x$ of (1.1) is a limit of points $x\in X$ with $F(0;x)>1-\alpha$.

Formalization targets

Goal: Theorem 3.5

If $X$ is compact, $f$ is continuous and Assumptions 3.1–3.3 hold, then with probability one, as $N\to\infty$ and $\varepsilon\to0$ jointly,

$$S^N_\varepsilon\neq\emptyset\ \text{eventually},\qquad v^N_\varepsilon\to v^*,\qquad \mathbb D(S^N_\varepsilon,S)=\sup_{x\in S^N_\varepsilon}\operatorname{dist}(x,S)\to0 .$$

Milestones

1. Uniform law of large numbers (proof of Theorem 3.4): w.p.1, $\sup_{\varepsilon\in(0,1]}\sup_{x\in U}|F^N_\varepsilon(0;x)-F_\varepsilon(0;x)|\to0$ as $N\to\infty$, for compact $U\subseteq X$.
2. Removal of the smoothing (proof of Theorem 3.4): $\sup_{x\in U}|F_\varepsilon(0;x)-F(0;x)|\to0$ as $\varepsilon\to0^+$.
3. Theorem 3.4: w.p.1, $\sup_{x\in U}|F^N_\varepsilon(0;x)-F(0;x)|\to0$ as $N\to\infty$ and $\varepsilon\to0$.
4. Eventual nonemptiness of $S^N_\varepsilon$ (proof of Theorem 3.5).
5. (3.3): $\liminf v^N_\varepsilon\ge v^*$ w.p.1.
6. (3.4): $\limsup v^N_\varepsilon\le v^*$ w.p.1.

Significance

Theorem 3.5 justifies solving the smooth problem (2.4) in place of (1.1): with enough samples and a small enough bandwidth, global solutions of the surrogate approximate global solutions of the chance-constrained program, and the optimal values agree in the limit. Unlike earlier results it controls the two approximation errors, sampling and smoothing, at once, so no order of limits has to be chosen in practice. It is the asymptotic counterpart of the paper's finite-sample feasibility bound (Theorem 3.13) and the theoretical basis for the trust-region method of §5.

The result is proved in the paper, with two steps imported from Shapiro–Dentcheva–Ruszczyński, second edition (a uniform law of large numbers, Theorem 7.53, and a convergence-of-expectations result, Theorem 4.91) and the deviation statement deferred to Theorem 5.3 there. None of these results, and no consistency theorem for sample approximations of chance constraints, is machine-checked on Prove2Me or, as far as is known, elsewhere. A formal proof requires writing the imported steps out for the specific integrands of this problem and completing the solution-set argument the paper leaves to the reference.

Difficulty

The pointwise statements are routine; the uniformity is not. The integrand $\Gamma_\varepsilon(C(x,\xi))$ converges, as $\varepsilon\to0$, to the indicator $\mathbf 1\{C(x,\xi)\le0\}$, which is discontinuous in $x$ wherever $C(x,\xi)=0$. A uniform law of large numbers for a family that degenerates into indicators needs the no-atom Assumption 3.1 at every point of $U$, not only at the limit. Moreover, the smoothing functions $\gamma_\varepsilon$ for different $\varepsilon$ are unrelated, so the family is not continuous in $\varepsilon$, and a Glivenko–Cantelli argument over a joint parameter $(x,\varepsilon)$ cannot be applied directly. The convergence of solution sets needs, in addition, that the limit of feasible points of (2.4) is feasible for (1.1), which uses the continuity of $F(0;\cdot)$ on $X$; that continuity again rests on Assumptions 3.1 and 3.2.

Formalization scope

• Decisions are Fin n → ℝ with the sup norm. Assumption 3.3 is stated for every radius, so the norm choice does not change it.
• The sample is an infinite sequence ξ : ℕ → Ω → Ξ of measurable, independent maps on a probability space, each with law $\mathbb P_\xi$; $F^N_\varepsilon$ uses the first $N$ draws.
• "As $N\to\infty$ and $\varepsilon\to0$" is the product filter atTop ×ˢ 𝓝[>] 0 on $\mathbb N\times\mathbb R$, with $\varepsilon>0$ because $\Gamma_\varepsilon$ needs it; one null set serves every conclusion of a statement.
• Assumption 3.1 is "no atoms": $\mathbb P_\xi(C(x,\xi)=y)=0$ for all $x\in X$, $y\in\mathbb R$. Assumption 3.2 is measurability of $C(x,\cdot)$ on $X$ plus almost-sure continuity of $C(\cdot,\xi)$ on $\mathbb R^n$.
• The family $\gamma_\varepsilon$ is any family with each member admissible; no relation across $\varepsilon$ is assumed. The quartic kernel (2.6) is admissible for every $\varepsilon>0$, so the hypothesis is satisfiable.
• The feasible set of (2.4) is $\{x\in X\mid F^N_\varepsilon(0;x)\ge1-\alpha\}$, the form the paper's proof uses. The quantile $Q^{1-\alpha}_\varepsilon$ of (2.4) is defined only when $(1-\alpha)N\notin\mathbb Z$, which fails for infinitely many $N$ when $\alpha$ is rational; where it is defined, the two feasible sets coincide.
• The optimal value is the real infimum, which Lean sets to $0$ on an empty set. The goal therefore asserts eventual nonemptiness of $S^N_\varepsilon$ itself, and (3.3)–(3.4) are stated as bounds on $f$ over the feasible set of (2.4), which imply the liminf and limsup without reading an infimum over a possibly empty set. The deviation $\mathbb D$ is stated pointwise ("every point of $S^N_\varepsilon$ is eventually within $\eta$ of $S$"), with $S$ nonempty by Assumption 3.3, so the distance to the empty set never arises.
• Iterated limits (first $N$, then $\varepsilon$), a null set chosen after $\eta$, or a feasible set defined through $Q_\varepsilon$ with its junk value would each be a different and weaker statement; none is used.

The definitions layer (Γ_ε, admissibility, $F$, $F_\varepsilon$, $F^N_\varepsilon$, $X_\alpha$, the shifted sample sets (3.2)) is shared with the companion mission on finite-sample feasibility. A uniform law of large numbers for almost-surely continuous, bounded integrands on a compact parameter set, and convergence of optimal values under uniform convergence of constraint functions, are reusable beyond this mission; contributions of either as standalone lemmas are welcome.

Selected references

• A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020; preprint arXiv:1905.07377v2, 2020. https://arxiv.org/abs/1905.07377, https://doi.org/10.1137/19M1261985
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, second edition, 2014 (Theorems 4.91, 5.3, 7.53; reference [40] of the paper). https://doi.org/10.1137/1.9781611973433
• B. K. Pagnoncelli, S. Ahmed, A. Shapiro, Sample average approximation method for chance constrained programming: theory and applications, J. Optim. Theory Appl. 142, 2009, pp. 399–416. https://doi.org/10.1007/s10957-009-9523-6
• J. Luedtke, S. Ahmed, A sample approximation approach for optimization with probabilistic constraints, SIAM J. Optim. 19, 2008, pp. 674–699. https://doi.org/10.1137/070702928
• L. J. Hong, Y. Yang, L. Zhang, Sequential convex approximations to joint chance constrained programs: a Monte Carlo approach, Oper. Res. 59, 2011, pp. 617–630. https://doi.org/10.1287/opre.1100.0910
• A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17, 2006, pp. 969–996. https://doi.org/10.1137/050622328

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

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

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.

Motivation

A Hawkes process is a model for events that make further events more likely for a time. It is used when event times cluster, including transaction arrivals in financial markets. Jaisson and Rosenbaum study what happens when the feedback approaches the threshold at which the usual stable model ceases to have a finite long-run mean intensity. The behavior depends on how fast the observation horizon grows relative to that approach to instability. Their first regime says that, when the horizon grows sufficiently faster, the observed count still becomes deterministic after normalization. The precise result is Theorem 2.1 of Jaisson and Rosenbaum (2015).

The mission concerns that first regime alone. It isolates an $L^2$ statement that controls the whole observed path at once, rather than a count at one fixed time. Later results in the paper use a different balance between the horizon and the feedback parameter and produce stochastic diffusion limits. Those later regimes are separate missions in this series.

Setting

For each horizon $T>0$, let $N^T_t$ count events through time $t$, starting from $N^T_0=0$. It is observed for $0\le t\le T$ on a probability space that may depend on $T$. Its intensity is the nonnegative process

$$\lambda_t^T=\mu+\int_0^t\phi^T(t-s)\,dN_s^T,\qquad \mu>0.$$

The baseline $\mu$ creates events even before any excitation. At each jump of $N^T$, the kernel $\phi^T$ adds an effect that depends on the elapsed time since that event. The intensity property is specified relative to the natural filtration $\mathcal F_t^T=\sigma(N_s^T:0\le s\le t)$: for $0\le a<b\le T$ and $A\in\mathcal F_a^T$, the expected number of new events on $A$ equals the expected integrated intensity on $A$ over $(a,b]$. This is the defining condition used in §2.1 of the paper.

Assumption 1 fixes a nonnegative measurable kernel $\phi$ of total mass one and finite first moment $m=\int_0^\infty s\phi(s)\,ds$. Its derivative is bounded and integrable. The horizon-dependent kernel is $\phi^T=a_T\phi$, with $0<a_T<1$ and $a_T\to1$. Thus $\|\phi^T\|_1=a_T$ approaches the stability boundary. The paper also defines the compensated count $M_t^T=N_t^T-\int_0^t\lambda_s^T\,ds$ and the resolvent $\psi^T=\sum_{k\ge1}(\phi^T)^{*k}$, where each convolution uses nonnegative time. These enter the supporting results.

Formalization targets

The goal is Theorem 2.1, in the regime $T(1-a_T)\to\infty$. Its $L^2$ assertion is

$$\mathbb E\!\left[\left(\sup_{v\in[0,1]}\frac{1-a_T}{T} \left|N^T_{Tv}-\mathbb E[N^T_{Tv}]\right|\right)^2\right]\longrightarrow0.$$

The supremum is inside the expectation. The time variable $v$ runs over the entire unit interval, so this is a statement about the normalized path of the count. The normalizing factor depends on both the horizon and the distance $1-a_T$ from the stability boundary.

The milestone list consists of the paper's renewal identity (Lemma 4.1), its two representations of the Hawkes mean and centered count, the exact mass of $\psi^T$, a pathwise fluctuation bound, the Doob $L^2$ estimate for $M^T$, and the finite-horizon bound with constant $4\mu/[T(1-a_T)]$. The final estimate has no asymptotic hypothesis; the goal adds the regime condition and takes its limit. The unnumbered milestones are the displays in §4.1, pp. 14–15, and Lemma 4.1 appears in §4.2, p. 15.

Significance

The result identifies a regime in which near instability does not produce macroscopic random fluctuations at the paper's normalization. It supplies a boundary between the familiar deterministic large-horizon behavior of stable Hawkes processes and the diffusion behavior obtained under the paper's other scaling. The theorem controls the largest fluctuation over the whole observation interval, which is stronger than a statement at each fixed $v$ or a bound on the supremum of separate variances.

The mathematical result is proved in the paper; the target here is a machine-checked proof of the same result. A completed development would also provide reusable Lean definitions for a simple counting process, its generated filtration, pathwise jump integration, Hawkes intensity, and nonnegative-time convolution resolvent. It would make explicit the maximal inequality and renewal estimates needed for other Hawkes scaling questions. This mission currently poses these statements as open Lean proof obligations; it does not claim the paper's proof is already formalized.

Difficulty

The near-instability parameter $a_T$ tends to one, so estimates for a Hawkes process with a fixed $a<1$ cannot simply be used with a uniform constant. The scale of the mean and the size of the fluctuations both change with $T$. There is also a pathwise issue: the theorem places a supremum over all $v\in[0,1]$ inside an $L^2$ expectation. A separate estimate for each $v$ does not provide the required control of the path maximum.

The point-process side adds another layer. The compensated count is a continuous-time martingale with jumps, and the intensity depends on its own event history. The result therefore needs the correct relation among the natural filtration, the intensity identity, the resolvent, and the martingale maximum. The book-keeping at a jump matters: the cadlag intensity includes the jump at its time, while stochastic compensator integrals use the same process only up to a set of times of Lebesgue measure zero.

Formalization scope

The Lean development indexes the paper's implicit horizons as a sequence $T_n>0$ tending to infinity; the multipliers $a_n\in(0,1)$ tend to one, and $T_n(1-a_n)\to\infty$. Each $N^{T_n}$ may use a different probability space. Time is represented by real numbers, with the counting-process conditions applied on nonnegative time and the Hawkes intensity identity applied only through the observation horizon. The count is natural-number valued, right-continuous, nondecreasing, and has unit jumps. The Hawkes intensity is defined by a finite sum over jumps in $(0,t]$, and the conditional intensity identity uses extended nonnegative expectations, so an infinite expectation is not silently assigned zero.

The kernel $\phi$ is measurable and nonnegative on $[0,\infty)$, has total mass one and finite first moment, and has an integrable bounded derivative; differentiability at zero is one-sided. The resolvent starts at the first convolution power, not at an identity term. Its $L^1$ mass is taken over positive time. The path supremum and its squared expectation are extended nonnegative quantities. Ordinary real expectations of $N^T_{Tv}$ are retained because their integrability follows from the Hawkes assumptions; the theorem does not assume it separately.

The Hawkes predicate is the paper's natural-filtration intensity condition for $\phi^T=a_T\phi$. A vacuous process condition, an intensity built from $\phi$ instead of $\phi^T$, or a supremum taken outside the expectation would change the target. Contributions to the generic counting-process and resolvent definitions, the renewal identity, the finite-horizon martingale estimates, and the goal theorem are all within scope. The source's p. 14 bound omits an absolute value on the centered count; the Lean milestone states the absolute-value form required by its subsequent squared estimate, while its verbatim field preserves the printed form.

Selected references

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