Stochastic Systems

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward SDE, solved from an initial state, with a backward SDE, solved from a terminal condition that depends on the forward state. Such systems arise from the stochastic maximum principle, from quasilinear parabolic PDEs through Feynman–Kac formulas, and in mathematical finance. Whenever a control problem or a market model is solved through its first-order conditions, a fully coupled FBSDE appears, and the question is whether it has a unique solution.

The history has a recurring gap: each method covers a different regime, and none handles coefficients that are random, fully coupled, and have a forward diffusion depending on the martingale integrand $Z$, over an arbitrary horizon.

• 1993: F. Antonelli proved well-posedness over a small time interval by contraction, under a smallness condition on the coupling.
• 1994: J. Ma, P. Protter and J. Yong introduced the four-step scheme, solving Markovian FBSDEs with deterministic coefficients over arbitrary horizons through a quasilinear PDE; the forward diffusion may not depend on $z$ in a degenerate way.
• 1995–1999: Y. Hu, S. Peng and Z. Wu developed the method of continuation, which allows random coefficients over arbitrary horizons under a monotonicity condition on the coefficients.
• 1999–2002: E. Pardoux and S. Tang, and F. Delarue, extended the PDE and fixed-point approaches under weak-coupling or strong-monotonicity conditions, in the Markovian setting.
• 2015: J. Ma, Z. Wu, D. Zhang and J. Zhang (the source of this mission) gave a unified approach through the decoupling field and a scalar ordinary differential equation that dominates its spatial derivative.

Setting

Fix a horizon $T>0$ and a probability space carrying a one-dimensional Brownian motion $B$, with $\mathbb F$ its natural filtration augmented by the null sets. All processes are real valued. The FBSDE (1.1) is

$$X_t=x+\int_0^t b(s,\Theta_s)\,ds+\int_0^t\sigma(s,\Theta_s)\,dB_s,\qquad Y_t=g(X_T)+\int_t^T f(s,\Theta_s)\,ds-\int_t^T Z_s\,dB_s ,$$

for $t\in[0,T]$, with $\Theta=(X,Y,Z)$. The coefficients $b,\sigma,f$ depend on $(t,\omega,x,y,z)$ and $g$ on $(x,\omega)$. Assumption 2.1 asks that they be progressively measurable for fixed $(x,y,z)$, that $I_0^2=\mathbb E\{(\int_0^T[|b|+|f|](t,0,0,0)dt)^2+\int_0^T|\sigma|^2(t,0,0,0)dt+|g(0)|^2\}$ be finite, and that they be Lipschitz in $(x,y,z)$ with a common constant $K_0$, uniformly in $\omega$. Solutions are sought in the space $\mathbb L^2$ of progressively measurable $\Theta$ with $\|\Theta\|^2_{\mathbb L^2}=\mathbb E\{\sup_t(|X_t|^2+|Y_t|^2)+\int_0^T|Z_t|^2dt\}<\infty$.

A decoupling field (Definition 2.2) is a random field $u(t,x)$ with $u(T,\cdot)=g$ such that, on every short interval $[t_1,t_2]$ and from every square-integrable initial state, the FBSDE with terminal map $u(t_2,\cdot)$ is uniquely solvable and its solution satisfies $Y_t=u(t,X_t)$.

The difference quotients (3.1) of the coefficients — $\tilde b_i,\tilde\sigma_i,\tilde f_i$ in the variables $x,y,z$ ($i=1,2,3$) and $\tilde h$ for $g$ — enter the scalar function

$$F=f_1+f_2y+y(b_1+b_2y)+\frac{(f_3+b_3y)\,y\,(\sigma_1+\sigma_2y)}{1-\sigma_3y},$$

and its essential supremum $\overline F(t,y)$ and infimum $\underline F(t,y)$ over all quotients give the dominating ODEs (3.13): $\overline y_t=\overline h+\int_t^T\overline F(s,\overline y_s)ds$ and $\underline y_t=\underline h+\int_t^T\underline F(s,\underline y_s)ds$, with $\overline h,\underline h$ the bounds of $\tilde h$.

Formalization targets

Goal: Theorem 7.4

Fix $c_1,c_2,c_3$ with $c_1>0$, $0<c_2<c_3$, $c_1c_3<1$ (5.13). There are $\varepsilon>0$ and $C>0$, depending only on $T$, $K_0$ and $c_1,c_2,c_3$, such that whenever Assumption 2.1 holds and the quotients satisfy one of the nine conditions of Cases I–III ((5.14); (5.15)–(5.18); (5.19)–(5.22)), uniformly in the quotient arguments, then (i) the FBSDE has a decoupling field $u$ whose quotient $(u(t,x_1)-u(t,x_2))/(x_1-x_2)$ obeys the bound assumed of $\tilde h$ with $c_2$ replaced by $c_3$, and (ii) for every $x$ there is a unique solution in $\mathbb L^2$, with

$$\|\Theta\|^2_{\mathbb L^2}\le C\,\big[\,|x|^2+I_0^2\,\big].$$

Milestones

• Lemma 5.1: comparison for scalar backward ODEs between a sub- and a super-solution.
• Theorems 5.9, 5.10, 5.11: under each case, the dominating ODEs have bounded solutions with the bound of $h$ transported to $c_3$, and $1-\sigma_3y$ stays away from $0$.
• Theorems 6.1, 6.2, 6.3: over a short horizon $T\le\delta$, unique solvability, solutions of (3.13) in a band, and a random field $u$ whose quotients lie between $\underline y$ and $\overline y$.
• Theorem 2.3: a decoupling field gives a unique global solution with $Y_t=u(t,X_t)$.

A companion statement, Corollary 7.5, gives well-posedness over $[0,T]$ under the sign conditions (7.5) or (7.6), with no smallness constant.

Significance

The theorem replaces structural assumptions (small horizon, monotonicity, deterministic coefficients, $\sigma$ independent of $z$) by conditions that can be read off the coefficients through a scalar ODE. It covers random coefficients and a forward diffusion that depends on $z$, the case in which the classical Riccati-type obstruction $\sigma_3h=1$ appears, and it recovers the earlier sufficient conditions as special cases (§7.4 of the paper). The decoupling field produced in (i) is uniformly Lipschitz, which is the input to the comparison and stability results of §8 and to numerical schemes based on $Y_t=u(t,X_t)$.

The result is proved in the paper; nothing here is open mathematically. None of it is formalized: there is no machine-checked existence theory for coupled FBSDEs in any proof assistant this mission is aware of. A complete development would be the first formal well-posedness theorem for a fully coupled FBSDE, and the milestones — the ODE comparison lemma, the small-time theory, and the patching argument of Theorem 2.3 — are each self-contained.

Difficulty

The obvious approach is a contraction argument on $[0,T]$. It works only when $T$ is small, because the Lipschitz constant of the solution map grows with the coupling; iterating it over a partition requires a terminal condition $u(t_i,\cdot)$ whose Lipschitz constant does not deteriorate from one subinterval to the next. Controlling that constant is the whole problem. Its spatial derivative satisfies a backward stochastic Riccati equation with quadratic growth in both $y$ and $z$ and a singularity where $1-\sigma_3y=0$; such equations need not have bounded solutions, and the standard comparison theory for quadratic BSDEs does not apply off the region where the generator is Lipschitz. A second difficulty is the small-time theory itself: when $\sigma$ depends on $z$, even a linear FBSDE with constant coefficients is well posed on short intervals only if $\sigma_3h\ne1$ (Theorem 7.1 of the paper), so in Cases II and III, where $\sigma_3$ and $h$ are large, the contraction argument does not apply even for small $T$.

Formalization scope

The development reuses the platform's Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathcal F}$, the $L^2$ Itô integral IsItoIntegral) and the augmented Brownian filtration of ReflectedBSDE.Existence.Setting. Time is $\mathbb R_{\ge0}$, time integrals are over real intervals, and the stochastic integral $\int_{t_1}^t\sigma\,dB$ is $J_t-J_{t_1}$ for an Itô integral process $J$ of $\mathbf 1_{(t_1,t_2]}\sigma(s,\Theta_s)$.

Committed conventions:

• Lipschitz bounds use the $\ell^1$ norm on $\mathbb R^3$ and hold for every $\omega$; $I_0^2$ and $\|\Theta\|^2_{\mathbb L^2}$ are lower Lebesgue integrals in $[0,\infty]$.
• Uniqueness is uniqueness in $\mathbb L^2$: $X,Y$ agree a.s. at each time and $Z$ agrees $dt\otimes d\mathbb P$-a.e.
• Solutions are unique only up to modification, so (7.2) is asserted for one solution in $\mathbb L^2$.
• Definition 2.2's "$0=t_1<t_2\le T$" is read as $0\le t_1$, as the proof of Theorem 2.3 uses it.
• Every condition on the quotients holds for every $t\in[0,T]$, almost surely, for all arguments with distinct coordinates. $\overline F(t,c)\le\varepsilon$ is stated in exactly that form. $\overline F,\underline F,\overline h,\underline h$ as functions are $\mathrm{EReal}$-valued, and solutions of (3.13) keep them finite.
• "$(1-\sigma_3y)^{-1}$ is bounded" is $|1-\tilde\sigma_3y_t|\ge\kappa>0$. Every use of $\alpha_3=b_2-b_3\sigma_2/\sigma_3$ carries $\tilde\sigma_3\ne0$, and (5.19), (5.21) carry the heading $\sigma_3\ne0$ of Table 3 in the goal.
• The quotient bounds on $u$ hold for each $t$ and each pair $x_1\ne x_2$ almost surely.
• Lemma 5.1 additionally assumes $y^1\le y^2$ and $L\ge0$, both implicit on the page.

The constants $\varepsilon$, $\delta$ and $C$ are chosen before the probability space and the coefficients. A formalization that places them after the coefficients, integrates without integrability, divides at the pole $1-\sigma_3y=0$, uses a real-valued essential supremum of an unbounded family, or states uniqueness without a solution class would make the statements vacuous or false; none of these is used.

Contributions are welcome on every milestone. The ODE layer (Lemma 5.1 and the a priori bounds of Theorems 5.9–5.11) needs only real analysis and is a natural first target. The stochastic layer needs Itô-integral facts (linearity, restriction to subintervals, the Burkholder–Davis–Gundy and Doob inequalities in $L^2$) and the Lipschitz BSDE theory; these are reusable well beyond this mission.

Selected references

• J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. https://arxiv.org/abs/1110.4658
• F. Antonelli, Backward–forward stochastic differential equations, Ann. Appl. Probab. 3(3):777–793, 1993. https://doi.org/10.1214/aoap/1177005363
• J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly — a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. https://doi.org/10.1007/BF01192258
• Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. https://doi.org/10.1007/BF01204218
• S. Peng, Z. Wu, Fully coupled forward–backward stochastic differential equations and applications to optimal control, SIAM J. Control Optim. 37(3):825–843, 1999. https://doi.org/10.1137/S0363012996313549
• F. Delarue, On the existence and uniqueness of solutions to FBSDEs in a non-degenerate case, Stochastic Process. Appl. 99:209–286, 2002. https://doi.org/10.1016/S0304-4149(02)00085-6
• J. Ma, J. Yong, Forward–Backward Stochastic Differential Equations and their Applications, Lecture Notes in Math. 1702, Springer, 1999. https://doi.org/10.1007/978-3-540-48831-6

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

Model-free bounds for lookback options

A lookback option pays a function of the running maximum of the underlying asset over the life of the contract. When the prices of European call options of all strikes at the maturity are quoted, the risk-neutral law $\mu$ of the terminal price is known, but the law of the whole path is not. The robust (model-free) superhedging cost of the lookback payoff is the cheapest initial capital that, combined with a static position in the quoted calls and dynamic trading in the underlying, dominates the payoff in every model consistent with $\mu$.

Hobson (Finance Stoch. 1998) computed this cost for $g(x)=x$ by a pathwise inequality, and identified the extremal model through the Azéma–Yor solution of the Skorokhod embedding problem (Azéma–Yor 1979). Galichon, Henry-Labordère and Touzi (Ann. Appl. Probab. 2014, arXiv:1401.3921) recast model-free bounds as a dual stochastic control problem in which the marginal constraint is penalised by a Lagrange multiplier $\lambda$. Their Theorem 3.1 recovers Hobson's bound for every $C^1$ nondecreasing $g$ from that dual, with an explicit optimal multiplier and stopping time. The result is one of the founding examples of martingale optimal transport.

Setting

Let $B$ be a real Brownian motion with continuous paths and $B_0=0$, adapted to a filtration $(\mathcal F_t)_{t\ge0}$ with increments independent of the past, and let $X_t=X_0+B_t$ for a spot $X_0\in\mathbb R$. Write $X^*_\tau=\max_{t\le\tau}X_t$. Let $\mathcal T_\infty$ be the set of stopping times $\tau$ for which the stopped process $(X_{t\wedge\tau})_{t\ge0}$ is a uniformly integrable martingale.

The marginal is a probability measure $\mu$ on $\mathbb R$ with finite first moment and mean $\int x\,\mu(dx)=X_0$. Its call prices are $c(x)=\int(y-x)^+\mu(dy)$. The payoff is $\xi=g(X^*)$ with $g:\mathbb R\to\mathbb R_+$ of class $C^1$ and nondecreasing.

For a multiplier $\lambda:\mathbb R\to\mathbb R$ and $\tau\in\mathcal T_\infty$ set $J(\lambda,\tau)=\mathbb E[g(X^*_\tau)-\lambda(X_\tau)]$ and $u^\lambda(X_0,X_0)=\sup_{\tau\in\mathcal T_\infty}J(\lambda,\tau)$. The admissible multipliers are

$$\Lambda^\mu_0=\Big\{\lambda\in\mathbb L^1(\mu):\ \sup_{\tau\in\mathcal T_\infty}\mathbb E[\lambda(X_\tau)^-]<\infty\Big\},$$

and the reduced superhedging problem (3.7) is

$$U^\mu(\xi)=\inf_{\lambda\in\Lambda^\mu_0}\Big\{\int\lambda\,d\mu+u^\lambda(X_0,X_0)\Big\}.$$

The barycenter function is $b(x)=\int_{[x,\infty)}y\,\mu(dy)/\mu([x,\infty))$ for $\mu((x,\infty))>0$ and $b(x)=x$ otherwise. The Hardy–Littlewood transform $\mu^{HL}$ is the probability measure with

$$\mu^{HL}([y,\infty))=\inf_{\xi<y}\frac{c(\xi)}{y-\xi}.$$

The Azéma–Yor stopping time is $\tau^*=\inf\{t>0:X^*_t\ge b(X_t)\}$, and the candidate multiplier is

$$\lambda^*(x)=\int_{\ell^\mu}^{x}\!\int_{\ell^\mu}^{y}g'(b(\xi))\,\frac{b(d\xi)}{b(\xi)-\xi}\,dy ,$$

that is, the convex function vanishing below $\ell^\mu$ that solves the weak ODE (3.21) with $\psi=b^{-1}$.

Formalization targets

Goal: Theorem 3.1

If $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$ and $\mu^{HL}(g)=\int g\,d\mu^{HL}<\infty$, then

$$U^\mu(\xi)=\mu(\lambda^*)+J(\lambda^*,\tau^*)=\mu^{HL}(g).$$

The goal is the paper's theorem for the reduced problem (3.7), in its full two-equality form: the value, its attainment by $(\lambda^*,\tau^*)$, and its closed form.

Milestones

1. The Neumann condition (3.23) for Peskir's candidate $v^\psi$.
2. Lemma 3.1: $u^\lambda\le v^\psi$ for convex $\lambda\in\Lambda^\mu_0$ and every relaxed free boundary $\psi\in\Psi^\lambda$.
3. Step (1) of Lemma 3.2: $\mu(\lambda)-\lambda(X_0)=\int(c-c_0)\,d\lambda''$, with $c_0(x)=(X_0-x)^+$.
4. Lemma 3.2: $\mu(\lambda)+u^\lambda(X_0,X_0)\le g(X_0)+\int\varphi(\psi(m),m)g'(m)\,dm$.
5. The pointwise minimizations (3.27) and (3.28).
6. Steps (2) and (3) of Lemma 3.3: properties of $\lambda^*$, and the integration by parts giving $\mu^{HL}(g)$.
7. Lemma 3.3, the upper bound $U^\mu(\xi)\le\mu^{HL}(g)$.
8. The Azéma–Yor facts: $\tau^*\in\mathcal T_\infty$, $X_{\tau^*}\sim\mu$, $X^*_{\tau^*}\sim\mu^{HL}$.
9. The lower bound $U^\mu(\xi)\ge\mu^{HL}(g)$ of Section 3.4.

Significance

The theorem identifies the model-free price of a lookback payoff as an explicit functional of the call prices, $\mu^{HL}(g)$, and exhibits the extremal model (Brownian motion stopped at $\tau^*$) and the optimal static hedge ($\lambda^*$). It shows that the dual stochastic control formulation is sharp on a nontrivial path-dependent payoff, which is the template for later work on martingale optimal transport with path-dependent costs.

The result has been proved since 2014 (and Hobson's bound since 1998). It has not been formalized. A complete development would provide machine-checked versions of the Azéma–Yor embedding, the law of the maximum at the embedding, a verification theorem for a reflected optimal stopping problem with a nonsmooth obstacle, and the convex-analytic identities linking call prices to second-derivative measures. Each of these is reusable well beyond this paper.

Difficulty

The upper bound requires a verification argument for an optimal stopping problem of the pair $(X,X^*)$ with a reflection at the diagonal, where the candidate $v^\psi$ is only as regular as the convex multiplier $\lambda$: second derivatives are measures and the free boundary $\psi$ solves its ODE only in a relaxed sense. An Itô formula for $C^2$ functions does not apply; an Itô–Tanaka (local time) argument for concave functions of $X$, with the reflection term killed by the Neumann condition, is needed, followed by a localisation that uses uniform integrability and the integrability condition in $\Lambda^\mu_0$. The lower bound needs the Azéma–Yor embedding and the law of $X^*_{\tau^*}$, neither of which is in Mathlib; the naive appeal to "the embedding exists" does not give the joint law of the stopped value and the maximum.

Formalization scope

The Lean development lives in the namespace LookbackMOT.HL and uses Mathlib's IsBrownianReal, IsStoppingTime, stoppedProcess, stoppedValue, Martingale, UniformIntegrable and HasLaw. Committed conventions:

• What is formalized. The goal is the reduced problem (3.7), not the superhedging problem (2.6): (2.6) needs stochastic integrals, which Mathlib does not have. The bridge between them (Proposition 2.1, the claim (3.4), Proposition 3.1) is outside this mission. The theorem's hypothesis $\sup_{\mathbb P\in\mathcal P_\infty}\mathbb E^{\mathbb P}[\xi^+]<\infty$ is stated through Proposition 3.1 with $\lambda=0$ as $\sup_{\tau\in\mathcal T_\infty}\mathbb E[g(X^*_\tau)]<\infty$. The horizon $T$ disappears: the stopping problem is over $\mathcal T_\infty$ with time in $[0,\infty)$.
• Standing hypotheses. The Brownian motion lives on an arbitrary filtered probability space with everywhere-continuous paths and $B_0=0$; the paper's canonical space is one instance. The mean condition and integrability of $\mu$ (p. 7) are assumed throughout. The spot $X_0$ is any real number. $\mu([0,\infty))=1$ is assumed only in (3.27).
• Added conditions. Every $\tau\in\mathcal T_\infty$ is a.s. finite (implied by uniform integrability). Every $\lambda\in\Lambda^\mu_0$ is measurable.
• Expectations of payoffs are $\mathbb E[\varphi^+]-\mathbb E[\varphi^-]$ in the extended reals, with $\infty-\infty=-\infty$; value functions are extended reals.
• Derivatives. $\lambda'$ is the right derivative and $\lambda''$ its Stieltjes measure. The weak ODE (3.21) is used both as a change of variables ($\lambda''$ is the image of $g'(m)/(m-\psi(m))\,dm$ under $\psi$) and on intervals ($\lambda'(\psi(y_2))-\lambda'(\psi(y_1))=\int_{y_1}^{y_2}g'(m)/(m-\psi(m))\,dm$), the two forms the paper's proofs use.
• The multiplier $\lambda^*$. It is written as $\lambda^*(x)=\int_{X_0<m<r^\mu}g'(m)(x-b^{-1}(m))^+/(m-b^{-1}(m))\,dm$, the change of variables $m=b(\xi)$ in (3.14) and the solution of (3.21) with $\psi=b^{-1}$ that the proof of Lemma 3.3 uses. It agrees with the $b(d\xi)$ formula when $b$ is continuous; at the jumps of $b$ (atoms of $\mu$) the Lebesgue–Stieltjes reading of (3.14) can fail to be $\mu$-integrable.
• Measures given by identities. $\mu^{HL}$ and $\lambda''$ enter as measures satisfying their defining identities on intervals; each exists and is unique.
• Printed slips not copied. (3.12) prints the numerator $c(y)$; the formalization uses $c(\xi)$. $b$, $\mu^{HL}$ and $\lambda^*$ are extended from $x\ge0$ to all of $\mathbb R$ by the same formulas.

No trivializing reading is available. Payoff expectations are never Bochner integrals (which would be $0$ for non-integrable payoffs). $\tau\equiv0$ lies in $\mathcal T_\infty$ and $\lambda\equiv0$ in $\Lambda^\mu_0$, so neither the supremum nor the infimum is over an empty set. The predicates for $\mu^{HL}$ and $\lambda''$ are satisfiable (witnessed for $\mu=\delta_{X_0}$ in a sorry-free check). $X_\tau$ is only evaluated where $\tau<\infty$ a.s. Every division has a positive denominator on the sets that carry mass.

Contributions welcome: the Azéma–Yor embedding and the law of the maximum; an Itô–Tanaka or local-time calculus sufficient for concave functions of Brownian motion and its maximum; the call-price identities of convex analysis; and the analysis of $\mu^{HL}$.

Selected references

• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24 (2014) 312–336. https://arxiv.org/abs/1401.3921 (v1, the version cited)
• D. Hobson, Robust hedging of the lookback option, Finance Stoch. 2 (1998) 329–347. https://doi.org/10.1007/s007800050046
• J. Azéma, M. Yor, Une solution simple au problème de Skorokhod, Séminaire de Probabilités XIII, LNM 721 (1979) 90–115. https://doi.org/10.1007/BFb0070852
• G. Peskir, Optimal stopping of the maximum process: the maximality principle, Ann. Probab. 26 (1998) 1614–1640. https://doi.org/10.1214/aop/1022855875
• L. Carraro, N. El Karoui, J. Obłój, On Azéma–Yor processes, their optimal properties and the Bachelier–drawdown equation, Ann. Probab. 40 (2012) 372–400. https://arxiv.org/abs/0902.1328

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.

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.