Probability

Motivation

In an aggregative game, each player's cost depends on its own decision and on the sum of all players' decisions. That form appears in resource sharing, production, and network games: a player may know its own choice while lacking a central feed of the aggregate. A distributed algorithm therefore has to estimate the aggregate through local communication as it updates decisions. Koshal, Nedić, and Shanbhag study this setting and give both synchronous and gossip schemes in Distributed Algorithms for Aggregative Games on Graphs. This mission concerns their asynchronous scheme, in which a random pair communicates at each tick.

The question is whether irregular, local updates still find the game's equilibrium when no agent knows in advance how often it will be selected. Each agent uses its own update count to set its step length. The paper's Proposition 3 states almost-sure convergence under strict monotonicity, compact strategy sets, and a connected graph. The result is a convergence claim about the complete random process, including who wakes, whom they contact, which estimate they exchange, and which projected step they take.

Setting

There are $N\ge1$ agents. Agent $i$ chooses $x_i\in K_i\subseteq\mathbb R^n$, with $K_i$ nonempty, compact, and convex. A strategy profile is $x=(x_1,\ldots,x_N)$ in $K=\prod_i K_i$, and its aggregate is $\bar x=\sum_i x_i$. The map $F_i(x_i,u)$ is the player's first-order response when its own decision is $x_i$ and its aggregate argument is $u$. The game map is $\phi_i(x)=F_i(x_i,\bar x)$. A solution $x^*$ of the variational inequality $\mathrm{VI}(K,\phi)$ is feasible and satisfies

$$\sum_i\langle x_i-x_i^*,\phi_i(x^*)\rangle\ge0 \quad\text{for every }x\in K.$$

The paper obtains $F_i$ from differentiable convex player costs, making VI solutions Nash equilibria. The formal statements take $F_i$ as the primitive map used by the algorithm. Strict monotonicity means $\sum_i\langle\phi_i(x)-\phi_i(y),x_i-y_i\rangle>0$ for different feasible profiles $x,y$. Along with continuity and compact convex strategy sets, it makes the VI solution unique. The paper's Assumptions 1–3 also impose a uniform Lipschitz bound on how $F_i(x_i,u)$ changes with $u$.

Agents occupy a connected, undirected graph. At a discrete tick $k$, a uniformly selected agent $I^k$ contacts a neighbour $J^k$ with probability $p_{I^kJ^k}>0$ on every edge. The ordered pairs are independent across ticks. Each agent maintains an aggregate estimate $v_i^k$; the selected pair average their estimates to form $\hat v_i^k$. Those agents take a projected step using $F_i(x_i^k,N\hat v_i^k)$ and then add their decision change to the estimate. Other agents retain their decisions and estimates. Initially $v_i^0=x_i^0$. The number $\Gamma_k(i)$ counts agent $i$'s updates through tick $k$, and its step length at an update is $\alpha_{k,i}=1/\Gamma_k(i)$. Equations (23)–(29) of the paper define these operations.

Formalization targets

Goal: almost-sure equilibrium convergence

Under Assumptions 1–3 and connectedness of the gossip graph, Proposition 3 asserts that there is a unique $x^*$ solving $\mathrm{VI}(K,\phi)$ and that the generated process satisfies

$$\Pr\bigl(\lim_{k\to\infty}x^k=x^*\bigr)=1.$$

The goal includes existence and uniqueness of $x^*$, rather than conditioning convergence on a possibly nonexistent solution. Its random draws have the rate-one-clock law: $\Pr(I^k=i,J^k=j)=p_{ij}/N$.

Milestones

The five milestones record the VI's unique solution from the proof of Proposition 1, conservation of the agents' average estimate in Lemma 2, the almost-sure stepsize bounds of Lemma 7, their summability consequences in Corollary 1, and the mean-square gossip contraction in relations (30)–(31). They cover the equilibrium, tracking, step length, and network-mixing parts of the claim. Their source wording, indices, and PDF pages are attached to the mission items.

Significance

The result shows that a shared aggregate can be learned well enough through pairwise, random exchanges to reach the same equilibrium characterized by the centralized VI. Update counts permit agents to choose diminishing steps without a common iteration clock or a schedule ensuring equal participation on each finite interval. Connectedness and positive contact probabilities ensure every graph edge can carry information. The convergence assertion is almost sure, so it concerns individual sample paths outside a null set, rather than merely an average error.

Formalizing the result would connect finite graph gossip, random update counts, projected VI iteration, and almost-sure convergence in one reusable development. The paper proves Proposition 3; this mission supplies an open machine-checked target, not a claim that the result is unresolved mathematically. A proof would need honest probability statements for the draw law and summability and a projection interface that does not assign arbitrary values on empty sets. The VI existence and uniqueness milestone can also serve other compact, strictly monotone games.

Difficulty

Pairwise averaging preserves the mean estimate, but it does not make each agent's estimate equal to that mean at every step. A projected decision change immediately perturbs the local estimate again. The selected agents and their step lengths also depend on the same update history, so deterministic simultaneous-update arguments do not directly apply. The paper controls this interaction using update-count asymptotics, contraction of the random gossip matrix, and almost-sure summability. None of those conclusions follows from connectedness alone if a nominal edge has zero contact probability.

Formalization scope

Lean represents each decision in EuclideanSpace ℝ (Fin n) and profiles as functions on Fin N. The aggregate is a finite sum. A projection is the relation saying that the selected point lies in its set and minimizes Euclidean distance, rather than a total function with an arbitrary output on an empty set. The profile topology used for convergence is the finite product topology. For vectors indexed by agents, relations (30)–(31) use the explicit Euclidean coordinate norm; the default norm of Fin N → ℝ is a sup norm.

The continuous-time Poisson clocks are encoded through their induced independent discrete tick pairs and exact joint law. Initial decisions are fixed and feasible. The source allows random initial decisions; the formal goal covers every deterministic start. This restriction is recorded because the paper's stated random initialization would require an explicit independence relation with future clock draws. Tick indices start at zero in Lean; a selected agent has $\Gamma_k(i)\ge1$, so the value assigned to $1/0$ never drives an update. The positive-time series and bounds still begin at $k=1$.

The paper gives the Lipschitz condition on aggregate arguments only in the feasible aggregate set $\bar K$. Its algorithm can evaluate $F_i$ outside that set, as its own footnote acknowledges. This development explicitly extends that condition to all of $\mathbb R^n$ to make those evaluations controlled. The change is substantive and disclosed on each affected item; the preprint's Lemma 3 proof contains the corresponding domain gap. The goal assumes neither the stepsize estimates nor the network contraction nor convergence of the estimate errors; they remain mathematical work. Further contributions may formalize the omitted intermediate lemmas, or refine the initialization and domain assumptions while preserving a meaningful statement.

Selected references

• J. Koshal, A. Nedić, and U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3), 680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501.

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

A random field on a sphere assigns a random value to every direction. Such fields appear when the underlying data are directional, including spherical models in spatial statistics and geophysics. The covariance of an isotropic field can be recorded by an angular power spectrum: one nonnegative number for each spherical harmonic degree. This changes the sample regularity question into a concrete spectral question. How fast must these numbers decay so that a realization is continuous, and how regular can that realization be? Lang and Schwab, 2015 give a sufficient summability condition and an exact range of Hölder exponents in their Theorem 4.5.

The question matters when a field is evaluated on a mesh or represented by finitely many spherical harmonics. A covariance function can be regular even when the original version of a random field has badly chosen values on null sets. The useful result is therefore the existence of one regular modification: at each fixed sphere point it agrees with the given field almost surely, while its sample paths are regular across the entire sphere. The paper treats this sample path result in §4, separately from its spectral characterization of covariance regularity in §3 and its later simulation and stochastic heat equation results.

Setting

Write $S^2=\{x\in\mathbb R^3:\|x\|=1\}$ for the unit sphere. Its geodesic distance is $d(x,y)=\arccos\langle x,y\rangle$, the length of the shorter great circle arc between $x$ and $y$. A random field $T$ is a jointly measurable map from a probability space times $S^2$ to the real numbers. A field is Gaussian when every finite collection of its values has a joint Gaussian distribution. Isotropy says that rotating all observation points together does not change that joint distribution. These are the conventions of Definition 2.1 in the paper.

For each degree $\ell\ge0$, let $P_\ell$ be the Legendre polynomial normalized by $P_\ell(1)=1$, and let $A_\ell\ge0$ be its angular power. The field has a constant mean and covariance determined by $(A_\ell)$:

$$\operatorname{Cov}(T(x),T(y)) =\sum_{\ell=0}^{\infty}A_\ell\frac{2\ell+1}{4\pi}P_\ell(\langle x,y\rangle).$$

Because $\langle x,y\rangle=\cos d(x,y)$, the same covariance is expressed by the distance kernel $k(r)=\sum_{\ell\ge0}A_\ell(2\ell+1)P_\ell(\cos r)/(4\pi)$ for $0\le r\le\pi$. A modification $T'$ of $T$ means $T'(x)=T(x)$ almost surely for each fixed $x$; it need not agree on one common full measure set at every $x$. The paper's Assumption 4.1, specialized to $S^2$, asks for finiteness of $\sum_{\ell\ge0}A_\ell\ell^{1+\beta}$.

Formalization targets

Goal: sample regularity

For $0<\beta\le2$, the target is Theorem 4.5 of Lang and Schwab:

$$\sum_{\ell=0}^{\infty}A_\ell\ell^{1+\beta}<\infty \quad\Longrightarrow\quad \exists\,T'\text{ modifying }T\text{ with paths Hölder of every order }0<\gamma<\beta/2.$$

The same modification serves every eligible exponent. The result leaves the Hölder constant free to depend on the sample and the exponent, as it must.

Supporting targets

The four milestones follow the source's statements and its proof order. The Legendre polynomial bounds on p. 16 lead to Lemma 4.2, $|k(0)-k(r)|\le C_\beta r^\beta$ for $r\in[0,\pi]$ and $\beta\in[0,2]$. Lemma 4.3 transfers this to $\mathbb E|T(x)-T(y)|^{2p}\le C_{\beta,p}d(x,y)^{\beta p}$ for every positive integer $p$. Theorem 4.4 is a Kolmogorov–Chentsov theorem for any random field on $S^2$: a moment exponent $2+\varepsilon p$ produces a continuous modification with every Hölder exponent below $\varepsilon$. The Gaussian and isotropic hypotheses belong to Lemma 4.3 and the goal; they are absent from Theorem 4.4.

Significance

The theorem provides a checkable bridge from a harmonic description of a field to sample path behavior. A practitioner can estimate or impose decay of the angular power spectrum, then know that a version of the field admits interpolation on the sphere with any exponent below $\beta/2$. The endpoint $\beta/2$ is not asserted. The moment estimate and the spherical modification theorem can also be reused when studying fields produced by other models; in particular, Theorem 4.4 needs no Gaussian assumption.

The result was proved in the 2015 paper; this mission concerns its machine checked formalization. Mathlib supplies Gaussian process and measure theory interfaces, but the paper's sphere distance, Legendre normalization, angular kernel and spherical version of Kolmogorov–Chentsov must be connected. A platform goal for a Kolmogorov–Chentsov theorem on $[0,\infty)$ uses a different index space and hypotheses, so it does not cover the present milestone. The finished development will provide a reusable sphere indexed modification theorem as well as the paper's specific spectral criterion.

Difficulty

A bound on the covariance kernel controls the second moment of field increments, but it does not by itself supply one continuous version with a common pathwise regularity statement. The desired exponent concerns values at uncountably many points, whereas the definition of modification gives an almost sure equality separately at each point. The gap is visible even for simple processes: changing a field at one random location can preserve each fixed point's law while destroying continuity of individual paths. The sphere also carries a two dimensional geodesic metric, so a one dimensional modification theorem indexed by time cannot be substituted without a new argument.

Formalization scope

Lean represents $S^2$ as the unit metric sphere in three dimensional Euclidean space. Coordinates have indices $0,1,2$ for the paper's $1,2,3$. All regularity statements use $d(x,y)=\arccos\langle x,y\rangle$, not the subtype's chord distance. Rodrigues' formula defines $P_\ell$, and the kernel is a real infinite sum with its factor $(2\ell+1)/(4\pi)$. The spectrum is nonnegative and has $\sum(2\ell+1)A_\ell<\infty$ as part of the field model, matching the finite variance convention used in §2. The covariance formulation allows a nonzero constant mean: Theorem 4.5 does not require centering.

The moment inequalities use extended nonnegative integrals, avoiding a default zero for nonintegrable real integrals. The paper's positive integers are expressed with an explicit $1\le p$ because Lean's naturals include zero. Real powers follow the usual convention: the degree zero term of $\ell^{1+\beta}$ is zero when $\beta\ge0$. On compact $S^2$, local Hölder continuity gives a global constant for each path and exponent. Exceptional sample paths may be redefined, so the formal conclusion states continuity and Hölder regularity for every sample of the chosen modification. The modification retains pointwise almost sure agreement and measurable evaluations; omitting agreement would make the goal trivial.

Contributions can address Legendre inequalities, covariance and Gaussian moment calculations, and a general Kolmogorov–Chentsov theorem for compact manifolds. The latter is reusable beyond this paper. The auxiliary Legendre and kernel definitions are also available to later spherical field missions.

Selected references

• A. Lang and Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Annals of Applied Probability 25(6), 2015, arXiv:1305.1170v3, DOI:10.1214/14-AAP1067.

Motivation

Stochastic partial differential equations on the sphere model quantities that live on the surface of the Earth or of the sky and are perturbed by spatially correlated noise: temperature anomalies, geophysical fields, fluctuations of the cosmic microwave background. The simplest such model is the stochastic heat equation on the unit sphere $\mathbb S^2$ with additive isotropic noise. Because the noise is isotropic and the Laplace–Beltrami operator is diagonal in the spherical harmonics, the equation decouples into one scalar Ornstein–Uhlenbeck equation per harmonic, and the solution can be simulated exactly in law by truncating its spherical-harmonic expansion at a degree $\kappa$. The practical question is how fast this spectral truncation converges, in mean square and along a single simulated path.

A. Lang and Ch. Schwab answer this in §7 of Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations (arXiv:1305.1170v3, Ann. Appl. Probab. 25(6), 2015). Their rates are expressed through the decay of the angular power spectrum of the noise, the same quantity that governs the sample regularity and the Karhunen–Loève truncation of isotropic Gaussian random fields in the earlier sections of the paper.

Setting

Let $\mathbb S^2\subset\mathbb R^3$ be the unit sphere with surface measure $\sigma$ (total mass $4\pi$) and $L^2(\mathbb S^2)$ the real square-integrable functions with norm $\|f\|^2_{L^2(\mathbb S^2)}=\int|f|^2d\sigma$. The spherical harmonics $Y_{\ell m}$, $\ell\ge0$, $|m|\le\ell$, are built from the Legendre polynomials $P_\ell(\mu)=2^{-\ell}(\ell!)^{-1}\frac{d^\ell}{d\mu^\ell}(\mu^2-1)^\ell$; the functions $Y_{\ell0}$, $\sqrt2\operatorname{Re}Y_{\ell m}$, $\sqrt2\operatorname{Im}Y_{\ell m}$ ($1\le m\le\ell$) form a real orthonormal basis of the degree-$\ell$ harmonics, on which the Laplace–Beltrami operator acts as multiplication by $-\lambda_\ell$, $\lambda_\ell=\ell(\ell+1)$.

On a probability space $(\Omega,\mathcal A,\mathbb P)$ let $\beta^i_{\ell m}$ ($\ell\ge0$, $0\le m\le\ell$, $i=1,2$) be independent real Brownian motions, and let $(A_\ell)_{\ell\ge0}$, $A_\ell\ge0$, be an angular power spectrum. The isotropic $Q$-Wiener process is

$$W(t)=\sum_{\ell\ge0}\sqrt{A_\ell}\Big(\beta^1_{\ell0}(t)Y_{\ell0}+\sqrt2\sum_{m=1}^{\ell}\big(\beta^1_{\ell m}(t)\operatorname{Re}Y_{\ell m}+\beta^2_{\ell m}(t)\operatorname{Im}Y_{\ell m}\big)\Big).$$

The stochastic heat equation is

$$dX(t)=\Delta_{\mathbb S^2}X(t)\,dt+dW(t),\qquad X(0)=X_0\in L^2(\Omega;L^2(\mathbb S^2)).$$

Its solution is $X(t)=\sum_{\ell\ge0}X_\ell(t)$ with

$$X_\ell(t)=e^{-\lambda_\ell t}\sum_{m=-\ell}^{\ell}(X_0,Y_{\ell m})Y_{\ell m}+\sqrt{A_\ell}\Big(\int_0^te^{-\lambda_\ell(t-s)}d\beta^1_{\ell0}(s)\,Y_{\ell0}+\sqrt2\sum_{m=1}^{\ell}\Big(\int_0^te^{-\lambda_\ell(t-s)}d\beta^1_{\ell m}(s)\operatorname{Re}Y_{\ell m}+\int_0^te^{-\lambda_\ell(t-s)}d\beta^2_{\ell m}(s)\operatorname{Im}Y_{\ell m}\Big)\Big),$$

and the spectral approximation is $X^\kappa(t)=\sum_{\ell=0}^{\kappa}X_\ell(t)$. The norm $\|Z\|_{L^p(\Omega;L^2(\mathbb S^2))}=(\mathbb E\|Z\|^p_{L^2(\mathbb S^2)})^{1/p}$ measures random fields. The standing assumption of §7 is the decay condition

$$A_\ell\le C\,\ell^{-\alpha}\quad\text{for all }\ell>\ell_0,\qquad \ell_0\in\{1,2,\dots\},\ \alpha>0 .$$

Formalization targets

Goal: Corollary 7.3 (p. 43)

For every $t>0$ and every $\beta<\alpha/2$, almost surely

$$\|X(t)-X^\kappa(t)\|_{L^2(\mathbb S^2)}\le\kappa^{-\beta}\quad\text{for all sufficiently large }\kappa .$$

The goal fixes no constant; only the exponent $\alpha/2$ enters, so it survives any improvement of the constants below.

Milestones

1. Display (3), p. 36. For $\ell\ge1$, $\int_0^te^{-\ell(\ell+1)(t-s)}d\beta(s)\sim\mathcal N\big(0,(2\ell(\ell+1))^{-1}(1-e^{-2\ell(\ell+1)t})\big)$.
2. Lemma 7.1, pp. 39–40, as proved. If the coefficients of $X_0$ are independent of the noise, then for $t>0$ and $\kappa\ge\ell_0$

$$\|X(t)-X^\kappa(t)\|^2_{L^2(\Omega;L^2(\mathbb S^2))}\le C\Big(\frac2\alpha+\frac1{\alpha+1}\Big)\kappa^{-\alpha}+e^{-2(\kappa+1)(\kappa+2)t}\|X_0\|^2_{L^2(\Omega;L^2(\mathbb S^2))}.$$

3. Lemma 7.2, pp. 41–43, as proved. For each $p>0$ there is $\hat C_p=\hat C_p(p,C,\alpha)$ with, for $t>0$ and $\kappa\ge\ell_0$,

$$\|X(t)-X^\kappa(t)\|_{L^p(\Omega;L^2(\mathbb S^2))}\le\hat C_p\kappa^{-\alpha/2}+e^{-(\kappa+1)(\kappa+2)t}\|X_0\|_{L^{\max(p,2)}(\Omega;L^2(\mathbb S^2))}.$$

Significance

Corollary 7.3 is the pathwise convergence rate of the spectral method for the stochastic heat equation on the sphere: a single simulated path of the truncated series is within $\kappa^{-\beta}$ of the true path in $L^2(\mathbb S^2)$ for all large $\kappa$, for any $\beta<\alpha/2$. Combined with the exact-in-law recursion on a time grid (pp. 36–38), it says that the only source of error in simulating this SPDE is the spectral truncation, and that the rate is governed by the decay exponent of the noise spectrum alone, with $\alpha>0$ sufficing (no trace-class condition $\alpha>2$ is needed, thanks to the smoothing of the heat semigroup). The mean-square and $L^p$ estimates of Lemmas 7.1 and 7.2 are the quantitative inputs; the $L^p$ bound for all $p$ is what makes a Borel–Cantelli argument possible.

The results are proved in the paper; none of them, nor the stochastic heat equation on the sphere, nor spherical harmonics, has a machine-checked formalization on the platform or in Mathlib. The work here is to formalize the known proof. Two printed statements need correction (see Formalization scope); the milestones state the bounds that the paper's proofs establish.

Difficulty

The obvious argument writes $X(t)-X^\kappa(t)$ as the tail of the series, splits it into the damped initial condition and the noise, and bounds each. The noise part is a Gaussian random field whose angular power spectrum $A_\ell(1-e^{-2\lambda_\ell t})/(2\lambda_\ell)$ decays like $\ell^{-(\alpha+2)}$, so its truncation error is controlled by the corresponding estimates for isotropic Gaussian random fields (Proposition 5.2 and Theorem 5.3 of the paper), which must be re-derived here. Several steps have no current library support: the Wiener integral of a deterministic integrand and its Gaussian law, orthonormality and completeness of the spherical harmonics in $L^2(\mathbb S^2,\sigma)$, moment equivalence for Gaussian vectors in a Hilbert space (to pass from $p=2$ to all $p$), and the passage between the pointwise series and its $L^2$ limit. The initial-condition tail decays like $e^{-(\kappa+1)(\kappa+2)t}$ but not uniformly as $t\downarrow0$, which is exactly why the printed "uniformly in time" bounds fail and why every statement takes $t>0$ fixed.

Formalization scope

• $\mathbb S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 with coordinates indexed $0,1,2$ (the paper's $y_1,y_2,y_3$); $\sigma$ is the measure toSphere of Lebesgue measure, of mass $4\pi$. Spherical harmonics are written in Cartesian form, $P_{\ell m}(\cos\vartheta)e^{im\varphi}=(-1)^mP_\ell^{(m)}(y_3)(y_1+iy_2)^m$, which is the paper's function also at the poles. For real $X_0$ the projection $\sum_m(X_0,Y_{\ell m})Y_{\ell m}$ is written in the real orthonormal basis.
• Brownian motions are Mathlib's IsBrownianReal processes on $\mathbb R_{\ge0}$, independent as a family of path-valued random variables. The stochastic convolution $\int_0^te^{-r(t-s)}db(s)$ is defined pathwise as $b(t)-r\int_0^te^{-r(t-s)}b(s)\,ds$, which equals the Wiener integral almost surely (integration by parts; $b(0)=0$ a.s.). This is the one place where a stochastic integral is replaced by a pathwise expression.
• The Laplace–Beltrami operator is not defined: the paper's spectral solution formula of p. 36 is taken as the definition of $X(t)$, as a pointwise limit of partial sums in $(\omega,y)$; where they diverge (a $\mathbb P\otimes\sigma$-null set for $t>0$) the value is irrelevant to every norm. All statements take $t>0$; the paper's time partition with $n\in\mathbb N$ forces this, and since $X^\kappa(t)$ is defined from the solution itself the independence of the time discretization is automatic and the partition is not an argument.
• Norms are lower Lebesgue integrals in $[0,\infty]$, so no integrability side condition hides in a default value; $X_0$ is jointly measurable with $\mathbb E\|X_0\|^2_{L^2(\mathbb S^2)}<\infty$; $A_\ell\ge0$; $\ell_0\ge1$.
• Corrections. Lemmas 7.1 and 7.2 claim bounds uniform in time with constants depending only on $\|X_0\|$, $C$, $\alpha$ (and $p$). Their proofs bound the initial-condition tail by $e^{-2(\kappa+1)(\kappa+2)t}\|X_0\|^2$ (resp. $e^{-(\kappa+1)(\kappa+2)t}\|X_0\|_{L^p}$) and absorb it into $C\kappa^{-\alpha}$ with a $t$-dependent constant; for nonzero $X_0$ the printed uniform bounds are false (as $t\downarrow0$ the error tends to the $L^2$ tail of $X_0$). The milestones state the proofs' bounds with the explicit exponential term; for $X_0=0$ Lemma 7.1 is the printed statement, uniformly in $t$. Lemma 7.1 additionally assumes that the coefficients of $X_0$ are independent of the noise, which its proof uses to drop a cross term. In Lemma 7.2 the constant $\hat C_p$ depends on $p,C,\alpha$ only and is quantified before everything else. Corollary 7.3 is stated for each fixed $t$: "uniformly in time" is not formalized. The constant on p. 42, $(2/(\alpha-2)+1/(\alpha-1))$, should read $(2/\alpha+1/(\alpha+1))$; it is existential in Lemma 7.2 and has no effect.
• A trivializing reading is ruled out: the error is measured against the solution defined by the explicit series, not against an arbitrary process satisfying a hypothesis, and no hypothesis pins the conclusion.
• Reusable infrastructure: real spherical harmonics and their orthonormality on $(\mathbb S^2,\sigma)$, the Wiener integral of deterministic functions and the Ornstein–Uhlenbeck law, and $L^p$ moment equivalence for Gaussian fields. Contributions of any of these, or of the truncation estimates of §5 for the shifted spectrum, are welcome.

Selected references

• A. Lang, Ch. Schwab, Isotropic Gaussian random fields on the sphere: regularity, fast simulation and stochastic partial differential equations, Ann. Appl. Probab. 25(6), 2015. arXiv:1305.1170
• A. Jentzen, P. E. Kloeden, Overcoming the order barrier in the numerical approximation of stochastic partial differential equations with additive space–time noise, Proc. R. Soc. A 465, 2009. doi:10.1098/rspa.2008.0325
• G. Da Prato, J. Zabczyk, Stochastic Equations in Infinite Dimensions, Cambridge University Press, 1992. doi:10.1017/CBO9780511666223
• D. Marinucci, G. Peccati, Random Fields on the Sphere, Cambridge University Press, 2011. doi:10.1017/CBO9780511751677

Motivation

Online prediction compares the losses of a sequence of decisions with the losses of one fixed decision chosen after the sequence is known. A learner would like a regret guarantee that remains valid for every such competitor, even when the losses arrive in an arbitrary order. Exponentially weighted averaging is a way to make each decision from all feasible points rather than committing to one candidate early. The method gives the Weighted Average Algorithm (WAA) in Chapter 11 of Orabona's text. It is particularly effective when the exponential of each negative loss is concave, a condition called exp-concavity.

The chapter first compares WAA with a competing probability distribution. Theorem 11.5 turns that guarantee into a bound against an individual feasible point. That distinction matters when the benchmark is a concrete portfolio, parameter vector, or other fixed decision, rather than a distribution over decisions. The same chapter later extends the weighted-average viewpoint to mixable losses through the Aggregating Algorithm; this mission focuses on the earlier deterministic-comparator result.

Setting

The feasible set $V$ is a closed, bounded, convex, full-dimensional subset of $\mathbb R^d$, with $d\geq1$. Its uniform distribution assigns a measurable subset probability equal to its Euclidean volume divided by $\operatorname{Vol}(V)$. Because $V$ is bounded and full-dimensional, its volume is finite and positive. Rounds are $t=1,\ldots,T$, with $T\geq1$. In round $t$, the learner predicts $x_t$, then observes a loss $\ell_t$ and pays $\ell_t(x_t)$. A competitor $u\in V$ is fixed across all rounds. Its regret is

$$R_T(u)=\sum_{t=1}^{T}\bigl(\ell_t(x_t)-\ell_t(u)\bigr).$$

For a parameter $\alpha>0$, a real-valued loss $\ell_t$ is $\alpha$-exp-concave on $V$ if $x\mapsto e^{-\alpha\ell_t(x)}$ is concave on $V$. Definition 7.31 in the source also permits a loss value of $+\infty$, with $e^{-\alpha(+\infty)}=0$. The mission defines that extended-valued concept for Proposition 7.34 and uses real-valued losses in its WAA target. The weighted average in round $t$ is

$$x_t=\frac{\int_V x\,\exp\!\left(-\alpha\sum_{s=1}^{t-1}\ell_s(x)\right)\,dx}{\int_V\exp\!\left(-\alpha\sum_{s=1}^{t-1}\ell_s(x)\right)\,dx}.$$

Thus $x_1$ is the centroid of $V$. This formula is Algorithm 11.1 with the uniform initial distribution and $1/\lambda_t=\alpha$. The existing published EWOO point definition uses precisely this one-based formula, so the mission imports that object. The integrals are with respect to Euclidean Lebesgue measure.

Formalization targets

The main target is Theorem 11.5, equation (11.6): for every $u\in V$,

$$R_T(u)\leq\frac d\alpha\left(1+\ln\left(\frac Td+1\right)\right).$$

The target fixes the exact dimension, horizon, and exp-concavity dependence from the source. It applies to each fixed competitor, with no distribution chosen in the statement. The milestone list records three source claims in reading order. Proposition 7.34 says that exp-concavity implies convexity, including the book's extended-real convention. Two displays in the proof of Theorem 11.5 describe the translated, contracted set $V'=\{\frac{T/d}{T/d+1}u+\frac{1}{T/d+1}w:w\in V\}$: the exponential losses there are bounded against those at $u$, and its uniform-prior mass is $1/(T/d+1)^d$. These are the chapter's explicit geometric and loss-comparison targets.

Significance

The theorem converts a distributional WAA guarantee into a bound for each deterministic competitor. Its dimension factor is $d$, and its logarithm contains $T/d+1$. This exact expression is sharper than replacing that logarithm by $\ln(T+1)$ for $d>1$; the distinction is visible in the target statement. A related EWOO result with the weaker $(d/\alpha)(1+\ln(T+1))$ form is already represented in the platform's library, but it does not establish the bound selected here. The source theorem is proved in the book; the remaining work is a machine-checked proof of this statement and the geometric milestones, with the source's constants intact.

The formal development can also support later results on exponentially weighted prediction. Its reusable pieces are the definition of exp-concavity, the extended-real epigraph convention, and the volume identity for a translated scaling of a convex body. The WAA prediction itself is represented by a previously published definition, giving future results a common algorithmic object rather than another copy of the same integral formula.

Difficulty

The general WAA statement compares the algorithm with a probability distribution, whereas Theorem 11.5 compares it with a point $u$. A point mass at $u$ is unsuitable as a comparator to a uniform continuous prior: it has no density with respect to that prior, so its relative entropy is infinite. The finite bound depends on identifying a region around $u$ that has positive uniform mass while retaining control of every exp-concave loss on that region. A formal treatment must also ensure that the weighted vector integral denotes an actual mean and that the normalization denominator is positive, rather than inheriting a default value from a total integral or division operator.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d), and a loss is indexed from round one; index zero is unused. The prior is uniform on $V$, and the point played is the published one-based EWOO weighted mean. The hypotheses $d,T\geq1$ make the printed ratios meaningful. Closedness, boundedness, convexity, and positive volume express the source's full-dimensional convex-body setting. The theorem additionally records almost-everywhere measurability of each loss on $V$, and integrability of each exponential weight and its vector moment; these are explicit analytic conditions for the real and Bochner integrals in Lean. They are not algorithmic restrictions or assumptions of the regret inequality's conclusion. Positive volume and integrability rule out a vacuous zero denominator or Lean's zero value for a non-integrable integral.

The source allows extended-real losses, but the goal uses real-valued losses on $V$. Proposition 7.34 separately retains the full extended-real statement through WithTop ℝ: $+\infty$ maps to zero under the exponential, and convexity is expressed by a convex epigraph. A complete proof needs the exp-concavity and Jensen facts, the weighted-mean properties on convex $V$, the measure and volume properties of $V'$, and the distributional WAA inequality from the chapter. Contributions that supply these lemmas under the stated conventions are within scope. The prediction cannot be replaced by an arbitrary point of $V$: the exact uniform-prior weighted mean is part of the goal.

Selected references

• Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. Chapter 11 and Proposition 7.34.

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.