Probability · Prove2Me

Numerical Analysis Partial Differential Equations·Captain: mikedeng1

Isotropic Gaussian Random Fields on the Sphere: Regularity, Fast Simulation and Stochastic Partial Differential Equations IV: Heat-Equation Spectral Truncation Error ≤ κ^{−β} a.s. for β < α/2Research Paper

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

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)$ .
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))}.

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

6 thms1 active userReviewed

Convex Optimization Machine Learning·Captain: mikedeng1

A Modern Introduction to Online Learning X: The Weighted Average Algorithm with a Uniform Prior Has Regret (d/α)(1 + ln(T/d + 1)) on α-Exp-Concave LossesTextbook

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.

7 thms1 active userReviewed

Statistics Stochastic Systems·Captain: mikedeng1

Limit Theorems for Nearly Unstable Hawkes Processes 2: When T(1 − a_T) → λ the Rescaled Intensity Converges in Law to a CIR Process and the Rescaled Hawkes Process to Its IntegralResearch Paper

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.

13 thms1 active userReviewed

Convex Optimization Machine Learning·Captain: mikedeng1

A Modern Introduction to Online Learning II: Online-to-Batch Conversion Turns a Regret Bound into a Risk Bound with Deviation 2√(2 ln(2/δ)/T)Textbook

Motivation

An online learning algorithm chooses a decision before seeing each round's data and is judged by regret: how much more loss it incurs than a fixed decision chosen in hindsight. Statistical learning asks a different question. After seeing data drawn from a distribution, how small is the decision's expected loss on another draw? Chapter 3 of Orabona's textbook connects these settings. It shows that a deterministic online rule with a pathwise regret guarantee also controls expected loss when its input data are independent samples. The chapter's high-probability result is the target here.

The distinction matters when an online guarantee is already available. A regret theorem holds for every loss sequence, including adversarial sequences, yet it does not by itself state what a learner achieves on future data from a distribution. The conversion supplies that statistical reading. It applies to the sequence of predictions produced along one sample path, with no need to select an empirical-risk minimizer from the full decision set. Chapter 3 also studies finite-set validation, in which a separate sample selects one candidate from a fixed collection Orabona, Chapter 3.

Setting

The decision set $V$ is a subset of Euclidean space $\mathbb R^d$ . A data point $z$ belongs to a measurable space $D$ and is drawn according to a probability distribution $\rho$ . The loss $f(x,z)$ lies in $[0,1]$ for every $x\in V$ and $z\in D$ , and is measurable as a function of $z$ when $x$ is fixed. Its true risk is $F(x)=\mathbb E_{z\sim\rho}[f(x,z)]$ . For a sample $\xi_1,\ldots,\xi_T$ drawn independently from $\rho$ , round $t$ presents the loss function $\ell_t(x)=f(x,\xi_t)$ .

A deterministic online algorithm produces predictions $x_1,\ldots,x_{T+1}$ in $V$ . Its prediction $x_t$ uses only $\xi_1,\ldots,\xi_{t-1}$ . For a fixed competitor $u\in V$ , its regret is $\operatorname{Regret}_T(u)=\sum_{t=1}^T\ell_t(x_t)-\sum_{t=1}^T\ell_t(u)$ . A proposed regret bound $R(u,T)$ is required to hold on every sample path and for every competitor $u$ . The risk comparison uses a minimizer of the full expression $F(u)+R(u,T)/T$ , whose existence the theorem assumes.

Formalization targets

The goal is Theorem 3.10, with $T\ge1$ and $0<\delta<1$ :

\mathbb P\!\left\{\frac1T\sum_{t=1}^T F(x_t) \le \min_{u\in V}\left(F(u)+\frac{R(u,T)}{T}\right) +2\sqrt{\frac{2\ln(2/\delta)}{T}}\right\}\ge1-\delta.

The minimum includes both risk and normalized regret. The theorem controls the average risk of the produced predictions; it does not require $F$ to be convex or claim the risk of their average decision. This makes the result applicable to decision sets and losses beyond the convex setting of the chapter's expectation result.

The first milestone is the two-sided bounded-martingale inequality of Theorem 3.9. A second milestone is the displayed concentration estimate in the proof of Theorem 3.10, which compares average true risk with average observed loss for the adaptive predictions. The final milestone is Theorem 3.17: if a fixed nonempty finite set $S\subseteq V$ is evaluated on fresh data and $\widehat x$ minimizes its empirical risk, then

F(\widehat x)\le\min_{x\in S}F(x) +2\sqrt{\frac{2\ln(2|S|/\delta)}{T}}

with probability at least $1-\delta$ Orabona, pp. 27–32.

Significance

The goal gives a direct way to read an online regret certificate as a distributional risk certificate. The bound retains the competitor-dependent function $R(u,T)$ inside the minimization: a decision with slightly larger risk but substantially smaller regret bound may give the better guarantee. Its deviation term has the exact constant and confidence dependence stated in the textbook. The finite-set theorem supplies a distinct validation guarantee for choosing one candidate from a fixed collection; it applies even when the risk is not convex.

Formalizing these results adds the probability layer absent from a deterministic regret statement: independent samples, a prediction rule constrained by past observations, true risk as an integral, and probability events for the adaptive sequence. Related online-to-batch statements already exist in the platform's developments of Hazan's online convex optimization text and Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning. They use different algorithm and loss models and do not state this competitor-dependent bound. The present mission records the precise Chapter 3 formulation as an open formal proof target; the local Lean statements compile, but their proofs are not supplied.

Difficulty

The observed loss $f(x_t,\xi_t)$ uses a prediction chosen from earlier observations, while the event in the goal concerns its expected loss $F(x_t)$ . Treating the predictions as fixed would ignore their dependence on the sample history. Allowing a prediction to inspect the current sample would break the comparison. The required concentration statement therefore has to retain the exact information available at each round. The comparator in the final bound is fixed before the samples are observed, while the online predictions remain sample dependent Orabona, proof of Theorem 3.10.

For the finite-set result, the selected predictor depends on the validation sample. A concentration estimate for a single fixed predictor does not immediately give the asserted guarantee for that selected predictor. The finite set must remain fixed before sampling, and the statement must account for every possible selected member.

Formalization scope

The Lean decision space is EuclideanSpace ℝ (Fin d). Samples are functions $\mathbb N\to D$ under the infinite product measure of $\rho$ ; their values at index zero are unused. The algorithm is a function of the full sample path constrained by a non-anticipation predicate: changing samples from round $t$ onward cannot change $x_t$ . Regret is against a fixed $u$ , with sums over rounds $1,\ldots,T$ . The pathwise regret guarantee quantifies over every sample path, so it cannot be replaced by an expected-regret assumption.

The integral defining $F$ is used with the book's measurable $[0,1]$ losses on $V$ , avoiding an undefined-integral convention. Measurability of each prediction, realized loss, and realized risk is stated explicitly where a probability event uses them. These regularity conditions make the probability statements meaningful and are the only extra conditions beyond the textbook's mathematical setup. A minimizer $u_\star\in V$ represents the assumed minimum in Theorem 3.10. The finite-set minimum is a real infimum whose input is nonempty, finite, and bounded. The positive horizon guards division by $T$ ; $0<\delta<1$ guards the logarithms. In Theorem 3.9, $B>0$ and $\varepsilon\ge0$ make its printed tail formula valid, including at the threshold boundary.

A complete development needs Mathlib's infinite product measure, filtration and martingale interfaces, conditional expectation or conditional moment bounds, and the sub-Gaussian concentration library. The risk, regret, non-anticipation, and empirical-risk definitions can be reused for later stochastic learning results. Contributions that establish the concentration milestone, connect it to the regret identity, or prove the finite-set validation statement all fit this scope.

Selected references

Francesco Orabona, Online Learning: A Modern Introduction Using Convex Optimization, arXiv:1912.13213v10, 2026. arXiv
Elad Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016; revised arXiv version, 2019. arXiv

5 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics XII: Multiple-State Insurance and Annuity CashflowsTextbook

Motivation and actuarial setting

Many insurance benefits depend on a policyholder's health or membership state rather than simply on being alive or dead. A disability annuity pays while a life occupies a disabled state; a critical illness or death benefit may be triggered by moving from one state to another. A rigorous multiple-state valuation therefore distinguishes payments for occupying a state from payments for a transition between states, and must also specify the timing of the payments.

The discrete-time models in Promislow, Fundamentals of Actuarial Mathematics, third edition, Chapter 19 §§19.2.1–19.2.3 [1], provide these two actuarial payment categories. Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8 [2], develop related multiple-state assumptions, transition probabilities, premium values and policy values. Norris, Markov Chains, §1.1 [3], supplies the finite-state stochastic-matrix foundation.

This mission develops the corresponding finite-horizon present-value formulas. It is the cashflow extension of the finite-state transition algebra in Mission X, but is designed as a self-contained draft while Mission X's definitions remain unpublished. The key mathematical obligations are correctly weighted transition benefits, state occupation annuities, finite-state distribution propagation, homogeneity and a capstone valuation decomposition.

Finite-state model and probability distributions

Let $S$ be a finite set of insurance states. At the start of policy year $k$ , let $\mu_{k,i}$ represent the probability of state $i$ , and let $P_{k,ij}$ be the conditional probability of occupying state $j$ at the end of the year, conditional on state $i$ at its start.

A state distribution must satisfy

\mu_{k,i}\ge0,\qquad \sum_{i\in S}\mu_{k,i}=1.

A valid one-year transition kernel has nonnegative entries and rows summing to one:

P_{k,ij}\ge0,\qquad \sum_{j\in S}P_{k,ij}=1.

The next year's marginal state distribution is obtained by propagating the current distribution through that kernel:

\mu_{k+1,j}=\sum_{i\in S}\mu_{k,i}P_{k,ij}.

The supporting theorems show that nonnegativity and total probability are preserved by this operation. The transition kernels are allowed to change from one year to the next. A separate path-space process need not be constructed to establish these finite-sum valuation identities, but $\mu$ and $P$ must obey the propagation relationship to represent one coherent Markov insurance model.

State-occupation payments

Let $c_{k,i}$ be the payment made at the beginning of policy year $k$ to a contract then occupying state $i$ . For example, it could represent a disability annuity paid only while the person is disabled. The expected amount at that payment time is

R^{\mathrm{occ}}_k=\sum_{i\in S}\mu_{k,i}c_{k,i}.

The expected present value of the state-occupation cashflows over $n$ policy years is

V_n^{\mathrm{occ}}= \sum_{0\le k<n}v^k\sum_{i\in S}\mu_{k,i}c_{k,i}.

A payment due at time zero is not discounted. A constant amount paid irrespective of state has its own expected value unchanged because the marginal state probabilities add to one. This is consistent with the state-occupation cashflow structure in [1, §19.2.3, equation (19.6)].

State-transition benefits

Let $b_{k,ij}$ be the benefit payable at the end of policy year $k$ when the contract transitions from state $i$ to state $j$ over that year. The expected one-year amount is

R^{\mathrm{tr}}_k= \sum_{i\in S}\sum_{j\in S} \mu_{k,i}P_{k,ij}b_{k,ij}.

The contract's expected present value of those transitions is

V_n^{\mathrm{tr}}= \sum_{0\le k<n}v^{k+1} \sum_{i\in S}\sum_{j\in S} \mu_{k,i}P_{k,ij}b_{k,ij}.

Unlike a reward depending only on the destination state, a transition-specific benefit may distinguish, for example, $i=\text{healthy}\to j=\text{disabled}$ from $i=\text{disabled}\to j=\text{disabled}$ . Keeping the pair $(i,j)$ explicit is necessary to represent such insurance benefits. This is the payment timing and transition structure considered in [1, §19.2.2, equations (19.2)–(19.4)].

Combined cashflows and capstone identity

The mission defines the complete finite-horizon value by adding the two types of cashflow:

\begin{aligned} V_n &=V_n^{\mathrm{occ}}+V_n^{\mathrm{tr}}\\ &=\sum_{0\le k<n}\left[ v^k\sum_i\mu_{k,i}c_{k,i} +v^{k+1}\sum_{i,j}\mu_{k,i}P_{k,ij}b_{k,ij} \right]. \end{aligned}

Because finite sums are linear, scaling both monetary benefit schedules by a constant $a\in\mathbb R$ scales the entire expected present value by $a$ :

V_n(ab,ac)=a\,V_n(b,c).

The capstone combines decomposition of the occupation and transition components with this scaling principle. Related milestones establish the zero-year, zero-benefit and one-year limits. For a one-year contract the exact timing reduces to

V_1=\sum_i\mu_{0,i}c_{0,i} +v\sum_{i,j}\mu_{0,i}P_{0,ij}b_{0,ij}.

The displayed formula is deterministic expected-value algebra for finite state probabilities, rather than a claim about a pathwise cashflow random variable. The later development of a stochastic path-space model, conditional benefits and second moments remains a separate task.

Formal proof structure and limitations

The proposed Lean draft contains five definitions: a finite-state probability distribution, one-step distribution propagation, expected transition-stage reward, expected occupation-stage reward and the combined finite-term PV. Thirteen supporting theorems prove probability propagation, zero and constant payments, scaling, valuation decomposition and the one-year boundary. The final capstone packages the overall value decomposition and benefit scaling.

The formal theorem statements do not require the cashflow amounts to be nonnegative because their linearity is algebraic. Probability interpretation additionally requires legitimate state probabilities and transition kernels. The source explicitly avoids interpreting arbitrary arrays $\mu_k$ and $P_k$ as the marginals of one Markov chain unless they satisfy the propagation identity.

These declarations are proposed mathematical obligations, not accepted proofs. Individual Lean modules import only the definitions their statements actually use, with all imports before Lean commands. Because the local definitions are not yet published as importable Prove2Me modules, downstream theorem previews must be revisited after their definitions are confirmed and published.

References

[1] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. Equations (19.2)–(19.4) address transition-based insurance benefits and equation (19.6) addresses occupation-based annuity benefits.

[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Multiple State Models, especially §§8.3–8.7 on states, transition probabilities, premiums and policy values.

[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, Chapter 1, §1.1 on stochastic matrices and discrete-time transition probabilities. The matrix-multiplication setting here permits different kernels at successive durations, in line with Promislow's non-stationary treatment.

19 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics XI: Annual Net Reserve RecursionTextbook

Motivation and actuarial setting

Prospective policy reserves measure the expected present value of an insurer's remaining benefits less remaining premiums, per policy still in force at a valuation date. When premiums and benefits occur at annual dates, consecutive reserve values satisfy a one-year cashflow balance. That recursion is central to valuation systems, reserve roll-forwards and the decomposition of a life insurance premium into risk and savings components.

This mission develops the annual net premium reserve recursion for a finite-term life assurance. It builds on the conceptual framework of prospective policy values without importing unconfirmed declarations from earlier Prove2Me missions. The principal actuarial sources are Gerber, Life Insurance Mathematics, third edition, Chapter 6 §6.3, notably equation (6.3.4) [1], and Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7 §7.3.3 [2]. Both develop the balance between an opening reserve, the premium due and the expected benefit plus closing reserve.

A key objective is correct treatment of impossible conditional events: the aggregate expected-loss recursion does not require next-year survival to have positive probability, while the familiar conditional-reserve formula needs the next year's reserve to be defined for an in-force life.

Time axis and cashflows

Let $K:\Omega\to\mathbb N$ be measurable curtate lifetime under a probability measure $P$ . Fix the contract term $n\in\mathbb N$ , integer valuation date $t$ , deterministic annual discount factor $v$ , death benefit $b$ and level premium $\pi$ . The insurer receives a premium at the start of each policy year $j<n$ for which $K\ge j$ . If $K<n$ , it pays the death benefit at the end of policy year $K$ , at calendar time $K+1$ .

The realised present value of the remaining net insurer loss, evaluated immediately before the time- $t$ premium, is

L_{n,t}(\omega) =bv^{K(\omega)+1-t} \mathbf1_{\{t\le K(\omega)<n\}} -\pi\sum_{t\le j<n}v^{j-t}\mathbf1_{\{K(\omega)\ge j\}}.

The date- $t$ premium appears in this expression and is worth one unit before multiplying by $\pi$ . Premiums earned before $t$ are excluded. The cashflow has finite calendar horizon even if the lifetime distribution is unbounded.

One-year death and survival partition

Define the probabilities of being in force, dying during the following year and surviving one further year by

S_t=P(K\ge t),\qquad D_t=P(K=t),\qquad S_{t+1}=P(K\ge t+1).

The event $\{K\ge t\}$ partitions into two disjoint events, $\{K=t\}$ and $\{K\ge t+1\}$ , so

S_t=D_t+S_{t+1}.

When $S_t>0$ , conditional annual death and survival probabilities are

q_t=\frac{D_t}{S_t},\qquad p_t=\frac{S_{t+1}}{S_t},\qquad q_t+p_t=1.

No annual death-event independence assumption is made. The result follows directly from the disjoint partition of a natural-valued lifetime.

Pathwise and aggregate cashflow recursions

For $t<n$ , the future loss satisfies the pointwise identity

L_{n,t}(\omega)+\pi\,\mathbf1_{\{K(\omega)\ge t\}} =vb\,\mathbf1_{\{K(\omega)=t\}} +vL_{n,t+1}(\omega).

If the person dies in year $t$ , the current premium is collected and the discounted death benefit becomes due. If the person survives, the one-step-discounted continuation accounts for all remaining premiums and the eventual death benefit. Before the start of the contract's surviving period, all relevant terms vanish.

Taking expectations and using integrability of the finite-term cashflow gives the unnormalised recurrence

\mathbb E_P[L_{n,t}]+\pi S_t =v\left(bD_t+\mathbb E_P[L_{n,t+1}]\right).

This identity remains meaningful when $S_{t+1}=0$ , because the future loss at $t+1$ is zero almost surely in that case. It is the safest formulation to prove before dividing by survival probabilities.

The conditional annual reserve

For $S_t>0$ , define the prospective reserve per policy in force at time $t$ as

V_t=\frac{\mathbb E_P[L_{n,t}]}{S_t}.

The Lean definition uses ordinary real division, which is totalised at zero, but the actuarial interpretation above is asserted only under a positive survival-probability assumption. If both $S_t>0$ and $S_{t+1}>0$ , substitute $\mathbb E[L_{n,t}]=S_tV_t$ and $\mathbb E[L_{n,t+1}]=S_{t+1}V_{t+1}$ into the aggregate identity. Division by $S_t$ yields

\boxed{V_t+\pi=v\bigl(q_tb+p_tV_{t+1}\bigr).}

The equation is the classical annual reserve balance: opening reserve plus premium equals the expected discounted claim and next-year reserve. Gerber [1, §6.3] also develops its decomposition into risk and savings premiums. This mission targets the core recursion and its probability and integrability prerequisites, rather than treating that later decomposition as already formalised.

The death-certain boundary $S_{t+1}=0$ is not hidden under a fictitious conditional reserve at $t+1$ . The aggregate identity above applies directly. A later extension can derive the explicit terminal conditional formula from it while preserving the zero-probability interpretation.

Formal graph and boundary cases

The draft introduces four definitions: the realised remaining loss, the in-force survival mass, death-year mass and prospective reserve quotient. Its twelve supporting theorems establish maturity and inception boundaries, the survival-event partition, conditional death/survival probabilities, loss integrability, the pointwise and integrated one-year recursions, reserve normalisation and the conditional reserve identity. A capstone combines the probability identity with the annual reserve recursion.

For $t\ge n$ , no covered future cashflow remains. At $t=0$ , $S_0=1$ , so the reserve is the unconditional expected loss at issue. The principal recursions allow any fixed real $v$ ; the usual insurance interpretation adopts a nonnegative discount factor. The proof obligations are finite-horizon and do not require a maximum possible lifetime.

The items are proposed Lean statements rather than accepted proofs. Their modules are dependency-ordered, with imports only at the beginning of each file. Until the supporting definitions have been individually published, downstream proof targets which import their modules must not be represented as ready for successful standalone compilation.

References

[1] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.3, Recursions, especially equations (6.3.4)–(6.3.10) and the premium risk/savings interpretation. Springer book DOI.

[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, §7.3.3, Recursive formulae for policy values. This chapter explicitly develops one-year annual policy-value recursions and related annual profit calculations.

[3] Open Actuarial Textbooks Project, Life Contingencies: Basic Life Contingent Benefits, Chapter 3, for the curtate-lifetime timing conventions used in the finite death-benefit and premium cashflows.

17 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics X: Finite-State Multiple-State ValuationTextbook

Motivation and actuarial context

Life-contingent benefits may depend on more than whether an insured life is alive or dead. Disability, recovery, critical illness and multiple causes of exit can all be represented by finite sets of states with possible transitions between them. Multiple-state models make it possible to value benefits on a transition, annuities paid while occupying a state, and different amounts payable according to the insured's health or other status. Dickson, Hardy and Waters develop the actuarial multiple-state setting in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 8 [1]. Promislow presents a discrete-time, potentially non-stationary Markov model and its insurance and annuity applications in Fundamentals of Actuarial Mathematics (2015), §§19.2.1–19.2.3 [2].

This mission establishes the finite-state, discrete-time algebra needed before tackling more difficult continuous-time transition intensities, differential equations or multistate reserves. The capstone connects composition of transition matrices with discounted state-dependent cashflows. The mathematical emphasis is on correct probabilities, annual timing and finite sums.

Discrete-time transition kernel

Let $S$ be a nonempty finite set of possible policyholder states. For one policy year, define $P_{ab}$ as the probability of ending the year in state $b$ , conditional on starting in state $a$ . To represent a genuine transition kernel it must satisfy

P_{ab}\ge0,\qquad \sum_{b\in S}P_{ab}=1 \quad(a,b\in S).

The model allows a different transition matrix in each year. It does not assume a constant transition law or that every state can reach every other state. For two successive policy years, with transition kernels $P$ and $Q$ , the two-step transition probability is

(PQ)_{ac}=\sum_{b\in S}P_{ab}Q_{bc}.

The intermediate state $b$ is summed out. This is the finite Chapman–Kolmogorov composition used in the non-stationary discrete Markov chain of [2, §19.2.1]. The proof must show that composing two nonnegative row-stochastic kernels produces another nonnegative row-stochastic kernel. Associativity,

(PQ)R=P(QR),

then permits an arbitrary finite sequence of yearly transition matrices to be grouped without changing the resulting transition probabilities.

The matrix calculations alone are not a theorem asserting that an arbitrary stochastic process has the Markov property. They formalise the transition-probability algebra assuming the yearly probabilities are the kernels of a Markov model. Proving a full path-space conditional-probability construction is outside this mission.

Discounted state-dependent cashflows

Suppose an annual payment depends on the state occupied after the next transition. Write $r_b$ for the amount paid at the next year end when the new state is $b$ , and $N_b$ for the continuation value at that date. Let $v$ be the deterministic one-period discount factor. The one-step prospective value in current state $a$ is

V(a)=v\sum_{b\in S}P_{ab}(r_b+N_b).

Both $r$ and $N$ are measured at the next year end, so this formula applies precisely one period of discounting to both. A constant amount $c$ paid at the next year end has value $vc$ , by the row-sum property. The valuation operator is linear in reward and continuation cashflows, and it is nonnegative when the discount factor, transition probabilities and cashflows are nonnegative.

For a payment $r_c$ arising only at the end of the second year, the two-stage recursion simplifies to

\begin{aligned} V_0(a) &=v\sum_b P_{ab} \left(v\sum_cQ_{bc}r_c\right)\\ &=v^2\sum_c(PQ)_{ac}r_c. \end{aligned}

This identity reconciles backward valuation with forward transition-probability composition. It is the discrete precursor to larger actuarial valuation and reserve recursions. Promislow's §§19.2.2–19.2.3 discuss state- and transition-dependent insurance and annuity cashflows [2].

Boundary conditions and limitations

When the discount factor is zero, a payment made only at the next year end has zero present value. When all future rewards and continuation values are zero, the valuation is zero. Neither algebraic identity requires a particular health-state interpretation.

The theorem graph uses a finite state type and sums over all states. A true actuarial example must supply valid transition probabilities, distinguish payments made on entering a state from those made for occupying the state, and preserve the timing of an insurance payment at the end of the year. No independence between annual state indicators is assumed. Multistate variance calculations need joint transition probabilities rather than naively treating indicators as independent [2, §19.2.2].

The mission creates three definitions, twelve supporting theorems and one capstone. The proof path begins with row normalisation and nonnegativity, proves composition and associativity, and then develops constant, zero, linear and two-step discounted reward identities. The capstone combines the preservation of a stochastic kernel, associative composition and the two-step reward valuation.

These are proposed Lean theorem statements, not claims of completed proofs. This draft uses Mathlib's finite-sum and elementary order algebra, with no reliance on unpublished actuarial mission definitions.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, Chapter 8, Multiple State Models, especially §§8.2–8.4. This provides the actuarial interpretation of state transitions and the Markov modelling assumptions.

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. The discrete non-stationary transition model and subsequent state-dependent life insurance and annuity examples are the direct cashflow motivation.

[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, §1.1, Definition and Basic Properties. The book defines a stochastic matrix by its probability-distribution rows and states Theorems 1.1.1–1.1.3 on the Markov property and powers of the transition matrix. Its basic homogeneous-chain construction is a supporting special case, not an assertion that the time-varying matrices in this mission are all equal.

16 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics IX: Prospective Term Insurance ReservesTextbook

Motivation and actuarial context

A net premium is usually set at policy inception. As an insured life survives and the remaining insurance term shortens, the expected future claim outgo and future premium income change. A prospective policy value measures the expected present value of the insurer's future loss on a policy that is still in force at the valuation date. This is the natural next stage after the equivalence principle of Actuarial Mathematics VIII. Dickson, Hardy and Waters provide the insurer's future-loss definition and the annual-cashflow policy-value framework in Actuarial Mathematics for Life Contingent Risks (2009), Chapter 7, §§7.3.1–7.3.3 [1]. Promislow covers both deterministic reserve recursions and the stochastic approach to reserves [2].

This mission formalises a finite-term life-assurance reserve at an integer valuation duration. Its central feature is survival conditioning: the reserve is a liability per surviving in-force policy, rather than the unconditional present value of the original contract. Separating these quantities avoids a common modelling error in stochastic policy values.

Model, contract timing and in-force event

Let $K:\Omega\to\mathbb N$ be measurable curtate future lifetime under a probability measure $P$ . Let $n\in\mathbb N$ denote the term, $t\in\mathbb N$ the valuation duration, $v\in\mathbb R$ a fixed per-period discount factor, $b\in\mathbb R$ the death benefit and $\pi\in\mathbb R$ the annual level premium.

Premiums are payable in advance at integer times $j<n$ while the life is alive. The benefit, if payable, occurs at the end of the year of death, at date $K+1$ . Only cashflows on or after duration $t$ enter the reserve, with discount exponents measured from $t$ .

The in-force survival event is

S_t=\{\omega\in\Omega:K(\omega)\ge t\}.

When $P(S_t)>0$ , conditioning on this event gives the valuation basis for policies in force at $t$ . A statement about reserves conditional on survival must not silently assume that $P(S_t)>0$ .

Future benefit, premium and loss values

The remaining unit term-assurance benefit present value is

B_{n,t}(\omega)= \mathbf1_{\{t\le K(\omega)<n\}}\,v^{K(\omega)+1-t}.

The remaining premium-annuity present value is

Y_{n,t}(\omega)= \sum_{t\le j<n} v^{j-t} \mathbf1_{\{K(\omega)\ge j\}}.

The realised future net loss is therefore

L_{n,t}(\omega;b,\pi)= bB_{n,t}(\omega)-\pi Y_{n,t}(\omega).

These finite expressions make it explicit whether a premium due at the valuation instant is included. Here $t$ is immediately before the premium at time $t$ , consistent with an annual premium payable in advance. The choice is essential when comparing reserve formulas across valuation conventions.

At $t=0$ the in-force event is certain. At or after $t=n$ , both remaining cashflow components vanish because the contract's coverage and premium period have ended.

Prospective reserve and normalisation

For positive survival probability, the prospective term-policy reserve per in-force policy is

V_{n,t} =\mathbb E_P[L_{n,t}\mid S_t] =\frac{\mathbb E_P[L_{n,t}]}{P(S_t)}.

The second equality holds because the model defines the realised future loss as zero outside $S_t$ . It is a conditional-event expectation, rather than an unrestricted claim about conditional expectation with respect to an arbitrary sigma-algebra. The formal quotient definition makes the denominator explicit, and the principal reserve interpretation and capstone theorem retain $P(S_t)>0$ as a hypothesis.

Linearity separates the reserve into benefit and premium components:

V_{n,t}= b\,\mathbb E_P[B_{n,t}\mid S_t] -\pi\,\mathbb E_P[Y_{n,t}\mid S_t].

In particular, multiplying both cashflow amounts by $c\in\mathbb R$ gives

V_{n,t}(cb,c\pi)=cV_{n,t}(b,\pi).

The finite payment period ensures integrability for any fixed real discount factor. When studying economic reserve properties, a nonnegative or positive discount factor can be imposed separately. No assumption of independence between survival indicators, benefits and premiums is made.

Boundary cases and formalisation strategy

The principal boundary checks are survival at inception, $t=0$ ; exhaustion of cover at $t\ge n$ ; finite sums with $n=0$ ; and zero in-force probability. The total real-valued quotient happens to evaluate to zero when both its numerator and denominator are zero in Lean, but this does not create an actuarially meaningful conditional reserve for an impossible in-force event. The descriptive and main conditional theorems are explicitly scoped to positive probability.

Five definitions provide the in-force event, future benefit PV, future premium PV, future loss PV and the prospective reserve. Supporting theorems develop survival-event measurability, cashflow boundaries, nonnegativity where applicable, integrability, inception valuation, benefit–premium decomposition and scaling. The capstone combines the survival-normalised expected-loss identity, valuation decomposition and scaling.

The formalisation is deliberately self-contained at the level of future cashflow definitions so the owner Draft does not depend on the unconfirmed publication of any Mission VIII declarations. The intended later bridge is an exact identity between the duration-zero future loss and the loss-at-issue formula from Mission VIII, once those definitions are published. All theorems are proposed proof targets, not assertions of accepted proofs.

Gerber [4, §§6.3 and 6.5] provides an independent treatment of net premium reserves and annual reserve recursions. Its equation (6.5.6) expresses a whole-life net reserve through the premium difference, illustrating the same prospective viewpoint but not asserting the more general term-reserve theorem of this mission.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 7, Policy Values, Cambridge University Press. Relevant sections: §7.3.1 (future loss), §7.3.2 (policy values for annual cashflows) and §7.3.3 (recursive policy values), printed pages 176–195.

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. In particular §6.3 (reserve recursion) and §15.5 (stochastic reserves).

[3] Dickson, Hardy and Waters (2009), Chapter 6, §6.5.1, equation (6.1), on the equivalence principle at policy inception, publisher book record.

[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, Net Premium Reserves, §6.3 and §6.5, including the premium-difference reserve formula (6.5.6).

19 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics VIII: Net Level Premiums and the Equivalence PrincipleTextbook

Motivation and actuarial context

The equivalence principle is one of the foundational methods of setting premiums for life-contingent contracts. It requires that the insurer's expected present value of future benefits equal the expected present value of future net premium income at policy inception. As a result, the expected present value of the net future-loss random variable is zero. Dickson, Hardy and Waters define the net future-loss random variable in Actuarial Mathematics for Life Contingent Risks (2009), §6.4, and state the equivalence principle in §6.5.1, equation (6.1) [1]. Promislow develops the corresponding stochastic premium principle in Fundamentals of Actuarial Mathematics (2015), §15.6.1 [2].

This mission makes that principle a rigorous theorem for a finite-term life assurance financed by level premiums payable annually in advance. It proves that a unique net premium exists when at least one premium is due and nonnegative discount factors are used, and it separately addresses the zero-term case where uniqueness fails. The formal treatment distinguishes realised loss from expected loss, keeps mortality and discounting assumptions explicit, and avoids treating survival-contingent benefits and premiums as independent.

Insurance contract, premium dates and realised loss

Let $(\Omega,P)$ represent the probability space, with a measurable natural-valued curtate future lifetime $K$ . Let $n\in\mathbb N$ denote the policy term, $v\in\mathbb R$ the annual discount factor, $b\in\mathbb R$ a deterministic death benefit and $\pi\in\mathbb R$ a level premium.

A unit $n$ -year term assurance pays once, at the end of the year of death, if death occurs within the covered term. Its realised benefit present value is $A_n$ , reusing the published definition from Actuarial Mathematics II. In conventional cashflow notation,

A_n(\omega)= \sum_{0\le k<n}v^{k+1}\mathbf 1_{\{K(\omega)=k\}}.

This is the discrete term-assurance structure from [3, §3.2.2, equation (3.8)]. Premiums are due at the start of each covered year while the insured remains alive. The realised present value of unit premium income is

Y_n(\omega)= \sum_{0\le k<n}v^k\mathbf 1_{\{K(\omega)\ge k\}}.

The insurer's discounted net future loss at inception is then

L_n(\omega;\pi,b) =bA_n(\omega)-\pi Y_n(\omega).

The same curtate lifetime determines both premium income and death benefit outgo. No independence assumption is made between these two random variables.

The equivalence-principle premium

Because the sums are finite, their measurability and integrability can be established from measurability of $K$ for any finite real $v$ . Linearity of expectation gives

\mathbb E_P[L_n(\pi,b)] =b\mathbb E_P[A_n]-\pi\mathbb E_P[Y_n].

For a positive term $n\ge1$ and $v\ge0$ , the first premium at time zero is certain: $v^0=1$ . All subsequent premium present values are nonnegative. Consequently,

Y_n(\omega)\ge1, \qquad \mathbb E_P[Y_n]\ge1>0.

The denominator in the premium formula is therefore strictly positive. Solving the linear expected-loss equation leads to the net level premium

\pi^*(b)= \frac{b\mathbb E_P[A_n]}{\mathbb E_P[Y_n]}, \qquad \mathbb E_P[L_n(\pi^*(b),b)]=0.

The theorem also proves uniqueness: any real premium $\pi$ satisfying $\mathbb E_P[L_n(\pi,b)]=0$ must equal $\pi^*(b)$ . This is the formal analogue of the equivalence premium calculation in [1, equation (6.1)]. As a related worked example, [1, equation (6.2)] gives a net premium for an endowment contract using the ratio of benefit and premium-annuity values. The mission specialises the general principle to an $n$ -year term assurance.

Scaling, boundaries and assumptions

Linearity yields the scaling identity

\pi^*(cb)=c\pi^*(b)

for any constant $c$ . In particular, a zero benefit produces a zero premium under the ratio definition. A nonnegative benefit gives a nonnegative premium when $0\le v$ , although the core algebraic scaling theorem does not require positive $b$ .

The boundary $n=0$ is deliberately distinct. Neither a term-assurance benefit nor a premium can occur, so $A_0=Y_0=L_0=0$ . Every quoted level premium has zero expected loss in this empty contract, and uniqueness does not follow. The ratio definition is therefore paired with explicit theorem hypotheses rather than falsely suggesting a unique zero-term premium.

At $v=0$ and $n\ge1$ , the certain initial premium remains payable at inception, while all covered death benefits are paid at strictly positive times and have zero discounted value. The net premium is zero. At $v=1$ , all payment sums remain finite and integrable for fixed $n$ , so no artificial upper bound $v<1$ is needed for these finite-term results.

Formalisation and dependency structure

The mission introduces three definitions: the realised finite premium annuity-due present value, the realised term-policy loss, and the equivalence net premium. Supporting theorems establish the initial premium lower bound, measurability and integrability, positivity of the expected premium annuity, linearity of expected loss, existence and uniqueness of the equivalence premium, benefit scaling, and the zero-term and zero-discount boundaries. The capstone combines positivity, zero expected loss, uniqueness and benefit scaling.

The only previously published actuarial definition imported is the $n$ -year term-assurance present value from Mission II. The mathematical arguments use finite sums and integration under a probability measure, rather than relying on unproved statements from other draft missions. All declarations in this owner Draft are mathematical proof targets. Their presence in a proposal does not mean that their proofs have been accepted.

Gerber [4, §5.3.1] independently develops annual-premium term insurance, including its realised loss and the net premium equations (5.3.9)–(5.3.11). Those results corroborate the payment timing and the equivalence-premium construction adopted here.

References

[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, book DOI 10.1017/CBO9780511800146. See §6.4, The present value of future loss random variable, and §6.5.1, Net premiums, particularly equations (6.1)–(6.2).

[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. See §15.6.1, The equivalence principle, and §15.6, The stochastic approach to premiums.

[3] Open Actuarial Textbooks Project, Life Contingencies, Chapter 3, Basic Life Contingent Benefits, §3.2.2, equation (3.8), finite term assurance.

[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 5, Net Premiums, particularly §5.3.1, equations (5.3.9)–(5.3.11), on finite term insurance and net annual premiums.

19 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics VII: Flat-Interest Assurance–Annuity EquivalenceTextbook

Motivation and actuarial context

Whole-life assurance and a whole-life annuity-due are two fundamental life-contingent contracts. The assurance provides one unit of benefit at the end of the year of death, whereas the annuity-due provides one unit at the start of each year that the life is still eligible for payment, including time zero. Under a constant positive effective annual interest rate, their realised present values satisfy an exact finite-geometric-series identity. This provides an unusually direct connection between insurance benefits, annuity values and the distribution of curtate future lifetime. The relationship and its expected-value and variance consequences are stated in Life Contingencies, Chapter 3, equations (3.13)–(3.14) [1].

This mission formally develops that equivalence in Lean, starting from the individual cashflows and ending with a capstone theorem that combines the pointwise, expectation and variance results. It also isolates the assumptions needed for these results, supplies reusable bounds and integrability lemmas, and treats the zero-interest boundary separately. Related treatments of whole-life insurance and life annuities are available in the actuarial textbooks of Promislow [2] and Dickson, Hardy and Waters [3]. The mission's declarations are proposed proof obligations, not claims that every theorem has already been proved.

Contracts and notation

Let $K:\Omega\to\mathbb N$ be the natural-valued curtate future lifetime of the insured life. In outcome $\omega$ , death occurs during policy year $K(\omega)+1$ . Let $i>0$ be a flat, deterministic annual effective interest rate and define

v=\frac{1}{1+i},\qquad 0<v<1.

The unit whole-life assurance, payable at the end of the year of death, has realised present value

Z_A(\omega)=v^{K(\omega)+1}.

This is the assurance contract defined in [1, §3.2.1, equation (3.7)]. The unit whole-life annuity-due makes payments at dates $0,1,\ldots,K(\omega)$ and therefore has realised present value

Z_D(\omega)=\sum_{k=0}^{K(\omega)}v^k.

The annuity cashflow and the flat-interest specialisation are discussed in [1, §3.3.1, equations (3.11) and (3.13)]. The difference in timing is essential: the assurance payment occurs at $K+1$ , one year after the last annuity-due payment at $K$ .

Pointwise assurance–annuity equivalence

For $i>0$ , the finite geometric sum gives

\begin{aligned} Z_D(\omega) &=\frac{1-v^{K(\omega)+1}}{1-v}\\ &=\frac{1+i}{i}\bigl(1-Z_A(\omega)\bigr). \end{aligned}

Equivalently, writing $d=i/(1+i)=1-v$ for the annual effective rate of discount,

Z_A(\omega)+dZ_D(\omega)=1.

These are pathwise statements. They hold for every realised natural-valued lifetime and require no assumptions about a mortality law or independence between annual survival events. They formalise the finite-series relationship in [1, equation (3.13)], rather than relying on an approximation or a selected life table.

Expected present values and variance

Now let $P$ be a probability measure on $\Omega$ and suppose that $K$ is measurable. The assumption $i>0$ implies $0<v<1$ , and the realised values obey

0<Z_A(\omega)\le 1, \qquad 0\le Z_D(\omega)\le\frac{1+i}{i}.

These deterministic bounds establish integrability, including the required second moments, even where $K$ has unbounded support across outcomes. Taking expectations of the pointwise identity yields

\mathbb E_P[Z_D] =\frac{1+i}{i}\left(1-\mathbb E_P[Z_A]\right).

If $A_x=\mathbb E_P[Z_A]$ and $\ddot a_x=\mathbb E_P[Z_D]$ denote the corresponding actuarial values for a life aged $x$ , then

\ddot a_x=\frac{1+i}{i}(1-A_x).

Translation by a constant leaves variance unchanged, and scaling multiplies variance by the square of the factor. Thus

\operatorname{Var}_P(Z_D) =\left(\frac{1+i}{i}\right)^2 \operatorname{Var}_P(Z_A).

The EPV and variance identities are stated in [1, equation (3.14)]. In particular, the variance factor is squared. No independence assumption is imposed: the assurance and annuity values are functions of the same lifetime, and the variance identity follows from their exact affine relationship.

Interest-rate boundary and scope

At zero interest, $v=1$ , the whole-life annuity-due has realised value

Z_D(\omega)=\sum_{k=0}^{K(\omega)}1=K(\omega)+1.

This is a separate pointwise theorem. The expression $(1+i)/i$ is undefined at $i=0$ , and an arbitrary distribution of $K$ need not give a finite undiscounted expected payment count or a finite variance. An expectation theorem at zero interest would require a suitable first-moment assumption on $K$ , while a finite variance requires a second moment.

The simple assurance–annuity equivalence also relies on a flat deterministic interest basis. Under a non-flat yield curve the discounted cashflow series has varying discount factors and the same fixed geometric multiplier does not generally exist. The source expressly makes this limitation in [1, §3.3.1].

Formalisation and proof structure

The mission adds one definition, the whole-life assurance realised present value, together with eleven supporting theorems and one capstone. The supporting graph establishes discount-factor positivity, the finite geometric sum, assurance positivity, the pointwise and unit identities, a boundedness lemma, integrability of both contracts, and their expected-value and variance relationships. A separate theorem handles zero interest. The capstone combines the key pathwise identity, expected-value relation, variance scaling and unit identity.

The only imported published actuarial definition is the existing whole-life annuity-due present-value definition from the earlier mission. The assurance definition is introduced here. The proposed proofs should use the appropriate finite-sum and probability-measure results from the pinned Mathlib, and no unproved theorem from another actuarial mission should be treated as an available proof dependency. These formal dependencies are distinct from the published textbook references below.

References

[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal results: §3.3.1, equations (3.13)–(3.14), on the flat-interest annuity identity, EPV and variance. Assurance definition: §3.2.1, equation (3.7). Whole-life annuities: §3.3.1, equations (3.11)–(3.12).

[2] Promislow, S. David (2010), Fundamentals of Actuarial Mathematics, Wiley. Publisher book record, particularly Chapters 4, Life Annuities, and 5, Life Insurance. This provides wider actuarial background rather than an attribution of equations (3.13)–(3.14) to Promislow.

[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, particularly Chapters 4, Insurance Benefits, 5, Annuities, and 12, Yield Curves and Non-Diversifiable Risk. These chapters provide context for contract valuation and the distinction between flat and varying interest rates.

14 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics VI: Guaranteed Life AnnuitiesTextbook

Motivation and actuarial context

A whole-life annuity provides payments contingent on the annuitant remaining alive. A guaranteed life annuity adds a minimum number of payments, irrespective of early death. This alters the insurer's cashflows, since payments during the guarantee period are certain and subsequent payments depend on survival. It is an important contract structure for retirement income and provides a natural bridge between annuities certain, whole-life annuities and deferred life annuities. The payment definitions and expected present values are given in the Open Actuarial Textbooks Project's Life Contingencies, Chapter 3, §3.3.4, equations (3.19) and (3.20) [1]. Guaranteed payments are also covered within the broader treatments of life annuities in [2] and [3].

The objective of this mission is to formalise both annuities payable in advance (due) and annuities payable in arrears (immediate), including their exact cashflow decompositions, expected values and variances. It develops the mathematical justification for infinite survival-weighted sums when the distribution of lifetime is not bounded above. These are formal theorem targets to be proved, rather than results already established merely by publishing the statements.

Contract definition and payment timing

Let $K:\Omega\to\mathbb N$ be curtate future lifetime, where $K(\omega)$ is the number of complete future years lived in outcome $\omega$ . Let $n\in\mathbb N$ be the number of guaranteed annual payments and let $v\in\mathbb R$ be a constant per-period discount factor. Each payment has unit amount, and an empty sum has value zero.

For an annuity-due, payments occur at times $0,1,\ldots$ . The first $n$ payments at times $0,\ldots,n-1$ are certain. Additional payments occur at times $n,\ldots,K(\omega)$ , if any.

For an annuity-immediate, payments occur at times $1,2,\ldots$ . The first $n$ payments at times $1,\ldots,n$ are certain. Additional payments occur at times $n+1,\ldots,K(\omega)$ , if any. The separate timing conventions are essential to the guaranteed-period boundary cases.

Realised present-value identities

The guaranteed annuity-due has realised present value

\begin{aligned} Z_{G,\mathrm{due}}(\omega) &=\sum_{0\le k<\max\{K(\omega)+1,n\}}v^k\\ &=\underbrace{\sum_{0\le k<n}v^k}_{C_{\mathrm{due}}} +\underbrace{\sum_{n\le k\le K(\omega)}v^k}_{D_{\mathrm{due}}(\omega)}. \end{aligned}

For an annuity-immediate, the corresponding identity is

\begin{aligned} Z_{G,\mathrm{imm}}(\omega) &=\sum_{0\le k<\max\{K(\omega),n\}}v^{k+1}\\ &=\underbrace{\sum_{0\le k<n}v^{k+1}}_{C_{\mathrm{imm}}} +\underbrace{\sum_{n\le k<K(\omega)}v^{k+1}}_{D_{\mathrm{imm}}(\omega)}. \end{aligned}

Here $C$ is the deterministic annuity-certain prefix and $D$ is the survival-dependent deferred continuation. The equations reproduce the underlying payment timing of [1, equations (3.19)–(3.20)]. They also connect to the deferred-annuity formulas in [1, equations (3.17)–(3.18)]. Additional pointwise theorems express each guaranteed value as its corresponding whole-life value plus the extra payments required when death occurs during the guarantee.

Expected values and variance

Let $P$ be a probability measure and assume that $K$ is measurable. For the analytical theorems, impose $0\le v<1$ . Write $\Pr(K\ge k)=P(\{\omega:K(\omega)\ge k\})$ . The expected present values are

\mathbb E_P[Z_{G,\mathrm{due}}] =\sum_{0\le k<n}v^k +\sum_{k=n}^{\infty}v^k\Pr(K\ge k)

and

\mathbb E_P[Z_{G,\mathrm{imm}}] =\sum_{0\le k<n}v^{k+1} +\sum_{k=n}^{\infty}v^{k+1}\Pr(K\ge k+1).

The fixed prefix and survival-weighted tail are those in the guaranteed-annuity textbook formulas [1]. A formal proof must establish measurability and integrability and justify taking expectation through the infinite sum. The geometric bound supplied by $0\le v<1$ makes these conclusions possible for a natural-valued lifetime distribution with unbounded support. No maximum attainable lifetime is assumed.

Since $C_{\mathrm{due}}$ and $C_{\mathrm{imm}}$ are deterministic, adding them changes the expected values but does not change the variances:

\begin{aligned} \operatorname{Var}_P(Z_{G,\mathrm{due}}) &=\operatorname{Var}_P(D_{\mathrm{due}}),\\ \operatorname{Var}_P(Z_{G,\mathrm{imm}}) &=\operatorname{Var}_P(D_{\mathrm{imm}}). \end{aligned}

These variance equalities are derived theorems, based on translation invariance of variance, rather than separate numbered statements in §3.3.4. The general survival-cashflow moment framework in [1, §3.1.1, equations (3.3), (3.5)–(3.6)] supplies background. No independence assumption between annual survival events is introduced.

Boundary cases and formal proof structure

When $n=0$ , both guaranteed annuities reduce to their corresponding whole-life annuities. When $K(\omega)=n$ , the due annuity can still pay at time $n$ , while the immediate deferred continuation is empty and the $n$ guaranteed immediate payments remain. When $K(\omega)=0$ , the due contract has its time-zero payment, and an immediate contract with $n>0$ still pays the $n$ certain instalments.

The finite realised-value identities hold algebraically for every real $v$ , including zero, one and negative values. The stated integrability, infinite expected-value and variance theorems deliberately use $0\le v<1$ . In particular, an arbitrary undiscounted lifetime distribution need not have a finite expected payment count.

The mission introduces four definitions, fourteen supporting theorems and one capstone. The intended proof path establishes cashflow decompositions and zero-guarantee identities, develops geometric bounds and measurable survival events, proves the expected-value and variance relations, and then assembles the capstone from the supporting results.

The formal dependency graph reuses six published Prove2Me declarations: the curtate-survival event and its measurability theorem, together with whole-life and deferred present-value definitions for due and immediate annuities. These are technical dependencies, distinct from the bibliographic sources below. An unproved theorem from an earlier mission is not treated as an available proof dependency.

References

[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal source: §3.3.4, equations (3.19)–(3.20). Related foundations: §3.3.1 (3.11)–(3.12), §3.3.3 (3.17)–(3.18), and §3.1.1 (3.3), (3.5)–(3.6). The explanatory sentence after (3.20) calls the contract deferred, although the section heading and displayed expressions describe a guaranteed annuity.

[2] Promislow, S. David (2010), “Life Annuities”, Chapter 4 of Fundamentals of Actuarial Mathematics, Wiley, DOI: 10.1002/9781119971528.ch4. The chapter's published summary includes guaranteed payments.

[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapter 5, Annuities. General context for life-annuity valuation.

27 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics V: Whole-Life and Deferred Life AnnuitiesTextbook

Motivation

Whole-life and deferred life annuities extend survival-contingent payments beyond a fixed policy term. A whole-life annuity may pay on each eligible anniversary until death, while a deferred annuity begins after a specified waiting period. Both are standard components of pension and life-contingency valuation.

Actuarial Mathematics I established how to value finite cashflows. Missions III and IV provide curtate survival events and temporary annuity schedules. This mission develops the infinite-horizon valuation step: it justifies the lifetime payment series and its expected present value, including the conditions under which expectation can be exchanged with the discounted survival series.

The mortality and discount model

Let $(\Omega,\mathcal F,P)$ be a probability space and let $K:\Omega\to\mathbb N$ be a measurable curtate future lifetime. Define the survival event at time $k$ by

S_k=\{\omega:K(\omega)\ge k\}.

For expected present value statements, assume a deterministic annual discount factor $v$ satisfying

0\le v<1.

This condition provides a geometric bound on the payments and justifies exchanging expectation with the discounted survival series. No particular life table or independence between survival dates is assumed, and $K$ need not have a finite upper bound.

Whole-life annuities

With unit payments in advance, a life with realised curtate lifetime $K(\omega)$ receives a payment at time zero and at each subsequent beginning-of-year date through time $K(\omega)$ . Its present value can be written

Z_{\mathrm{WL,due}}(\omega)=\sum_{k=0}^{K(\omega)}v^k =\sum_{k=0}^{\infty}v^k\mathbf1_{\{K(\omega)\ge k\}}.

Its expected present value, given by equation (3.11), is

\mathbb E_P[Z_{\mathrm{WL,due}}] =\sum_{k=0}^{\infty}v^kP(S_k).

A whole-life annuity in arrears pays at times $1,\ldots,K(\omega)$ , with no payment at time zero:

Z_{\mathrm{WL,immediate}}(\omega) =\sum_{k=0}^{\infty}v^{k+1}\mathbf1_{\{K(\omega)\ge k+1\}}.

Equation (3.12) gives its expected present value:

\mathbb E_P[Z_{\mathrm{WL,immediate}}] =\sum_{k=0}^{\infty}v^{k+1}P(S_{k+1}).

The payment in advance at time zero is certain, and the remaining payments match the arrears stream. Thus their pointwise and expected values satisfy

Z_{\mathrm{WL,immediate}}=Z_{\mathrm{WL,due}}-1.

Deferred life annuities

For a deferral period $n\in\mathbb N$ , a deferred annuity in advance has its first possible payment at time $n$ , with no payments before then. Equation (3.17) gives its indicator representation:

Z_{\mathrm{deferred,due}} =\sum_{k=n}^{\infty}v^k\mathbf1_{\{K\ge k\}},

and its expected present value is

\mathbb E_P[Z_{\mathrm{deferred,due}}] =\sum_{k=n}^{\infty}v^kP(S_k).

A deferred annuity in arrears starts at time $n+1$ and requires survival to that date. Equation (3.18) gives

Z_{\mathrm{deferred,immediate}} =\sum_{k=n}^{\infty}v^{k+1}\mathbf1_{\{K\ge k+1\}},

with expected present value

\mathbb E_P[Z_{\mathrm{deferred,immediate}}] =\sum_{k=n}^{\infty}v^{k+1}P(S_{k+1}).

The timing conditions matter. If $K=n$ , there is a due payment at time $n$ , but no immediate payment at time $n+1$ . When $n=0$ , each deferred annuity is its corresponding whole-life annuity.

Whole-life values minus temporary annuities

The discounted cashflows in equations (3.17) and (3.18) are the corresponding whole-life streams with the first $n$ potential payment dates removed. Pointwise, this gives

Z_{\mathrm{deferred,due}} =Z_{\mathrm{WL,due}} -\sum_{k=0}^{n-1}v^k\mathbf1_{S_k},

and

Z_{\mathrm{deferred,immediate}} =Z_{\mathrm{WL,immediate}} -\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{S_{k+1}}.

Taking expectations gives the source's deferred-annuity valuation differences: each deferred annuity's expected present value is the corresponding whole-life expected present value less that of the temporary annuity.

The finite prefix sums reproduce the temporary-annuity schedules from Mission IV without importing its unpublished declarations. Mission IV remains a Draft, so its new theorems are not available as published imports. The two published curtate survival results from Mission III can be used.

Formalisation and analytical scope

The four new definitions use a finite payment sum for each realised natural-valued lifetime. Each realised cashflow therefore has finite support, even when the possible lifetimes are unbounded. The milestones connect these finite realised sums with infinite survival-indicator series, prove the deferred and initial-payment decompositions, establish integrability under the geometric discount condition, and derive four infinite expected-value formulas.

The capstone combines these formulas and decompositions for the same probability measure, curtate lifetime, discount factor and deferral period. The measure need not arise from a particular mortality model.

The condition $0\le v<1$ applies to the expected present value claims. Pointwise present value identities hold for any real $v$ , since each realised natural-valued lifetime is finite and so produces only finitely many payments. At $v=1$ , an arbitrary lifetime distribution can have infinite expectation, so finite expected values cannot be assumed. The condition used here is sufficient; it is not claimed to be the sharpest possible condition under the source's financial discount assumptions.

Source and dependencies

The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3 §3.3.1 equations (3.11)–(3.12) and §3.3.3 equations (3.17)–(3.18). The temporary prefixes are the payment schedules from §3.3.2 equations (3.15)–(3.16), and the general expectation-of-cashflows step is equation (3.3).

This mission covers whole-life and deferred annuities. Guaranteed-period benefits, flat-interest assurance–annuity equivalence and continuous-time intensity-based valuations are separate later projects.

22 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics IV: Temporary Life Annuities and Their MomentsTextbook

Motivation

A life annuity pays a series of amounts while its recipient survives. A term assurance pays at most once during the policy term, whereas a temporary life annuity may pay several times. The indicators for its payments can therefore overlap, so a correct second-moment calculation must retain the dependence between them.

This mission formalises temporary life annuities payable in advance and in arrears, using the finite contingent-cashflow framework established in Actuarial Mathematics I. It reuses the curtate survival-event definition from Actuarial Mathematics III.

Survival events and dependence

Let $(\Omega,\mathcal F,P)$ be a probability space, and let $K:\Omega\to\mathbb N$ be the measurable curtate future lifetime, counting completed years. The event that the life survives to time $k$ is

S_k=\{\omega:K(\omega)\ge k\}.

These events are nested. For all $i,j\in\mathbb N$ ,

S_i\cap S_j=S_{\max(i,j)}.

Consequently their indicators satisfy

\mathbf1_{S_i}(\omega)\mathbf1_{S_j}(\omega)=\mathbf1_{S_{\max(i,j)}}(\omega).

This matters for second moments: survival to one payment date and survival to another are not mutually exclusive. Their intersection is survival to the later date. No independence assumption is made.

Temporary life annuity payable in advance

A unit temporary life annuity payable in advance makes up to $n$ payments, at times $k=0,\dots,n-1$ . The payment at time $k$ is made if $K\ge k$ . With deterministic annual discount factor $v$ , its random present value is

Z_{\mathrm{due}}=\sum_{k=0}^{n-1}v^k\mathbf1_{S_k}.

The expected present value is

\mathbb E_P[Z_{\mathrm{due}}]=\sum_{k=0}^{n-1}v^kP(S_k).

These are the temporary-annuity-in-advance identities in Chapter 3, equation (3.15). The first payment, at time zero, is certain whenever $n\ge1$ .

Temporary life annuity payable in arrears

A unit temporary life annuity payable in arrears has potential payments at times $k+1$ , for $k=0,\dots,n-1$ . A payment is made only if $K\ge k+1$ :

Z_{\mathrm{immediate}}=\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{S_{k+1}}.

Its expected present value is

\mathbb E_P[Z_{\mathrm{immediate}}]=\sum_{k=0}^{n-1}v^{k+1}P(S_{k+1}).

These are the corresponding payment-in-arrears identities in equation (3.16). In particular, a life with $K=0$ can receive the first payment of the annuity in advance, but no payment from the annuity in arrears.

Second moments and variance

The general moment calculations in Section 3.1.1 apply to the payment schedules in equations (3.15) and (3.16). Intersections of survival events reduce to the requirement to survive to the later date.

For payments in advance, the finite double-sum second moment is

\mathbb E_P[Z_{\mathrm{due}}^2]= \sum_{i=0}^{n-1}\sum_{j=0}^{n-1}v^{i+j}P(S_{\max(i,j)}).

For payments in arrears, it is

\mathbb E_P[Z_{\mathrm{immediate}}^2]= \sum_{i=0}^{n-1}\sum_{j=0}^{n-1} v^{i+j+2}P(S_{\max(i+1,j+1)}).

These are ordered double sums. Every ordered pair of payment dates contributes, including the diagonal terms and both orders of each off-diagonal pair. The corresponding variances are

\operatorname{Var}_P(Z_{\mathrm{due}})= \mathbb E_P[Z_{\mathrm{due}}^2]-\bigl(\mathbb E_P[Z_{\mathrm{due}}]\bigr)^2,

\operatorname{Var}_P(Z_{\mathrm{immediate}})= \mathbb E_P[Z_{\mathrm{immediate}}^2]-\bigl(\mathbb E_P[Z_{\mathrm{immediate}}]\bigr)^2.

The double-sum second-moment results are formal specialisations of the general moment equations (3.5)–(3.6). They are not additional numbered results in Section 3.3.2, which gives the expectation and present-value identities in equations (3.15) and (3.16).

Formalisation goal

The main theorem packages the expected values, second moments and variances of both annuities under the same $P$ , $K$ , $v$ and $n$ . Its supporting milestones establish the nesting of survival events and the products of their indicators, the finite payment schedules, and the successive valuation identities.

Both definitions are instances of the generic finite present-value construction from Actuarial Mathematics I. The curtate survival event is imported from Actuarial Mathematics III. Together, these provide reusable foundations for later missions on deferred and guaranteed life annuities.

The finite sums cover $n=0$ , when both annuities have zero present value, and $n=1$ , when the advance annuity includes the certain payment at time zero and the arrears annuity pays only if the life has completed at least one year. Algebraically, the identities allow any real $v$ . In actuarial applications, $v$ is normally positive. This mission asserts neither convergence of an infinite whole-life annuity nor statistical independence of survival payments.

Source references

The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Open Actuarial Textbooks Project, Chapter 3 §3.1.1 equations (3.5)–(3.6) and §3.3.2 equations (3.15)–(3.16).

This is a draft mission and has not yet been published. It formalises finite-term annual payments. Continuous payment timing, deferred whole-life payments, guaranteed-period annuities and infinite valuation are planned separately.

21 thms1 active userReviewed

Completed

Actuarial Science·Captain: WillR

Actuarial Mathematics III: Pure Endowment and Endowment AssuranceTextbook

Motivation

An endowment assurance pays a fixed benefit either when the policyholder dies during the policy term or when the policy reaches its maturity date. It therefore brings death-contingent and survival-contingent payments together in one valuation framework.

Actuarial Mathematics I established general identities for valuing finite contingent cashflows. Mission II formalised unit term assurance and the mutually exclusive events of death in different policy years. This mission extends those foundations to pure endowments and endowment assurances, covering payment dates, expected present values, second moments and variances.

Exact lifetime and curtate lifetime

Let $(\Omega,\mathcal F,P)$ be a probability space. The exact future lifetime $T$ takes nonnegative real values, while the curtate future lifetime $K$ records completed years. Their relationship is

K(\omega)\le T(\omega)<K(\omega)+1.

For a term $n\in\mathbb N$ , the textbook's pure-endowment payment in equation (3.9) depends on strict survival:

E_n^{>}=\{\omega:T(\omega)>n\}.

The endowment-assurance formula in equation (3.10), by contrast, uses a maturity payment when $K+1>n$ , equivalently when $K\ge n$ . Define

E_n^{\ge}=\{\omega:K(\omega)\ge n\}.

These events differ if death occurs exactly at time $n$ . Given the relationship between exact and curtate lifetime,

E_n^{\ge}=E_n^{>}\cup\{\omega:T(\omega)=n\}.

Thus equation (3.9) uses exact lifetime and excludes death at $T=n$ , whereas equation (3.10) uses curtate lifetime and includes it, since then $K=\lfloor T\rfloor=n$ . This endpoint identity clarifies the textbook's conventions; it is not itself a numbered textbook result. No assumption is made that death at a policy anniversary has probability zero.

Pure-endowment benefit

Under the strict exact-lifetime convention, a unit pure endowment payable at time $n$ has random present value

Z_{\mathrm{pure}}=v^n\mathbf1_{\{T>n\}}.

Equation (3.9) gives its expected value and variance:

\mathbb E_P[Z_{\mathrm{pure}}]=v^nP(T>n),

\operatorname{Var}_P(Z_{\mathrm{pure}}) =v^{2n}P(T>n)\bigl(1-P(T>n)\bigr).

Here $v$ is a deterministic annual discount factor. The Lean algebra permits any real $v$ , including the conventional case of a positive discount factor.

Endowment-assurance benefit

The endowment assurance pays a unit benefit at the end of the policy year of death if death occurs within the first $n$ years. Otherwise, it pays at time $n$ . As in equation (3.10), its present value is defined by

Z_{\mathrm{endow}}(\omega)=v^{\min(K(\omega)+1,n)}.

The theorem expresses this value as the sum of the unit term assurance from Mission II and the curtate maturity payment:

Z_{\mathrm{endow}} =\sum_{k=0}^{n-1}v^{k+1}\mathbf1_{\{K=k\}} +v^n\mathbf1_{\{K\ge n\}}.

The death benefit and maturity benefit are mutually exclusive. This gives the expected value and second moment:

\mathbb E_P[Z_{\mathrm{endow}}] =\sum_{k=0}^{n-1}v^{k+1}P(K=k)+v^nP(K\ge n),

\mathbb E_P[Z_{\mathrm{endow}}^2] =\sum_{k=0}^{n-1}v^{2(k+1)}P(K=k)+v^{2n}P(K\ge n).

The variance is then

\operatorname{Var}_P(Z_{\mathrm{endow}}) =\mathbb E_P[Z_{\mathrm{endow}}^2] -\bigl(\mathbb E_P[Z_{\mathrm{endow}}]\bigr)^2.

Formalisation goals and milestones

The formalisation proves measurability of the strict and curtate survival events, the exact boundary-event bridge, disjointness of death during the term from survival to maturity, and the pure-endowment expectation and variance. It also proves the endowment decomposition, expectation, second moment and variance. The formal capstone brings these results together under one probability measure, using the same exact and curtate lifetimes, term and discount factor. It states the boundary bridge explicitly and includes the pure-endowment mean and variance, along with the endowment present value, mean, second moment and variance.

The formalisation reuses Mission II's definition of term-assurance present value rather than reconstructing it. The main namespace remains ActuarialValuation, so later life-annuity missions can use the survival-event lemmas.

The edge cases require care. When $n=0$ , the endowment assurance pays immediately. The strict pure endowment, however, still depends on whether $T>0$ . Death at exactly $T=n$ is represented separately and is never excluded by an unstated continuity assumption. The finite real-valued Lean identities permit negative or zero discount factors as a mathematical generalisation, although ordinary actuarial applications use positive discount factors.

Source and scope

The primary source is the Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3, Chapter 3 §3.2.3 equation (3.9) and §3.2.4 equation (3.10).

Mission II, Actuarial Mathematics II: Term Assurance Present Values and Moments, is under moderator review at drafting time. Its relevant published definitions and theorem IDs are referenced directly.

This mission formalises unit benefits over a finite term with deterministic annual discounting. It establishes a finite-horizon result, not an infinite-horizon theorem. It does not cover immediate death benefits, arbitrary benefit scales, lifetime-dependent interest, infinite whole-life present values or the full continuous-time theory of mortality.

28 thms1 active userReviewed

Statistics Stochastic Systems·Captain: mikedeng1

Limit Theorems for Nearly Unstable Hawkes Processes 1: When T(1 − a_T) → ∞ the Rescaled Hawkes Process Is Asymptotically Deterministic in L²Research Paper

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.

10 thms1 active userReviewed

Machine Learning Statistics·Captain: mikedeng1

Learning without Concentration: Least-Squares ERM in a Convex Class Is Within 2 max{α_N(γ, δ/4), βN(τQ{F−F}(2τ)/16)} of f* in L₂ under a Small-Ball ConditionResearch Paper

Motivation

Least-squares regression over a class of functions is the basic problem of statistical learning theory: given an i.i.d. sample $(X_i,Y_i)_{i=1}^N$ from an unknown joint law, select a function in a class $F$ whose prediction error $\mathbb E(f(X)-Y)^2$ is close to the best possible in $F$ . The standard analysis of empirical risk minimization (ERM) compares empirical means with true means uniformly over the class, which requires the class and the target to concentrate: bounded functions, or sub-Gaussian tails. Heavy-tailed classes and targets, which arise as soon as the data are not bounded, fall outside that analysis.

S. Mendelson, Learning without Concentration (arXiv:1401.0304, J. ACM 62(3), 2015), showed that concentration is not needed for the lower half of the argument. The only property used for the quadratic part of the loss is a small-ball condition: functions in $F-F$ are not too concentrated near zero. Under that condition, ERM over a closed convex class attains an error governed by two localized complexity parameters, one intrinsic to the class and one measuring its interaction with the noise. The same lower-bound mechanism appears, for random matrices, in Koltchinskii–Mendelson (arXiv:1312.3580); the localized complexity parameters follow Lecué–Mendelson (arXiv:1305.4825).

Setting

Let $(\Omega,\mu)$ be a probability space and let $(X,Y)$ have joint law $\nu$ on $\Omega\times\mathbb R$ , with $X\sim\mu$ and $\mathbb EY^2<\infty$ . Let $F\subset L_2(\mu)$ be a closed, convex class of real functions on $\Omega$ , and let $f^*\in F$ minimize $\mathbb E(f(X)-Y)^2$ over $F$ . The noise is $\xi=f^*(X)-Y$ . Given an i.i.d. sample $(X_i,Y_i)_{i=1}^N$ from $\nu$ , an empirical minimizer $\hat f$ minimizes $\frac1N\sum_{i=1}^N(f(X_i)-Y_i)^2$ over $F$ . Let $(\varepsilon_i)_{i=1}^N$ be independent random signs, independent of the sample, and write $F\cap rD_{f^*}=\{f\in F:\|f-f^*\|_{L_2}\le r\}$ .

The small-ball function of a class $H$ is $Q_H(u)=\inf_{h\in H}\Pr(|h(X)|\ge u\|h\|_{L_2})$ ; it is applied to $F-F=\{f-h:f,h\in F\}$ .
The intrinsic parameter (Definition 2.1) is

\beta^*_N(\gamma)=\inf\Bigl\{r>0:\mathbb E\sup_{f\in F\cap rD_{f^*}}\Bigl|\tfrac1{\sqrt N}\textstyle\sum_{i}\varepsilon_i(f-f^*)(X_i)\Bigr|\le\gamma\sqrt N r\Bigr\}.

The multiplier process (2.2) is $\phi_N(s)=\sup_{f\in F\cap sD_{f^*}}\bigl|\tfrac1{\sqrt N}\sum_i\varepsilon_i\xi_i(f-f^*)(X_i)\bigr|$ with $\xi_i=f^*(X_i)-Y_i$ , and the noise parameter is

\alpha^*_N(\gamma,\delta)=\inf\bigl\{s>0:\Pr(\phi_N(s)\le\gamma s^2\sqrt N)\ge1-\delta\bigr\}.

For the proof (§5), $\beta_N(H,\gamma)=\inf\{r>0:\mathbb E\sup_{h\in H\cap rD}|\frac1N\sum_i\varepsilon_ih(X_i)|\le\gamma r\}$ , with $D$ the unit ball of $L_2(\mu)$ , and $H$ is star-shaped around 0 if $\lambda h\in H$ for all $h\in H$ , $0<\lambda\le1$ .

Formalization targets

Goal: Theorem 3.1

Fix $\tau>0$ with $Q_{F-F}(2\tau)>0$ and $\gamma<\tau^2Q_{F-F}(2\tau)/16$ . For every $0<\delta<1$ , with probability at least $1-\delta-\exp(-NQ^2_{F-F}(2\tau)/2)$ , every empirical minimizer satisfies

\|\hat f-f^*\|_{L_2}\le2\max\Bigl\{\alpha^*_N(\gamma,\delta/4),\ \beta^*_N\Bigl(\frac{\tau Q_{F-F}(2\tau)}{16}\Bigr)\Bigr\}.

The joint law, the class and the target are arbitrary subject to the hypotheses above; no boundedness, moment or tail condition beyond $L_2$ is imposed.

Milestones

In attack order:

Localization for a star-shaped class (§5, p. 20): $r>\beta_N(H,\gamma)$ implies $\mathbb E\sup_{h\in H\cap rD}|\frac1N\sum_i\varepsilon_ih(X_i)|\le\gamma r$ .
$\beta^*_N(\gamma)=\beta_N(F-f^*,\gamma)$ (§5, p. 20).
Theorem 5.4 (p. 21), the uniform empirical small-ball estimate: for $H$ in the unit sphere of $L_2(\mu)$ , if $\mathbb E\sup_{h\in H}|\frac1N\sum_i\varepsilon_ih(X_i)|\le\tau Q_H(2\tau)/16$ , then with probability at least $1-2\exp(-NQ_H^2(2\tau)/2)$ , $\inf_{h\in H}|\{i:|h(X_i)|\ge\tau\}|\ge NQ_H(2\tau)/4$ .
Corollary 5.5 (p. 22): the same estimate, $|\{i:|h(X_i)|\ge\tau\|h\|_{L_2}\}|\ge NQ_H(2\tau)/4$ , for every $h$ of a star-shaped class with $\|h\|_{L_2}\ge r>\beta_N(H,\tau Q_H(2\tau)/16)$ .
$F-f^*$ is star-shaped when $F$ is convex (proof of Theorem 5.3, p. 23).
Theorem 5.3 (p. 21): estimate (5.1) for $H=F-f^*$ .
The projection inequality $\mathbb E\xi(f-f^*)(X)\ge0$ for $f\in F$ (§5, p. 23).
Display (5.3) (p. 23): with probability at least $1-2\exp(-NQ^2_{F-F}(2\tau)/2)$ ,

\frac1N\sum_{i=1}^N(f-f^*)^2(X_i)\ge\frac{\tau^2}4Q_{F-F}(2\tau)\|f-f^*\|^2_{L_2}

for all $f\in F$ with $\|f-f^*\|_{L_2}\ge r$ . 9. Display (5.5) (p. 24): a bound $4\gamma\alpha^2$ on $|P_N\xi(f-f^*)-\mathbb E\xi(f-f^*)|$ on the sphere $\|f-f^*\|_{L_2}=\alpha$ extends to $4\gamma\|f-f^*\|^2_{L_2}$ outside it (deterministic).

Significance

Theorem 3.1 separates the error of ERM into a "low-noise" term $\beta^*_N$ , which depends on the class only and matches the realizable rate, and a "high-noise" term $\alpha^*_N$ , which depends on how the class correlates with the actual noise. Both are computable for heavy-tailed classes: the paper derives from it sharp rates for linear regression with heavy-tailed design and for the persistence problem in $\ell_1^n$ (§4). The small-ball lower bound (Theorem 5.4 and (5.3)) is reusable on its own: it gives lower isometry estimates for random matrices with heavy-tailed rows (the setting of Koltchinskii–Mendelson).

The result is proved in the paper. As far as is known, none of it has been machine-checked: there is no formal statement of Theorem 3.1, of the small-ball estimate, or of the localized parameters $\alpha^*_N,\beta^*_N$ in Lean. The mission produces the first formal statements of these objects, and a formal proof would also check the constants of the printed argument.

Difficulty

The obvious approach, a uniform law of large numbers for the squared loss over $F$ , fails: without concentration, $\frac1N\sum_i(f-f^*)^2(X_i)$ need not be close to $\|f-f^*\|^2_{L_2}$ uniformly, and an upper estimate is unavailable. The proof needs only a one-sided lower estimate, and the difficulty is to obtain it uniformly over an infinite, unbounded class from the small-ball condition alone, with a probability that is exponential in $N$ . A second difficulty is the multiplier term $\frac1N\sum_i\xi_i(f-f^*)(X_i)$ , where the noise $\xi$ may be heavy-tailed and dependent on $X$ ; it must be controlled through the random-sign process defining $\alpha^*_N$ , not through a bound on $\xi$ . The standard tools involved (bounded differences, symmetrization, contraction for Bernoulli processes) are not in Mathlib.

Formalization scope

All objects live in one definitions file, LearnNoConc.ERM.Setting. The conventions are:

The data are a joint law ν on Ω × ℝ; the law of $X$ is ν.map Prod.fst. The sample is a point of Fin N → Ω × ℝ under Measure.pi; $N\ge1$ is assumed.
$\|\cdot\|_{L_2}$ is eLpNorm · 2 μ, valued in $[0,\infty]$ . The expectation over random signs is the average over all $2^N$ sign vectors.
Suprema and expectations of suprema are taken in $[0,\infty]$ (⨆, ‖·‖ₑ, lower Lebesgue integral), and $\alpha^*_N,\beta^*_N,\beta_N$ are $[0,\infty]$ -valued infima, so an empty set of admissible radii gives $+\infty$ and a vacuous bound, as on the page. Defining inequalities are compared in the extended reals.
"With probability at least $1-p$ , $A$ " is stated as "the outer probability of the complement of $A$ is at most $p$ ".
The goal quantifies over every empirical minimizer, and $f^*$ is any minimizer of the risk over $F$ .
Added, disclosed hypotheses: $\mathbb EY^2<\infty$ ; every $f\in F$ measurable; and pointwise separability of $F$ (a countable subclass approximating every element pointwise and in $L_2$ ), which stands in for the measurability of suprema the paper takes for granted. Without it the lower integral of a non-measurable supremum would make $\beta^*_N$ smaller and the goal stronger than the paper.

A formalization in which an infimum over an empty set is $0$ , a supremum or an integral of a non-integrable function is truncated to $0$ , $f^*$ is an arbitrary element of $F$ , or $\hat f$ is one chosen minimizer would trivialize or change the statement; all of these are ruled out above.

A complete development needs McDiarmid's bounded differences inequality, Giné–Zinn symmetrization (in expectation and in probability), the Ledoux–Talagrand contraction inequality for Bernoulli processes, and the measurability theory of suprema over separable classes. These are reusable well beyond this mission, and contributions of any of them are welcome, as are proofs of the milestones independently of the goal.

Selected references

S. Mendelson, Learning without Concentration, J. ACM 62(3), Article 21, 2015. Preprint arXiv:1401.0304v2 (the version cited here). https://arxiv.org/abs/1401.0304, https://doi.org/10.1145/2699439
V. Koltchinskii, S. Mendelson, Bounding the smallest singular value of a random matrix without concentration, preprint, 2013. https://arxiv.org/abs/1312.3580
G. Lecué, S. Mendelson, Learning subgaussian classes: Upper and minimax bounds, preprint, 2013. https://arxiv.org/abs/1305.4825
A. W. van der Vaart, J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996, §2.3.3 (pointwise separable classes). https://doi.org/10.1007/978-1-4757-2545-2

11 thms1 active userReviewed

Analysis Stochastic Systems·Captain: mikedeng1

Affine Volterra Processes 3: Global Solutions with Nonpositive Real Part of the Square-Root Riccati–Volterra EquationResearch Paper

Motivation

The Volterra square-root model describes a nonnegative, time-dependent state whose present value depends on a weighted history. Ordinary square-root diffusions use a constant kernel and have a Markov state; replacing that kernel by a function of elapsed time allows persistent or singular memory. This matters for the transform formulas used to characterize distributions of such processes. Those formulas depend on a deterministic nonlinear integral equation, and require a solution that exists at every finite time. Abi Jaber, Larsson and Pulido isolate that requirement in Lemma 6.3 of Affine Volterra processes, arXiv:1708.08796v3 (2019).

The paper's Section 6 treats processes in the nonnegative orthant and its Section 7 specializes the framework to a Volterra Heston model. The present mission concerns the deterministic equation behind the Section 6 transform. The stochastic existence theorem and the transform identity are separate results in the same paper. Keeping this mission on the integral equation makes its analytic content usable independently of a chosen probability space.

Setting

Fix a finite coordinate set of size $d$ . A diagonal kernel consists of real functions $K_i(t)$ for $t\ge0$ , with the $i$ -th entry of the matrix kernel equal to $K_i$ and all off-diagonal entries zero. A resolvent of the first kind for $K_i$ is a nonnegative measure $L_i$ for which the convolution $K_i*L_i$ equals one at positive times. The relevant regularity condition, labeled (2.5), requires local square integrability and positive-time translation bounds of order $h^{\gamma_i}$ for some $\gamma_i\in(0,2]$ . Condition (3.4) requires a kernel to be nonnegative, nonzero, nonincreasing and continuous at positive times. It also requires its resolvent measure to have decreasing interval masses $L_i([s,s+t])$ as $s$ increases. Each shifted function $\Delta_hK_i(t)=K_i(t+h)$ must satisfy (3.4) for $0\le h\le1$ , with its own resolvent. These are the assumptions of Theorem 6.1 and hence of its Lemma 6.3 (pp. 6, 14, 28–29).

Let $u=(u_i)$ be a complex row vector and let $f(t)=(f_i(t))$ be a locally integrable complex row function. Let $B$ be a real matrix whose off-diagonal entries are nonnegative, and let $\sigma_i>0$ . The $i$ -th square-root Riccati–Volterra equation is

\psi_i(t)=u_iK_i(t)+\int_0^t K_i(t-s)\left(f_i(s)+\sum_j\psi_j(s)B_{ji}+\frac{\sigma_i^2}{2}\psi_i(s)^2\right)\,ds.

The index $B_{ji}$ selects column $i$ : in the paper's notation $B=(b^1\;\cdots\;b^d)$ and the coupling is $\psi(s)b^i$ . The kernel acts only on the $i$ -th equation, while $B$ couples the coordinates. The coefficient $b^0$ from the stochastic process does not enter this equation (equation (6.3), p. 27).

Formalization targets

The goal is the global existence, uniqueness and sign statement of Lemma 6.3. If $\operatorname{Re}u_i\le0$ and $\operatorname{Re}f_i\le0$ , then

\exists!\,\psi\in L^2_{\mathrm{loc}}(\mathbb R_+,\mathbb C^d) \quad\text{solving (6.3) globally, with}\quad \operatorname{Re}\psi_i\le0\quad\text{for every }i.

For functions defined only up to null sets, the equation, uniqueness and sign conclusion are understood almost everywhere. The goal has no fixed time horizon and no hard-coded kernel: it covers every diagonal kernel satisfying the paper's conditions. The five milestones record the source's analytic support: the shifted resolvent bounds (3.9)–(3.10), the $L^2$ stability lemma C.1, maximal-solution Theorem B.1, global-solution Corollary B.3 and nonnegative-orthant invariance Theorem C.2. Their statements and locations are recorded in the milestone list.

Significance

Global solvability makes the square-root transform equation meaningful at any finite horizon. Uniqueness fixes the transform parameter determined by a kernel and forcing function. The nonpositive real part is the sign property needed in the paper's subsequent exponential-affine transform argument for nonnegative states (Theorem 6.1(ii), pp. 28–29). Without a global solution, that argument would only address a time interval before a possible blow-up.

The result is proved in the cited paper; this mission asks for a machine-checked development of that known theorem and its supporting integral-equation results. Its reusable output includes an $L^2$ notion of Volterra solution, the first-kind resolvent hypotheses, maximal lifetime, stability under changes of forcing and kernel, and a comparison statement for diagonal systems. The goal and milestones are presently proof obligations, not claims of existing machine-checked proofs.

Difficulty

Local solvability alone does not control the quadratic term $\psi_i^2$ for arbitrarily large time. In particular, a generic local fixed-point theorem can yield a maximal solution whose $L^2$ norm diverges at a finite horizon. Sign information for the real part is also coupled to the imaginary part through that quadratic term; checking each coordinate independently does not establish invariance of the nonpositive half-plane. The analysis has to preserve the kernel's first-kind resolvent conditions and the off-diagonal sign pattern of $B$ across the coupled system. Singular kernels allowed by (2.5) prevent replacing the problem with a standard ordinary differential equation.

Formalization scope

Time is represented by real numbers and every local $L^p$ condition is restricted to positive bounded intervals. Vectors are functions on Fin d; matrix $L^p$ membership is componentwise. These finite-dimensional norms are equivalent to the Euclidean and operator norms used in the paper. The kernel regularity estimates are Big-O statements as $h$ tends to zero through positive values. A first-kind resolvent is a nonnegative measure supported on nonnegative times, with the convolution identity and interval-mass monotonicity stated directly. The convolution at positive time is an interval integral; the bound at zero in (3.10) uses the integral on $[0,0]$ , while the source describes a right-continuous extension when available.

Solutions are locally square integrable and satisfy their equations almost everywhere. The integrability of each asserted convolution is part of the solution predicate, so the default zero value of a nonintegrable Lean integral cannot create a spurious solution. A maximal lifetime is extended-nonnegative-real valued, allowing infinity, and a finite lifetime requires an infinite extended $L^2$ norm. Sign conditions on locally integrable forcing and on the solution are almost everywhere. Measurable time dependence of the nonlinear drift is made explicit for Theorem B.1 and Corollary B.3, where it is necessary to interpret their integrals. The condition $b^0\ge0$ of the square-root process is omitted from the goal because $b^0$ is absent from (6.3).

The development needs Mathlib's Bochner integrals, local $L^p$ predicates, measures, complex arithmetic and asymptotic filters. Proof contributions to the five source milestones and the goal are welcome, including infrastructure for nonconvolution Volterra resolvents where the paper cites earlier literature. The formalization must keep the coefficient $\sigma_i^2/2$ , the column index $B_{ji}$ , and every shift $h\in[0,1]$ .

Selected references

E. Abi Jaber, M. Larsson and S. Pulido, Affine Volterra processes, arXiv:1708.08796v3, 2019. Preprint.
G. Gripenberg, S.-O. Londen and O. Staffans, Volterra Integral and Functional Equations, Cambridge University Press, 1990. DOI.

8 thms1 active userReviewed

Functional Analysis Machine Learning Statistics·Captain: mikedeng1

Generalization Properties of Learning with Random Features: Ridge Regression with c₀√n·log(108κ²√n/δ) Random Features Has Excess Risk at Most c₁·log²(18/δ)/√n with Probability 1 − δResearch Paper

Motivation

Kernel ridge regression is a standard nonparametric estimator with optimal statistical guarantees, but it needs the $n\times n$ kernel matrix of the data: roughly $O(n^3)$ time and $O(n^2)$ memory. Random features (Rahimi and Recht, NeurIPS 2007) replace the kernel by an average over $M$ randomly sampled feature functions, turning the problem into ridge regression in dimension $M$ , at cost $O(nM^2)$ time and $O(nM)$ memory. The question is how many features are needed before the statistical accuracy of the exact kernel method is lost.

The first statistical analysis of a random-features estimator (Rahimi and Recht, NeurIPS 2009), for Lipschitz losses over a ball of fixed radius, needs $O(n)$ features to reach an $O(1/\sqrt n)$ bound. Rudi and Rosasco (arXiv:1602.04474, NeurIPS 2017) showed that $M$ of order $\sqrt n\log n$ features already give the $O(1/\sqrt n)$ excess risk that exact kernel ridge regression attains with regularization $\lambda=n^{-1/2}$ (Caponnetto and De Vito 2007), assuming only that the best predictor in the reproducing kernel Hilbert space exists.

Setting

Let $X$ be a separable input space and $(\Omega,\pi)$ a probability space. A random feature is a function $\psi:X\times\Omega\to\mathbb R$ , continuous in both variables with $|\psi(x,\omega)|\le\kappa$ for some $\kappa\ge1$ . It defines the kernel

K(x,x')=\int_\Omega\psi(x,\omega)\psi(x',\omega)\,d\pi(\omega),

whose reproducing kernel Hilbert space is $\mathcal H$ . Data $(x_1,y_1),\dots,(x_n,y_n)$ are drawn i.i.d. from a probability $\rho$ on $X\times\mathbb R$ with $|y|\le b$ almost surely, $b>0$ . The expected risk is $\mathcal E(f)=\int(f(x)-y)^2\,d\rho(x,y)$ , and $f_{\mathcal H}\in\mathcal H$ is a minimizer of $\mathcal E$ over $\mathcal H$ , assumed to exist.

Given features $\omega_1,\dots,\omega_M$ drawn i.i.d. from $\pi$ , independently of the data, the feature map is $\phi_M(x)=M^{-1/2}(\psi(x,\omega_1),\dots,\psi(x,\omega_M))$ . With $\widehat C_M=\frac1n\sum_i\phi_M(x_i)\phi_M(x_i)^\top$ and $\widehat S_M^\top\widehat y=\frac1n\sum_iy_i\phi_M(x_i)$ , the random-features ridge estimator with parameter $\lambda>0$ is

\widehat f_{\lambda,M}(x)=\phi_M(x)^\top\widehat w_{\lambda,M},\qquad\widehat w_{\lambda,M}=(\widehat C_M+\lambda I)^{-1}\widehat S_M^\top\widehat y .

In the Lean development these are kernelOf, featureMap, empCov, empCross, rfWeights, rfEstimator and risk in the namespace RFRidge.Basic.

Formalization targets

Goal: Theorem 1

There are constants $c_0,c_1>0$ , independent of $n$ , $\lambda$ and $\delta$ , and a threshold $n_0$ such that for every $\delta\in(0,1]$ and $n\ge n_0$ , with $\lambda_n=n^{-1/2}$ and

M_n=c_0\sqrt n\,\log\frac{108\kappa^2\sqrt n}{\delta}

features, with probability at least $1-\delta$ over the data and the features,

\mathcal E(\widehat f_{\lambda_n,M_n})-\mathcal E(f_{\mathcal H})\le\frac{c_1\log^2\frac{18}{\delta}}{\sqrt n}.

The constants are existential: the paper prints them without values, and the values in its appendix are not established by the printed proof. The goal therefore asserts the shape of the bound, which survives any later improvement of the constants.

Milestones

The proof goes through an analytic decomposition of the excess risk on $L^2(X,\rho_X)$ followed by concentration. The milestones are the results of that proof that are stated as printed:

Lemma 1: the integral operator $L$ of $K$ equals $\int\psi_\omega\otimes\psi_\omega\,d\pi(\omega)$ .
Lemma 2: the component of the regression function orthogonal to the range of $L$ is invisible to every random-features predictor, almost surely.
Proposition 4 (Cordes), Proposition 9 (interpolation $\|XA^\sigma\|\le\|X\|^{1-\sigma}\|XA\|^\sigma$ ) and Proposition 8 (a multiplicative bound between regularized operators).
Lemma 5: the bound on the approximation error under the source condition $Pf_\rho=L^rg$ . Lemmas 3 and 4 remain draft items, but are omitted from the milestone list because the PDF text layer corrupts their displayed equations and the mechanical verbatim checker rejects the exact visual transcription.
Propositions 1 and 2: Bernstein inequalities for real random variables and for random vectors in a Hilbert space.

Significance

Theorem 1 shows that, in the basic setting, random features reduce the cost of kernel ridge regression from $O(n^3)$ time and $O(n^2)$ memory to $O(n^2)$ and $O(n\sqrt n)$ without losing the minimax-optimal $O(1/\sqrt n)$ rate. It is the reference result on the statistical cost of random-features approximations, and the same decomposition yields the paper's faster rates under source and capacity conditions (Theorems 2 and 3) and the analysis of data-dependent feature sampling.

To the best of the mission's knowledge, none of these results has a machine-checked proof. Formalizing them requires real infrastructure: integral operators on $L^2$ defined by a kernel with an integral representation, operator inequalities for the continuous functional calculus, and Bernstein inequalities in Hilbert spaces. The Bernstein inequalities and the operator inequalities (Cordes, interpolation, Proposition 8) are reusable well beyond this paper.

Difficulty

The obvious argument controls $\sup_{x,x'}|K_M(x,x')-K(x,x')|$ uniformly and transfers it to the estimator. It needs $M$ of order $n$ to keep the $O(1/\sqrt n)$ rate, because a uniform kernel approximation ignores that the estimator only probes $K$ through a regularized operator. Getting $\sqrt n\log n$ features requires comparing the integral operators $L$ and $L_M$ relative to $L+\lambda I$ , in the operator norm weighted by $(L+\lambda I)^{-1/2}$ , and this needs fractional powers of operators, operator monotonicity and concentration of random operators. A second subtlety is that the regression function need not lie in the closure of $\mathcal H$ ; Lemma 2 shows that the orthogonal component does not affect any random-features estimator.

Formalization scope

All models are posed in Lean 4 with Mathlib. The input space is a separable topological space with its Borel σ-algebra, the feature space $\Omega$ is the type W, and $\psi$ is jointly continuous, jointly measurable for the product σ-algebra (an added hypothesis: without second countability it does not follow from continuity), and bounded by $\kappa\ge1$ everywhere. The RKHS is Mathlib's RKHS ℝ H X ℝ, tied to the kernel by RKHS.kernel H x x' 1 = K x x'. Samples and features are indexed from $0$ ; the $n$ samples and $M_n$ features have the product law $\rho^{\otimes n}\otimes\pi^{\otimes M_n}$ , and $M_n$ is rounded up. "With probability at least $1-\delta$ " is "the failure event has probability at most $\delta$ ", with $\delta\in(0,1]$ and $n\ge1$ .

Operators: the paper's Hilbert spaces are real, but Mathlib's continuous functional calculus for bounded operators, which defines $A^s$ and $(A+\lambda I)^{-1/2}$ , exists only on complex Hilbert spaces. The operator milestones are therefore posed on complex Hilbert spaces, and every inverse or power is the functional calculus of an explicit real function; the real statements follow by complexification. Lemmas 3–5 are stated for abstract positive operators satisfying exactly the relations their proofs use, and add $r\le1$ (the range of Assumption 6), without which Lemma 5 is false. Proposition 8 states $\beta<1$ as a conclusion. Lemma 3 corrects a sign in the exponent of $C_{M,\lambda}$ : its display prints $-1/2$ where its proof uses $+1/2$ ; the printed bound fails for scalar operators.

A trivializing formalization is ruled out: the goal mentions only the estimator, the risk and $f_{\mathcal H}$ , never the operators of the proof, and its constants $c_0,c_1$ are fixed before $\delta$ and $n$ , so they cannot absorb $\log^2(18/\delta)$ or $\sqrt n$ .

Not included: Theorem 4 (the analytic decomposition), Propositions 5 and 7 (which need Hilbert–Schmidt norms and traces), Lemmas 6–10 and Theorems 5–7 of Appendix A.3–A.4. Contributions of these intermediate results, of a Lean theory of integral operators of kernels, and of Hilbert-space concentration inequalities are welcome.

Selected references

A. Rudi, L. Rosasco, Generalization Properties of Learning with Random Features, NeurIPS 2017; arXiv:1602.04474v5. https://arxiv.org/abs/1602.04474
A. Rahimi, B. Recht, Random Features for Large-Scale Kernel Machines, NeurIPS 2007. https://papers.nips.cc/paper/3182-random-features-for-large-scale-kernel-machines
A. Caponnetto, E. De Vito, Optimal Rates for the Regularized Least-Squares Algorithm, Foundations of Computational Mathematics 7, 2007. https://doi.org/10.1007/s10208-006-0196-8
A. Rahimi, B. Recht, Weighted Sums of Random Kitchen Sinks: Replacing Minimization with Randomization in Learning, NeurIPS 2008 (proceedings 2009). https://papers.nips.cc/paper/3495-weighted-sums-of-random-kitchen-sinks-replacing-minimization-with-randomization-in-learning
H. O. Cordes, Spectral Theory of Linear Differential Operators and Comparison Algebras, Cambridge University Press, 1987. https://doi.org/10.1017/CBO9780511662836

11 thms1 active userReviewed

Machine Learning Optimization·Captain: mikedeng1

Stochastic Model-Based Minimization of Weakly Convex Functions 3: The Projected Stochastic Subgradient Method Is an Approximate Descent Method on the Moreau Envelope for Any StepsizesResearch Paper

Motivation

The projected stochastic subgradient method minimizes an expected loss $f(x) = \mathbb E_{\xi\sim P}[f(x,\xi)]$ over a closed convex set $X$ : it samples a data point, steps against a sampled subgradient, and projects back onto $X$ . For convex $f$ its sample complexity has been known for decades, and for smooth nonconvex $f$ the stochastic gradient method needs $O(\varepsilon^{-4})$ samples to reach gradient norm $\varepsilon$ (Ghadimi–Lan 2013). Many problems in statistical learning and signal processing are neither convex nor smooth — robust phase retrieval, nonlinear regression with an $\ell_1$ loss, covariance estimation, conditional value-at-risk with smooth losses — but are weakly convex: they become convex after adding a quadratic $\frac{\rho}{2}\|x\|^2$ .

Timeline. Nurminskii (1970s) showed that for weakly convex losses $f(\cdot,\xi)$ and no constraint the stochastic subgradient method subsequentially converges to a stationary point almost surely, without a rate. Ghadimi and Lan (2013) proved the $O(\varepsilon^{-4})$ rate for smooth $f$ . Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 2019) proved the first rate for the plain projected stochastic subgradient method on weakly convex problems, measured by the gradient of the Moreau envelope, and for any nonnegative stepsizes. This is Theorem 3.1 of their paper and the goal of this mission.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. Let $X \subseteq \mathbb R^d$ be nonempty, closed and convex, and let $f : \mathbb R^d \to \mathbb R$ be $\rho$ -weakly convex ( $\rho > 0$ ): $x \mapsto f(x) + \frac{\rho}{2}\|x\|^2$ is convex. The problem is

\min_{x \in X} f(x), \qquad \text{i.e. } \min_x \varphi(x),\ \varphi = f + \delta_X,

where $\delta_X$ is $0$ on $X$ and $+\infty$ off $X$ .

The subdifferential $\partial f(x)$ is the set of $v$ with $f(y) \ge f(x) + \langle v, y - x\rangle + o(\|y - x\|)$ as $y \to x$ . For $\lambda > 0$ the Moreau envelope and the proximal point of $\varphi$ are

\varphi_\lambda(x) = \min_{y \in X}\Big\{f(y) + \tfrac{1}{2\lambda}\|y - x\|^2\Big\}, \qquad \operatorname{prox}_{\lambda\varphi}(x) = \operatorname*{argmin}_{y \in X}\Big\{f(y) + \tfrac{1}{2\lambda}\|y - x\|^2\Big\}.

Assumption A (stochastic subgradient oracle): on a probability space $(\Omega, \mathcal F, P)$ one can draw i.i.d. samples $\xi_0, \xi_1, \dots \sim P$ (A1); there are an open set $U \supseteq X$ and a measurable map $G$ with $\mathbb E_\xi[G(x,\xi)] \in \partial f(x)$ for all $x \in U$ (A2); and $\mathbb E_\xi\|G(x,\xi)\|^2 \le L^2$ for all $x \in X$ (A3).

Algorithm 3.1 with $r = \delta_X$ starts at $x_0 \in X$ and, for $t = 0, \dots, T$ , samples $\xi_t$ and sets $x_{t+1} = \operatorname{proj}_X(x_t - \alpha_t G(x_t, \xi_t))$ with stepsizes $\alpha_t \ge 0$ . It returns $x_{t^*}$ with $t^*$ drawn from $\{0, \dots, T\}$ with probability $\alpha_t / \sum_i \alpha_i$ .

Formalization targets

Goal: Theorem 3.1, (3.4) and (3.5)

For every $\bar\rho > \rho$ and any stepsizes $\alpha_t \ge 0$ with $\sum_t \alpha_t > 0$ ,

\mathbb E\big[\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2\big] \le \frac{\bar\rho}{\bar\rho - \rho}\cdot\frac{\big(\varphi_{1/\bar\rho}(x_0) - \min\varphi\big) + \frac{\bar\rho L^2}{2}\sum_{t=0}^T\alpha_t^2}{\sum_{t=0}^T\alpha_t},

and with $\alpha_t = \gamma/\sqrt{T+1}$ , $\gamma > 0$ ,

\mathbb E\big[\|\nabla\varphi_{1/(2\rho)}(x_{t^*})\|^2\big] \le 2\cdot\frac{\big(\varphi_{1/(2\rho)}(x_0) - \min\varphi\big) + \rho L^2\gamma^2}{\gamma\sqrt{T+1}}.

Milestones

Lemma 2.1 (p. 10): for a closed proper $\varphi$ , weak convexity, the approximate secant inequality (2.4), the subgradient inequality (2.5) and hypomonotonicity of $\partial\varphi$ are equivalent.
§3.1, display after (3.8) (pp. 13–14; the display starts on p. 13 and ends on p. 14): for $x \in X$ and $\hat x = \operatorname{prox}_{\varphi/\bar\rho}(x)$ , $f(x) - f(\hat x) - \frac{\rho}{2}\|x - \hat x\|^2 \ge (\bar\rho - \rho)\|x - \hat x\|^2 = \frac{\bar\rho - \rho}{\bar\rho^2}\|\nabla\varphi_{1/\bar\rho}(x)\|^2$ .
Lemma 2.2 (p. 11): for $\lambda \in (0, \rho^{-1})$ the envelope $\varphi_\lambda$ is $C^1$ with $\nabla\varphi_\lambda(x) = \lambda^{-1}(x - \operatorname{prox}_{\lambda\varphi}(x))$ .
Theorem 3.1, (3.3) (p. 13): the one-step estimate

\mathbb E\big[\varphi_{1/\bar\rho}(x_{t+1})\big] \le \mathbb E\big[\varphi_{1/\bar\rho}(x_t)\big] - \frac{\alpha_t(\bar\rho - \rho)}{\bar\rho}\mathbb E\big[\|\nabla\varphi_{1/\bar\rho}(x_t)\|^2\big] + \frac{\alpha_t^2\bar\rho L^2}{2}.

Significance

The result. The gradient of the Moreau envelope is a near-stationarity measure: $\|\nabla\varphi_\lambda(x)\|$ small means that $x$ is within $\lambda\|\nabla\varphi_\lambda(x)\|$ of a point $\hat x \in X$ with $f(\hat x) \le f(x)$ and $\operatorname{dist}(0, \partial\varphi(\hat x)) \le \|\nabla\varphi_\lambda(x)\|$ . Theorem 3.1 therefore gives $O(\varepsilon^{-4})$ sample complexity for finding nearly stationary points of nonsmooth nonconvex constrained stochastic problems, matching the smooth case. Estimate (3.3) shows that the Moreau envelope is an approximate Lyapunov function for the method, and it holds for arbitrary nonnegative stepsizes; Theorem 3.4 of the same paper (the proximal extension) needs $\alpha_t \le 1/\bar\rho$ and a worse constant.

Formalizing it. The result is proved in the paper; no machine-checked version exists. A formalization requires the Fréchet subdifferential of extended-valued functions, the Moreau envelope and its smoothness under weak convexity (Lemma 2.2, which the paper cites as standard rather than proving), and a measure-theoretic treatment of the iterates of a stochastic algorithm on a product probability space. Lemma 2.1 and Lemma 2.2 are reused by the other missions of this series.

Difficulty

The obvious approach — show that $f(x_t)$ decreases in expectation — fails: without smoothness, a subgradient step can increase $f$ by an amount of order $\alpha_t$ , not $\alpha_t^2$ , and no stepsize repairs that. The argument instead tracks the Moreau envelope, which is smooth even though $f$ is not; the difficulty moves into (i) Lemma 2.2, the $C^1$ -smoothness of the envelope of a weakly convex function, which is a nontrivial piece of variational analysis, and (ii) the conditional-expectation bookkeeping that turns a one-sample estimate into (3.3) along the random iterates, including the integrability of $\varphi_{1/\bar\rho}(x_t)$ and $\|\nabla\varphi_{1/\bar\rho}(x_t)\|^2$ , which the paper does not discuss.

Formalization scope

Carrier and encoding. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). An extended-valued function is encoded by its domain and its real values on the domain; $\varphi = f + \delta_X$ is the pair $(X, f)$ , and $\varphi_\lambda$ is moreauEnv X f lam, a real infimum over $X$ . Lemma 2.2 supplies the attainment and differentiability under which this infimum is the paper's envelope.
The projection is a function proj constrained by the published nearest-point predicate SpectralProjGrad.Shared.IsProjOnto X proj. It is not the proximal-point predicate of $\alpha_t\delta_X$ , so that $\alpha_t = 0$ remains meaningful; zero stepsizes are allowed, as in Algorithm 3.1.
Randomness. $T+1$ i.i.d. samples are a point of $\Omega^{T+1}$ under the product measure; $\mathbb E[\cdot(x_{t^*})]$ is the $\alpha$ -weighted average of $\mathbb E[\cdot(x_t)]$ , exactly as the paper's proof identifies it. Every bounded expectation comes with an integrability conclusion, since a Bochner integral of a non-integrable function is $0$ .
Added hypotheses. $\rho > 0$ (implicit in $\varphi_{1/(2\rho)}$ and in $\lambda < \rho^{-1}$ of Lemma 2.2); $\sum_t\alpha_t > 0$ in (3.4) (needed for $t^*$ ); closedness and properness in Lemmas 2.1–2.2. $\min\varphi$ is any lower bound $\varphi^*$ of $f$ on $X$ . The $C^2$ clause of Lemma 2.1 is not stated.
Erratum. The rearranged display before "Notice that the left-hand-side is precisely …" (p. 14) has an extra factor $\bar\rho$ in its denominator; the statement (3.4), which the goal formalizes, is what the unfolded recursion gives.
Ruled out. A formalization with an unconstrained proj, a stochastic subgradient not tied to $\partial f$ by (A2), expectations without integrability, or $\min\varphi$ as a junk-valued infimum would be trivial or false; each is excluded by the statements' hypotheses and conclusions.
Not included. The complexity remarks (3.9)–(3.10) and the paragraph on improved complexity under convexity.

Proofs of any milestone are welcome; Lemma 2.2 and the product-measure bookkeeping for (3.3) are the reusable parts.

Selected references

D. Davis, D. Drusvyatskiy, Stochastic Model-Based Minimization of Weakly Convex Functions, SIAM J. Optim. 29(1), 2019; arXiv:1803.06523v3. https://arxiv.org/abs/1803.06523
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3

10 thms1 active userReviewed

Markov Chain Statistics·Captain: mikedeng1

Spectral Gaps for a Metropolis–Hastings Algorithm in Infinite Dimensions II: The pCN Algorithm Has a Wasserstein Spectral Gap Uniform in the Dimension When the Potential Is Locally LipschitzResearch Paper

Motivation

Bayesian inverse problems for functions — the initial condition of a PDE, a permeability field, a diffusion coefficient — lead to posterior measures $\mu$ on an infinite-dimensional Hilbert space $H$ , given by a density $\exp(-\Phi)$ with respect to a Gaussian prior $\gamma$ . In practice $\mu$ is sampled by Markov chain Monte Carlo on an $m$ -dimensional discretisation $\mu_m$ , and the question that matters is whether the sampler's convergence rate survives the limit $m\to\infty$ . For the standard random-walk Metropolis algorithm it does not (mission III of this series). The preconditioned Crank–Nicolson (pCN) algorithm, whose proposal preserves $\gamma$ , was introduced to avoid this (Beskos, Roberts, Stuart and Voss 2008; Cotter, Roberts, Stuart and White 2013).

Hairer, Stuart and Vollmer (2014) prove that pCN has a Wasserstein spectral gap that is uniform in the dimension. Mission I of this series covers their result for globally Lipschitz potentials $\Phi$ (Theorem 2.12). This mission covers Theorem 2.14, which needs only that $\Phi$ be locally Lipschitz, with a local Lipschitz constant growing slower than any exponential. That class contains potentials of polynomial growth, which arise for nonlinear forward maps.

Setting

$H$ is a separable real Hilbert space with a centred Gaussian measure $\gamma$ , and $(e_i)_{i\ge0}$ is an orthonormal basis of eigenvectors of the covariance of $\gamma$ . $P_mH$ is the span of $e_0,\dots,e_{m-1}$ , and $\gamma_m$ is the image of $\gamma$ under the orthogonal projection onto $P_mH$ . For a potential $\Phi:H\to\mathbb R$ the targets are

\mu(dx)\propto e^{-\Phi(x)}\gamma(dx),\qquad \mu_m(dx)\propto e^{-\Phi(x)}\gamma_m(dx).

Fix a step size $\delta\in(0,\tfrac12]$ and put $\rho=1-(1-2\delta)^{1/2}$ . One pCN step from $x$ draws $\xi\sim\gamma$ and proposes $p_x=(1-2\delta)^{1/2}x+\sqrt{2\delta}\,\xi$ . The proposal is accepted with probability $\alpha(x,p_x)=1\wedge\exp(\Phi(x)-\Phi(p_x))$ ; otherwise the chain stays at $x$ . Its transition kernel is $\mathcal P$ . The kernel $\mathcal P_m$ is the same algorithm on $P_mH$ with $\xi\sim\gamma_m$ .

Distances between probability measures are Wasserstein lifts of a cost $c$ : $c(\nu_1,\nu_2)=\inf_\pi\int c\,d\pi$ over couplings $\pi$ of $\nu_1,\nu_2$ . A kernel is $d$ -contracting if $d(x,y)<1$ implies $d(\mathcal P(x,\cdot),\mathcal P(y,\cdot))\le c\,d(x,y)$ for a fixed $c<1$ . A set $S$ is $d$ -small if $d(\mathcal P(x,\cdot),\mathcal P(y,\cdot))\le s<1$ for all $x,y\in S$ .

The distance of this mission is a weighted path length (3.6). For unit-speed $C^1$ paths $\psi:[0,T]\to H$ from $x$ to $y$ ,

\bar d(x,y)=\inf_{T,\psi}\frac1\varepsilon\int_0^T e^{\eta\|\psi(t)\|}\,dt,\qquad d=1\wedge\bar d,\qquad \tilde d(x,y)=\sqrt{d(x,y)\,(1+V(x)+V(y))},

with $V(x)=\|x\|^i$ ( $i\ge1$ ) or $V(x)=e^{v\|x\|}$ ( $v>0$ ).

There are two assumptions. Assumption 2.10 says that for $\|x\|\ge R$ every proposal within distance $r(\|x\|)$ of the proposal mean $(1-\rho)x$ is accepted with probability at least $e^{\alpha_l}$ , where $r(s)\le\frac\rho2 s$ . Assumption 2.13 says that $e^{-\Phi}$ is $\gamma$ -integrable and that $\varphi(r)=\sup_{x\ne y\in B_r(0)}|\Phi(x)-\Phi(y)|/\|x-y\|\le M_\kappa e^{\kappa r}$ for every $\kappa>0$ .

Formalization targets

Goal: Theorem 2.14

Under Assumption 2.10 with $r(s)=r s^a$ ( $r>0$ , $a\in(\frac12,1)$ ) and Assumption 2.13:

$\mu$ and every $\mu_m$ are the unique invariant probability measures of $\mathcal P$ and $\mathcal P_m$ .
For $\eta$ small enough and then $\varepsilon$ small enough, there is one $\tilde n$ such that for every $m$ and all probability measures $\nu_1,\nu_2$

\tilde d(\nu_1\mathcal P^{\tilde n},\nu_2\mathcal P^{\tilde n})\le\tfrac12\tilde d(\nu_1,\nu_2),\qquad \tilde d(\nu_1\mathcal P_m^{\tilde n},\nu_2\mathcal P_m^{\tilde n})\le\tfrac12\tilde d(\nu_1,\nu_2).

The essential point is that $\tilde n$ does not depend on $m$ .

Milestones

Lemma 3.5 (1)–(3): the comparison of $\bar d$ with $\|x-y\|e^{\eta(\|x\|\vee\|y\|)}/\varepsilon$ , and the contraction of $\bar d$ under a common-noise pCN step,

\bar d(p_x,p_y)\le(1-2\delta)^{1/2}e^{\eta[-\rho(\|x\|\vee\|y\|)+\sqrt{2\delta}\|\xi\|+J]}\bar d(x,y).

Lemma 3.6: $\mathcal P$ and every $\mathcal P_m$ are $d$ -contracting with one constant.
Lemma 3.7: bounded sets are $d$ -small for $\mathcal P^n$ and every $\mathcal P_m^n$ , with $n$ and $s$ independent of $m$ .

The paper derives Theorem 2.14 from these, from Lemma 3.2 (Lyapunov functions) and from Proposition 2.6 (the weak Harris theorem of Hairer, Mattingly and Scheutzow 2011). The last two are posed in mission I of this series.

Significance

A Wasserstein spectral gap uniform in $m$ means that the number of pCN steps needed to reach a given accuracy does not grow with the discretisation level. In §4 of the paper this yields a strong law of large numbers and a central limit theorem for pCN ergodic averages, and, combined with Theorem 2.15, an $L^2_\mu$ -spectral gap and mean-square error bounds, all uniform in the dimension. The locally Lipschitz case is the one that covers potentials of polynomial growth.

The result is proved in the paper. It has not been formalized. A formalization would produce a reusable weak-Harris toolkit for Markov kernels on Polish spaces, and a machine-checked account of the path-metric construction, which the paper adapts from Hairer and Majda (2010) and Hairer, Mattingly and Scheutzow (2011). It would also check the paper's proof, whose printed Lemma 3.5 (3) contains a typographical slip in the exponent; the formalized bound is the one the proof derives.

Difficulty

With $\Phi$ only locally Lipschitz, no single $\varepsilon$ makes $1\wedge\|x-y\|/\varepsilon$ contracting. The probability that exactly one of two coupled chains accepts is controlled by $|\Phi(x)-\Phi(y)|$ , and far from the origin this exceeds any fixed multiple of $\|x-y\|$ . The weighted path distance makes far-out points "close" only when they are very close in norm. But then even the "both accept" move can increase the distance, because the weight $e^{\eta\|\cdot\|}$ changes along the move. Showing that the shrinkage $(1-\rho)$ of the proposal mean beats this, while the Gaussian noise term stays integrable uniformly in $m$ , is the content of Lemmas 3.5 and 3.6. The order of the choices ( $R$ , then $\eta$ , then $\varepsilon$ ) is essential.

Formalization scope

$H$ is a real Hilbert space that is complete, separable and Borel. $\gamma$ is Mathlib's IsGaussian with mean zero. $(e_i)$ is a HilbertBasis ℕ whose vectors are pairwise uncorrelated under the covariance bilinear form.
$P_mH$ is a submodule. $\gamma_m$ is the pushforward under the orthogonal projection. $\mathcal P_m$ lives on the subtype $P_mH$ , with $\Phi$ and $V$ restricted to it and $d$ restricted from $H$ .
$\mu$ and $\mu_m$ are Mathlib's normalised tilted measures. The goal concludes that they are probability measures.
The Metropolis–Hastings kernel is built from Mathlib's Kernel.withDensity. Kernel powers are composition powers, and $\nu\mathcal P^n$ is Measure.bind.
Wasserstein lifts and $\bar d$ are infima in $[0,\infty]$ , so no junk zero arises from an empty or unbounded set. Unit speed is imposed on $(0,T)$ , so $\bar d(x,x)=0$ through the constant path with $T=0$ .
Contraction, smallness and Lyapunov constants are explicit arguments. "Uniform in $m$ " is "one constant for all $m$ ".
"Small enough" is $\exists\eta_0>0\ \forall\eta\in(0,\eta_0]\ \exists\varepsilon_0>0\ \forall\varepsilon\in(0,\varepsilon_0]$ .
Several readings are disclosed. " $r\in\mathbb R$ " is read as $r>0$ , $i\in\mathbb N$ as $i\ge1$ , and $v>0$ . Assumption 2.10 is stated for $s\ge0$ , the domain of $r$ , and requires $r(s)>0$ for $s>0$ so that the acceptance balls are nonempty. Its infimum and the supremum $\varphi(r)$ of Assumption 2.13 are stated pointwise.
The general form of Lemma 3.6 has a disclosed radius-floor hypothesis: $r(s)$ stays bounded away from zero for large $s$ . The printed proof needs a uniform positive probability for the proposal ball; this hypothesis supplies it. Theorem 2.14's power-law radius already meets it.
The formalization rules out trivialising readings. The tilted measure cannot be the zero measure, because the goal asserts it is a probability measure. Uniqueness is among probability measures. $V\equiv1$ is excluded. A $\tilde n$ chosen after $m$ would give a per-dimension gap, not this theorem.
A complete development needs:
- the weak Harris theorem (Proposition 2.6, mission I);
- Gaussian tail bounds of Fernique type, with the dimension-monotonicity of Lemma 3.1 (mission I);
- the Lyapunov drift Lemma 3.2 (mission I);
- calculus of $C^1$ paths in Hilbert space;
- synchronous couplings of Metropolis–Hastings kernels.
The Harris and coupling layers are reusable well beyond this paper. Contributions to any of them are welcome.

Selected references

M. Hairer, A. M. Stuart and S. J. Vollmer, Spectral gaps for a Metropolis–Hastings algorithm in infinite dimensions, arXiv:1112.1392v4 (2014), published in Ann. Appl. Probab. 24(6) (2014) 2455–2490, https://doi.org/10.1214/13-AAP982. https://arxiv.org/abs/1112.1392v4
M. Hairer, J. C. Mattingly and M. Scheutzow, Asymptotic coupling and a general form of Harris' theorem with applications to stochastic delay equations, Probab. Theory Related Fields 149 (2011) 223–259. MR2773030, https://mathscinet.ams.org/mathscinet-getitem?mr=2773030
M. Hairer and A. J. Majda, A simple framework to justify linear response theory, Nonlinearity 23 (2010) 909–922. MR2602020, https://mathscinet.ams.org/mathscinet-getitem?mr=2602020
A. Beskos, G. O. Roberts, A. M. Stuart and J. Voss, MCMC methods for diffusion bridges, Stoch. Dyn. 8 (2008) 319–350. MR2444507, https://mathscinet.ams.org/mathscinet-getitem?mr=2444507
S. L. Cotter, G. O. Roberts, A. M. Stuart and D. White, MCMC methods for functions: modifying old algorithms to make them faster, Statist. Sci. 28 (2013) 424–446. https://doi.org/10.1214/13-STS421

13 thms1 active userReviewed

Analysis Stochastic Systems·Captain: mikedeng1

Affine Volterra Processes 2: The Exponential-Affine Transform Formula via the Riccati–Volterra EquationResearch Paper

Motivation

Many stochastic models have a present state that depends on a weighted history of past drift and noise. A stochastic Volterra equation captures this dependence through a kernel $K$ : a recent increment and an older increment can enter the current state with different weights. Classical affine diffusions arise from the special constant kernel $K=I$ . For those diffusions, conditional Fourier–Laplace transforms can often be found from finite-dimensional Riccati ordinary differential equations. The paper by Abi Jaber, Larsson and Pulido asks for an analogous transform when the kernel retains memory. Its Theorem 4.3 gives a formula for a continuous affine Volterra process under a stated Riccati–Volterra solution assumption.

The result matters for models in which the history cannot be replaced by the current state alone. The transform characterizes conditional distributions and integrated path functionals in the form used by the paper's later results. The present mission isolates Theorem 4.3 and four of its stated supporting claims. The paper proves these results; the mission seeks machine-checked proofs of their Lean statements.

Setting

Fix a positive integer $d$ and a deterministic, matrix-valued kernel $K:[0,\infty)\to\mathbb R^{d\times d}$ whose entries are locally square integrable. The Volterra convolution of $K$ with a vector function $v$ is $(K*v)(t)=\int_0^t K(t-s)v(s)\,ds$ . Matrix convolutions retain the order of multiplication: $(K*R)(t)=\int_0^t K(t-s)R(s)\,ds$ .

Let $A^0,\ldots,A^d$ be real symmetric matrices and $b^0,\ldots,b^d$ real column vectors. Their affine covariance and drift are $a(x)=A^0+\sum_i x_iA^i$ and $b(x)=b^0+\sum_i x_i b^i$ . The matrix $B=(b^1\ \cdots\ b^d)$ has the $b^i$ as columns. For a complex row $u$ , write $A(u)=(uA^1u^\top,\ldots,uA^du^\top)$ ; the transpose is ordinary, with no complex conjugation.

An affine Volterra process $X$ is a continuous solution of

X_t=x_0+\int_0^t K(t-s)b(X_s)\,ds+\int_0^t K(t-s)\sigma(X_s)\,dW_s.

Here $W$ is a $d$ -dimensional Brownian motion on a usual stochastic basis, $x_0$ is deterministic, and $X$ stays in a state space $E$ . The continuous coefficient $\sigma$ obeys $\sigma(x)\sigma(x)^\top=a(x)$ on $E$ , where $a(x)$ is positive semidefinite. This is Definition 4.1 and the standing setting of Section 4 of the paper.

Formalization targets

The main target is Theorem 4.3. Fix a finite horizon $T$ , a complex row $u$ , and an integrable complex-row function $f$ . Suppose a square-integrable function $\psi$ solves the Riccati–Volterra equation

\psi=uK+\bigl(f+\psi B+\tfrac12A(\psi)\bigr)*K.

Define $Y$ by the stochastic integral and drift in equations (4.4)–(4.5). The theorem identifies $Y_t$ with a conditional mean plus a quadratic correction:

Y_t=\mathbb E[uX_T+(f*X)_T\mid\mathcal F_t] +\tfrac12\int_t^T\psi(T-s)a(\mathbb E[X_s\mid\mathcal F_t])\psi(T-s)^\top\,ds, \qquad 0\le t\le T.

It also states that $e^{Y}$ is a local martingale on $[0,T]$ . If it is a true martingale, then the exponential-affine transform formula is

\mathbb E\!\left[e^{uX_T+(f*X)_T}\mid\mathcal F_t\right]=e^{Y_t},\qquad t\le T.

The milestone list records Lemma 4.2's conditional and unconditional means, the mean Volterra equation stated in the proof of Theorem 4.3, the resolvent commutation claim in the proof of Lemma 4.4, and Lemma 4.4's equivalent Riccati equation. A second-kind resolvent $R_B$ of $-KB$ uses the paper's sign convention $H*R_B=R_B*H=H-R_B$ for $H=-KB$ ; the equivalent equation uses $E_B=K-R_B*K$ .

Significance

The conditional transform links a path-dependent stochastic equation to a deterministic nonlinear Volterra equation. It supplies a way to describe the law of a future state together with a linear functional of its past. The conditional-mean milestone separately gives a usable formula for $\mathbb E[X_T\mid\mathcal F_t]$ , while the resolvent milestones identify the deterministic kernel relations needed by the transform.

The source provides proofs of these claims. The formalization task is to check their assumptions and equalities against a precise model of Brownian Itô integration, conditional expectation, and matrix convolution. Published Lean definitions for Brownian motion and an Itô integral relation are reused. The affine Volterra process, its Riccati equation, and these theorem statements are drafted here; their proofs remain open.

Difficulty

The conditional payoff involves the entire path before $T$ , while $X$ generally has no finite-dimensional Markov state. Consequently, the familiar affine-diffusion formula in terms of $X_t$ alone is not the target of Theorem 4.3. Deterministic matrix convolutions are order-sensitive, and the two resolvents of $-KB$ and $-BK$ have different kernels. Stochastic convolutions also have integrands that depend on the terminal time. The passage from fixed-time integral equalities to a continuous local-martingale process requires care about versions and filtration adaptation.

Formalization scope

Processes use nonnegative real time, while deterministic kernels and interval integrals use real time. Finite-dimensional $L^p$ conditions are checked componentwise. Kernel and resolvent identities between locally integrable functions hold almost everywhere on positive time. Riccati equations hold almost everywhere on $[0,T]$ ; stochastic and conditional identities hold almost surely at each fixed time. The local-martingale claim uses the real and imaginary parts of the complex exponential, stopped at $T$ .

The process definition includes the Section 4 assumptions on symmetry, covariance positivity, continuity of $\sigma$ , deterministic $x_0$ , and the usual stochastic basis. Brownian Itô terms are constrained by the published integral relation. Deterministic drift convolutions require integrable integrands. The theorem asserts integrability of the payoff and of $X_s$ as conclusions, preventing conditional expectation from defaulting to zero. In (4.6) the conditional means $\mathbb E[X_s\mid\mathcal F_t]$ enter the $ds$ -integral through a jointly measurable version in $(s,\omega)$ , so that integral cannot default to zero. The dimension is positive, and the theorem does not specialize the kernel to $I$ or insert a resolvent assumption into its goal.

A complete development will need reusable results on locally integrable matrix kernels and their resolvents, stochastic Fubini interchange, moment bounds for Volterra solutions, and conditional expectation of the resulting integrals. The moment bound is posed as Lemma 3.1 in the companion existence mission. This draft includes the four listed milestones; Lemmas 2.1 and 2.5 from the source are left for a fuller stochastic Fubini and semimartingale encoding. Contributions that preserve their general hypotheses and conclusions are welcome.

Selected references

E. Abi Jaber, M. Larsson, and S. Pulido, Affine Volterra processes, arXiv:1708.08796v3, 2019. Preprint

14 thms1 active userReviewed

Machine Learning Optimization·Captain: mikedeng1

Stochastic Model-Based Minimization of Weakly Convex Functions 2: The Proximal Stochastic Subgradient Method Drives E‖∇φ_{1/ρ̄}(x_{t*})‖² to Zero at Rate O(1/√T)Research Paper

Motivation

The proximal stochastic subgradient method is the workhorse of large-scale learning: to minimize a regularized population risk $\varphi(x) = f(x) + r(x)$ with $f(x) = \mathbb E_{\xi \sim P}[f(x,\xi)]$ , it samples a data point, takes a step against a sampled subgradient of $f$ , and applies the proximal map of the regularizer $r$ . Its sample complexity is classical for convex problems ( $O(\varepsilon^{-2})$ samples for function accuracy $\varepsilon$ ) and for smooth nonconvex problems ( $O(\varepsilon^{-4})$ samples for gradient norm $\varepsilon$ , Ghadimi–Lan 2013). For problems that are both nonsmooth and nonconvex, however, no complexity bound was known for any reasonably broad class before Davis–Drusvyatskiy 2019.

Many such problems — robust phase retrieval, nonlinear least squares with an $\ell_1$ loss, conditional value-at-risk minimization with smooth losses, covariance estimation — are weakly convex: they become convex after adding a quadratic $\frac{\rho}{2}\|x\|^2$ . This mission formalizes the complexity guarantee of Davis and Drusvyatskiy for the proximal stochastic subgradient method on weakly convex problems.

Timeline. Nurminskii (1973) showed that for weakly convex $f(\cdot,\xi)$ and $r = 0$ the stochastic subgradient method has limit points that are stationary, without a rate. Ghadimi and Lan (2013) proved the $O(\varepsilon^{-4})$ rate for smooth $f$ . Davis and Drusvyatskiy (arXiv 2018, SIAM J. Optim. 2019) proved the first rate for the proximal stochastic subgradient method under weak convexity, measured by the gradient of the Moreau envelope; this is Theorem 3.4 of their paper.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. Let $r : \mathbb R^d \to \mathbb R \cup \{+\infty\}$ be closed (its epigraph is closed) and convex, with nonempty domain $D = \operatorname{dom} r$ , and let $f : \mathbb R^d \to \mathbb R$ be $\rho$ -weakly convex: $x \mapsto f(x) + \frac{\rho}{2}\|x\|^2$ is convex. Set $\varphi = f + r$ .

The subdifferential $\partial\psi(x)$ of a function $\psi$ at a point $x$ of its domain is the set of vectors $v$ with $\psi(y) \ge \psi(x) + \langle v, y - x\rangle + o(\|y - x\|)$ as $y \to x$ ; it is empty off the domain. For $\lambda > 0$ the Moreau envelope and the proximal map are

\psi_\lambda(x) = \min_y \Big\{\psi(y) + \tfrac{1}{2\lambda}\|y - x\|^2\Big\}, \qquad \operatorname{prox}_{\lambda\psi}(x) = \operatorname*{argmin}_y \Big\{\psi(y) + \tfrac{1}{2\lambda}\|y - x\|^2\Big\}.

Assumption A (stochastic subgradient oracle): on a probability space $(\Omega, \mathcal F, P)$ one can draw i.i.d. samples $\xi_0, \xi_1, \dots \sim P$ (A1); there are an open set $U \supseteq D$ and a measurable map $G$ with $\mathbb E_\xi[G(x,\xi)] \in \partial f(x)$ for all $x \in U$ (A2); and $\mathbb E_\xi\|G(x,\xi)\|^2 \le L^2$ for all $x \in D$ (A3).

Algorithm 3.1 starts at $x_0 \in D$ and, for $t = 0, \dots, T$ , samples $\xi_t$ and sets $x_{t+1} = \operatorname{prox}_{\alpha_t r}(x_t - \alpha_t G(x_t, \xi_t))$ . It returns $x_{t^*}$ with $t^*$ drawn from $\{0, \dots, T\}$ with probability $\alpha_t / \sum_i \alpha_i$ .

Formalization targets

Goal: Theorem 3.4, (3.15) and (3.16)

For $\bar\rho \in (\rho, 2\rho]$ and stepsizes $\alpha_t \in (0, 1/\bar\rho]$ ,

\mathbb E\big[\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2\big] \le \frac{\bar\rho}{\bar\rho - \rho}\cdot\frac{\big(\varphi_{1/\bar\rho}(x_0) - \min\varphi\big) + 2\bar\rho L^2\sum_{t=0}^T\alpha_t^2}{\sum_{t=0}^T\alpha_t},

and with $\alpha_t = \gamma/\sqrt{T+1}$ , $\gamma \in (0, \frac{1}{2\rho}]$ ,

\mathbb E\big[\|\nabla\varphi_{1/(2\rho)}(x_{t^*})\|^2\big] \le 2\cdot\frac{\big(\varphi_{1/(2\rho)}(x_0) - \min\varphi\big) + 4\rho L^2\gamma^2}{\gamma\sqrt{T+1}}.

Milestones

In the order the proof uses them: Lemma 2.1 (subdifferential characterization of weak convexity), the existence of $\hat v_t \in \partial f(\hat x_t)$ with $\bar\rho(x_t - \hat x_t) \in \partial r(\hat x_t) + \hat v_t$ (§3.2), Lemma 3.2 ( $\hat x_t$ is a proximal point of $r$ ), Lemma 3.3 (one-step contraction towards $\hat x_t$ ), Lemma 2.2 (the envelope is $C^1$ with $\nabla\varphi_\lambda(x) = \lambda^{-1}(x - \operatorname{prox}_{\lambda\varphi}(x))$ ), and the one-step descent estimate (3.14).

Significance

The result. A small $\|\nabla\varphi_\lambda(x)\|$ certifies that $x$ is within $\lambda\|\nabla\varphi_\lambda(x)\|$ of a point $\hat x$ with $\varphi(\hat x) \le \varphi(x)$ and $\operatorname{dist}(0, \partial\varphi(\hat x)) \le \|\nabla\varphi_\lambda(x)\|$ . Theorem 3.4 therefore gives a sample complexity of $O(\varepsilon^{-4})$ for reaching an $\varepsilon$ -nearly stationary point, matching the smooth rate, for a method that is run in practice without modification. The underlying observation — the method is an approximate descent method on the Moreau envelope — is reused in the paper's model-based analysis (Theorem 4.3) and in subsequent work on stochastic nonsmooth nonconvex optimization.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A complete development produces reusable infrastructure: the Fréchet subdifferential of extended-valued functions, weak convexity and its subgradient characterization, Moreau envelopes of weakly convex functions and their differentiability, nonexpansiveness of convex proximal maps, and the bookkeeping of iterates driven by i.i.d. samples under a product measure.

Difficulty

The obvious argument — show that $\varphi(x_t)$ decreases in expectation — fails: neither $\varphi(x_t) - \min\varphi$ nor $\operatorname{dist}(0, \partial\varphi(x_t))$ need tend to zero, and the latter is discontinuous in $x$ . Progress must be measured on the Moreau envelope, which requires comparing the iterate $x_{t+1}$ with the proximal point $\hat x_t$ of $\varphi$ , not of $r$ . In Lean, the heaviest single ingredient is Lemma 2.2 (differentiability of the envelope of an extended-valued weakly convex function), and the direction $4 \Rightarrow 1$ of Lemma 2.1, which in the paper rests on Rockafellar–Wets' characterization of convexity by monotonicity of the subdifferential.

Formalization scope

Carrier. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). An extended-valued function is a pair (domain $D$ , real values on $D$ ); closedness is closedness of $\{(x,t) : x \in D,\ \psi(x) \le t\}$ . The subdifferential is the published regular subgradient NonconvexSplitting.Shared.IsRegularSubgrad of the $+\infty$ -extended lift.
Proximal map. prox a z is a function constrained, for every $a > 0$ , to return a minimizer over $D$ of $r(y) + \frac{1}{2a}\|y - z\|^2$ ; this determines it uniquely.
Randomness. The samples $\xi_0, \dots, \xi_T$ form a point of $\Omega^{T+1}$ under the product measure $P^{\otimes(T+1)}$ ; $\mathbb E$ is the Bochner integral, and every bounded expectation is accompanied by a conclusion that its integrand is integrable. The conditional expectation $\mathbb E_t$ in Lemma 3.3 is the integral over one sample with the iterate held fixed.
Output index. Because $t^*$ is independent of the samples, $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_{t^*})\|^2$ is the $\alpha$ -weighted average of $\mathbb E\|\nabla\varphi_{1/\bar\rho}(x_t)\|^2$ , as in the paper's (3.17).
$\min\varphi$ is an arbitrary real lower bound $\varphi^*$ of $\varphi$ on $D$ .
Corrected constant in (3.14). The paper prints the last term of (3.14) as $\alpha_t^2\bar\rho L^2$ ; its proof, and the unfolded sum leading to (3.15), give $2\alpha_t^2\bar\rho L^2$ , and that is what is stated. (3.15) and (3.16) are stated as printed.
Lemma 2.1 is stated for items 1–4; the clause for $C^2$ -smooth functions is not stated. Lemma 2.2 adds the implicit hypotheses that $\varphi$ is closed and proper, and includes existence and uniqueness of the proximal point.
Ruling out trivializations. The proximal map is tied to $r$ , $G$ is tied to $\partial f$ by (A2), $\min\varphi$ is not a real infimum, and integrability is concluded, so neither a junk value nor an unconstrained selection can make the statements hold vacuously; the hypotheses are satisfied by $r = f = 0$ , $G = 0$ .
Contributions welcome: proofs of the milestones, general lemmas on Moreau envelopes of weakly convex functions, and the nonexpansiveness of convex proximal maps on a closed convex domain.

Selected references

D. Davis and D. Drusvyatskiy, Stochastic Model-Based Minimization of Weakly Convex Functions, SIAM J. Optim. 29(1), 2019; arXiv:1803.06523v3, 2018. https://arxiv.org/abs/1803.06523
S. Ghadimi and G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://doi.org/10.1137/120880811
R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3), 1951. https://doi.org/10.1214/aoms/1177729586

12 thms1 active userReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Stochastic Model-Based Minimization of Weakly Convex Functions 4: Under Convexity, Stochastic Model-Based Minimization Reaches Expected Function Gap (½‖x₀−x*‖² + L²γ²)/(γ√(T+1))Research Paper

Motivation

Many problems in statistical learning and signal processing take the form of minimizing an expectation $f(x)=\mathbb E_\xi[F(x,\xi)]$ plus a regularizer or constraint $r(x)$ , where the only access to $f$ is through samples $\xi\sim P$ . The classical tool is the stochastic (proximal) subgradient method, which replaces $f$ at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss $F(\cdot,\xi)$ , and the stochastic prox-linear method linearizes only the smooth inner part of a composite loss $h(c(x,\xi))$ . In experiments the richer models are markedly less sensitive to the choice of step size.

Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization, in which each step minimizes a sampled one-sided model $f_{x_t}(\cdot,\xi_t)$ of $f$ plus $r$ plus a quadratic penalty. Their main theorem (Theorem 4.3) covers weakly convex problems through the Moreau envelope. This mission formalizes the companion result for the convex setting, Theorem 4.1: when the models lower-bound $f$ in expectation without quadratic error and $f_x(\cdot,\xi)+r$ is convex, the expected function gap at a weighted average of the iterates decays like $1/\sqrt T$ . As the paper notes (p. 22), for the stochastic proximal subgradient method this improves earlier bounds (Cruz 2017; Duchi–Singer 2009) because no subgradient norm of $r$ enters the estimate.

Setting

Work in $\mathbb R^d$ with the Euclidean norm. The problem is

\min_{x\in\mathbb R^d}\ \varphi(x):=f(x)+r(x),

where $f:\mathbb R^d\to\mathbb R$ is locally Lipschitz and $r:\mathbb R^d\to\mathbb R\cup\{+\infty\}$ is closed (its epigraph is closed) with nonempty domain $D=\operatorname{dom}r$ . A function $\psi$ is $\rho$ -weakly convex if $x\mapsto\psi(x)+\frac\rho2\|x\|^2$ is convex; $\rho=0$ is ordinary convexity.

Assumption B (p. 18) fixes a probability space $(\Omega,\mathcal F,P)$ , an open convex set $U\supseteq D$ , real constants $\tau,\eta,\mathsf L$ , a measurable model $(x,y,\xi)\mapsto f_x(y,\xi)$ on $U\times U\times\Omega$ and a measurable $L:\Omega\to\mathbb R_+$ such that:

(B1) i.i.d. samples $\xi_0,\xi_1,\dots\sim P$ can be drawn;
(B2) $\mathbb E_\xi[f_x(x,\xi)]=f(x)$ and $\mathbb E_\xi[f_x(y,\xi)-f(y)]\le\frac\tau2\|y-x\|^2$ for $x,y\in U$ ;
(B3) $f_x(\cdot,\xi)+r$ is $\eta$ -weakly convex for every $x\in U$ and almost every $\xi$ ;
(B4) $\sqrt{\mathbb E[L(\xi)^2]}\le\mathsf L$ and $f_x(x,\xi)-f_x(y,\xi)\le L(\xi)\|x-y\|$ for $x,y\in U$ and almost every $\xi$ .

Algorithm 4.1 (p. 19) starts at $x_0$ and, for $t=0,\dots,T$ , samples $\xi_t\sim P$ and sets

x_{t+1}=\operatorname*{argmin}_{x}\Big\{r(x)+f_{x_t}(x,\xi_t)+\frac{\beta_t}{2}\|x-x_t\|^2\Big\}.

The convex setting is $\tau=0$ and $\eta=0$ . Write $\alpha_t=\beta_t^{-1}>0$ for the step sizes and let $x^*$ be any minimizer of $\varphi$ .

Formalization targets

Goal: Theorem 4.1, (4.17) and (4.18)

For every $T>0$ ,

\mathbb E\Big[\varphi\Big(\tfrac{1}{\sum_{t=0}^T\alpha_t}\textstyle\sum_{t=0}^T\alpha_t x_{t+1}\Big)-\varphi(x^*)\Big]\le\frac{\frac12\|x_0-x^*\|^2+2\mathsf L^2\sum_{t=0}^T\alpha_t^2}{\sum_{t=0}^T\alpha_t},

and with the constant step $\alpha_t=\gamma/\sqrt{T+1}$ , $\gamma>0$ ,

\mathbb E\Big[\varphi\Big(\tfrac{1}{T+1}\textstyle\sum_{t=1}^{T+1}x_t\Big)-\varphi(x^*)\Big]\le\frac{\frac12\|x_0-x^*\|^2+2\mathsf L^2\gamma^2}{\gamma\sqrt{T+1}}.

The factor $2$ in front of $\mathsf L^2$ is the constant the paper's proof establishes; see Formalization scope.

Milestones

Lemma 4.1: $\varphi$ is $(\tau+\eta)$ -weakly convex and $|f(x)-f(y)|\le\mathsf L\|x-y\|$ on $U$ .
Lemma 4.2, (4.8): for every $x\in\operatorname{dom}r$ , with $x_t$ fixed and $\mathbb E_t$ the expectation over $\xi_t$ ,

\mathbb E_t\|x_{t+1}-x\|^2\le\frac{\beta_t+\tau}{\beta_t-\eta}\|x_t-x\|^2-\frac{2}{\beta_t-\eta}\mathbb E_t[\varphi(x_{t+1})-\varphi(x)]+\frac{4\mathsf L^2}{\beta_t(\beta_t-\eta)}.

Proof of Theorem 4.1, first display (p. 23): $2\alpha_t\mathbb E[\varphi(x_{t+1})-\varphi(x^*)]\le\mathbb E\|x_t-x^*\|^2-\mathbb E\|x_{t+1}-x^*\|^2+4\mathsf L^2\alpha_t^2$ .

Significance

Theorem 4.1 is the function-value guarantee of the model-based framework. Theorem 4.3 measures progress by the gradient of the Moreau envelope, which is the right quantity for nonconvex problems but says nothing directly about suboptimality; under convexity, Theorem 4.1 gives the familiar $O(1/\sqrt T)$ rate for the gap itself. It applies to the stochastic proximal point and prox-linear methods as well as to the proximal subgradient method, and §4.2 of the paper uses it for minimizing an expectation of a pointwise maximum of convex functions, such as the conditional value-at-risk. The estimate (4.8) behind it is also the engine of the strongly convex rate $O(1/(\mu T))$ (Theorem 4.2, a separate mission of this series).

The result is proved in the paper; nothing in it is open. To our knowledge none of these statements has a machine-checked proof. The formalization contributes a checked version of the one-step estimate (4.8) with its corrected constant, a reusable Lean encoding of Assumption B and of Algorithm 4.1 with extended-valued $r$ , and the passage from conditional one-step bounds to expectations over the product measure of the samples.

Difficulty

The argument is short on paper; the work lies in the measure theory the paper leaves implicit. The iterate $x_{t+1}$ is an argmin that depends on $x_t$ and on the fresh sample $\xi_t$ , and the one-step estimate holds only conditionally, with $x_t$ frozen. Turning it into an inequality between unconditional expectations requires measurability of the iterates, independence of $\xi_t$ from the past, and integrability of $\varphi(x_{t+1})$ and $\|x_{t+1}-x^*\|^2$ , which the paper takes for granted. The convex function $\varphi$ is extended-valued, so the function gap is meaningful only because every iterate and every average lies in $\operatorname{dom}r$ .

A naive one-step argument that bounds $f(x_t)-f(x_{t+1})$ and $f_{x_t}(x_t,\xi_t)-f_{x_t}(x_{t+1},\xi_t)$ separately, each by a Lipschitz constant times $\|x_{t+1}-x_t\|$ , gives the constant $4\mathsf L^2$ in (4.8) and not the printed $2\mathsf L^2$ . The printed constant is false (see below), so the constant cannot be improved simply by tightening that one step.

Formalization scope

Space and encoding. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The extended-valued $r$ is a real function together with its domain D; closedness of $r$ is closedness of $\{(x,t):x\in D,\ r(x)\le t\}$ , and convexity is ConvexOn ℝ D. $\mathsf L$ is L and $L(\xi)$ is Lfun.
Randomness. The $T+1$ samples are a point of $\Omega^{T+1}$ under the product measure $P^{\otimes(T+1)}$ ; expectations are Bochner integrals. Every theorem that bounds an expectation also concludes integrability of the integrand, so the junk value $0$ of a non-integrable integral cannot make a bound hold vacuously. The single-step estimate (4.8) holds $x_t$ fixed and integrates over one sample; integrability of $r(x_{t+1})$ is a hypothesis there, and a conclusion in the run-level statements, where the minimizer $x^*$ supplies the lower bound.
Algorithm. The iterates are the run of an update map that always lies in $D$ , is jointly measurable, and is a minimizer of the subproblem for almost every sample. An unconstrained update map would make the goal false; this one is pinned to the paper's step. $x_0\in U$ is assumed, since the model is only defined on $U$ . The parameter $\bar\rho$ of Algorithm 4.1 does not affect the iterates, and requiring $\beta_t>\bar\rho>\tau+\eta=0$ over the steps used is the same as $\alpha_t>0$ .
Minimizer. $x^*\in D$ with $\varphi(x^*)\le\varphi(y)$ for all $y\in D$ . A minimizer of $f$ alone, or an arbitrary point, would trivialize the goal; convexity of $\varphi$ is not assumed separately, since it follows from Lemma 4.1.
Corrected constant (paper typo). The paper prints $2\mathsf L^2/(\beta_t(\beta_t-\eta))$ in (4.8), $2\mathsf L^2\alpha_t^2$ in the first display of the proof of Theorem 4.1, and $\mathsf L^2$ in (4.17)–(4.18). Its own proof of (4.8) (p. 21) bounds the error terms by $2\mathsf L^2/\beta_t$ and divides by $(\beta_t-\eta)/2$ , which gives $4\mathsf L^2/(\beta_t(\beta_t-\eta))$ . The printed (4.8) and the printed first display fail on a one-dimensional example ( $r=0$ , $f=|\cdot|$ , a linear model with slope $\pm1$ at the origin, $\beta=1$ ). The Lean statements carry the constants the proof establishes: $4\mathsf L^2$ in (4.8) and the display, $2\mathsf L^2$ in (4.17)–(4.18). Whether the printed (4.17) holds by a sharper argument is not settled here; the milestone texts quote the page verbatim.
Needed infrastructure. Product measures and independence of coordinates (Measure.pi), Fubini–Tonelli over $\Omega^{t}\times\Omega$ , measurability of the run, Jensen's inequality for a convex function on a convex set, and strong convexity of the subproblem. Proofs of any milestone are welcome, as are a general "conditional one-step bound to expectation over the run" lemma reusable by the other missions of this series.

Selected references

D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1):207–239, 2019; arXiv:1803.06523v3. https://arxiv.org/abs/1803.06523
J. Duchi, Y. Singer, Efficient online and batch learning using forward backward splitting, J. Mach. Learn. Res. 10:2899–2934, 2009. https://jmlr.org/papers/v10/duchi09a.html
J. Cruz, On proximal subgradient splitting method for minimizing the sum of two nonsmooth convex functions, Set-Valued Var. Anal. 25:245–263, 2017. https://doi.org/10.1007/s11228-016-0376-5

6 thms1 active userReviewed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Stochastic Model-Based Minimization of Weakly Convex Functions 5: Under μ-Strong Convexity, Model-Based Minimization with β_t = μ(t+1)/2 Reaches Expected Function Gap O(1/(μT))Research Paper

Motivation

Many problems in statistical learning and signal processing minimize an expectation $f(x)=\mathbb E_\xi[F(x,\xi)]$ plus a regularizer or constraint $r(x)$ , with access to $f$ only through samples $\xi\sim P$ . The standard tool is the stochastic (proximal) subgradient method, which replaces $f$ at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss $F(\cdot,\xi)$ , and the stochastic prox-linear method linearizes only the smooth inner map of a composite loss $h(c(x,\xi))$ . The richer models are markedly less sensitive to the step size in practice.

Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization: each step minimizes a sampled one-sided model $f_{x_t}(\cdot,\xi_t)$ of $f$ , plus $r$ , plus a quadratic penalty. Their main theorem (Theorem 4.3) concerns weakly convex problems. This mission formalizes the companion result for the strongly convex setting, Theorem 4.2: when the models lower-bound $f$ in expectation and $f_x(\cdot,\xi)+r$ is $\mu$ -strongly convex, the expected function gap at a nonuniformly weighted average of the iterates decays like $1/(\mu T)$ . The weighting is the technique of Schmidt, Le Roux and Bach (2012) for the projected stochastic subgradient method; the paper extends it to the fully proximal, model-based setting (p. 23).

Setting

Work in $\mathbb R^d$ with the Euclidean norm. The problem is

\min_{x\in\mathbb R^d}\ \varphi(x):=f(x)+r(x),

where $f:\mathbb R^d\to\mathbb R$ is locally Lipschitz and $r:\mathbb R^d\to\mathbb R\cup\{+\infty\}$ is closed (its epigraph is closed) with nonempty domain $D=\operatorname{dom}r$ . A function $\psi$ is $\rho$ -weakly convex if $x\mapsto\psi(x)+\frac\rho2\|x\|^2$ is convex; a negative modulus $\rho=-\mu$ is $\mu$ -strong convexity.

Assumption B (p. 18) fixes a probability space $(\Omega,\mathcal F,P)$ , an open convex set $U\supseteq D$ , real constants $\tau,\eta,\mathsf L$ , a measurable model $(x,y,\xi)\mapsto f_x(y,\xi)$ on $U\times U\times\Omega$ and a measurable $L:\Omega\to\mathbb R_+$ such that:

(B1) i.i.d. samples $\xi_0,\xi_1,\dots\sim P$ can be drawn;
(B2) $\mathbb E_\xi[f_x(x,\xi)]=f(x)$ and $\mathbb E_\xi[f_x(y,\xi)-f(y)]\le\frac\tau2\|y-x\|^2$ for $x,y\in U$ ;
(B3) $f_x(\cdot,\xi)+r$ is $\eta$ -weakly convex for every $x\in U$ and almost every $\xi$ ;
(B4) $\sqrt{\mathbb E[L(\xi)^2]}\le\mathsf L$ and $f_x(x,\xi)-f_x(y,\xi)\le L(\xi)\|x-y\|$ for $x,y\in U$ and almost every $\xi$ .

Algorithm 4.1 (p. 19) starts at $x_0$ and, for $t=0,\dots,T$ , samples $\xi_t\sim P$ and sets

x_{t+1}=\operatorname*{argmin}_{x}\Big\{r(x)+f_{x_t}(x,\xi_t)+\frac{\beta_t}{2}\|x-x_t\|^2\Big\}.

The strongly convex setting is $\tau=0$ and $\eta=-\mu$ with $\mu>0$ , run with $\beta_t=\mu(t+1)/2$ . Let $x^*$ be any minimizer of $\varphi$ .

Formalization targets

Goal: Theorem 4.2

For every integer $T>0$ ,

\mathbb E\Big[\varphi\Big(\frac{2}{(T+2)(T+3)-2}\sum_{t=1}^{T+1}(t+1)\,x_t\Big)-\varphi(x^*)\Big]\le\frac{\mu\|x_0-x^*\|^2}{(T+2)^2}+\frac{16\mathsf L^2}{\mu(T+2)},

together with integrability of the function inside the expectation. The paper prints $8\mathsf L^2$ ; see Formalization scope.

Milestones

Lemma 4.1 (p. 18): $\varphi$ is $(\tau+\eta)$ -weakly convex and $|f(x)-f(y)|\le\mathsf L\|x-y\|$ on $U$ .
Lemma 4.2, (4.8) (p. 20): for a fixed current point $x_t$ and any $x\in\operatorname{dom}r$ ,

\mathbb E_t\|x_{t+1}-x\|^2\le\frac{\beta_t+\tau}{\beta_t-\eta}\|x_t-x\|^2-\frac{2}{\beta_t-\eta}\mathbb E_t[\varphi(x_{t+1})-\varphi(x)]+\frac{4\mathsf L^2}{\beta_t(\beta_t-\eta)}.

Proof of Theorem 4.2, first display (p. 23): with $\Delta_t=\frac12\mathbb E\|x^*-x_t\|^2$ ,

\mathbb E[\varphi(x_{t+1})-\varphi(x^*)]\le\beta_t\Delta_t-(\beta_t+\mu)\Delta_{t+1}+\frac{2\mathsf L^2}{\beta_t}.

Significance

The result. Theorem 4.2 is the $O(1/(\mu T))$ rate for a whole family of stochastic methods at once: the stochastic proximal point, prox-linear and proximal subgradient methods all satisfy Assumption B (§4.2 of the paper). The rate is in function values at an explicit averaged point, with explicit constants, and needs neither smoothness of $f$ nor bounded subgradients of $r$ : the regularizer enters only through the strong convexity of the subproblems. The $1/(\mu T)$ order is the one Schmidt, Le Roux and Bach obtained for the projected stochastic subgradient method; Theorem 4.2 extends it to models that are not linear and to a general closed $r$ .

Formalizing it. The result is proved in the paper; it is not formalized anywhere to our knowledge. Formalizing it pins down the exact constant (the printed one does not follow from the paper's lemmas; see below), the measure-theoretic content of "iterates generated by Algorithm 4.1" (a measurable selection of the argmin, the product measure of the samples, conditional expectation as an integral over one fresh sample) and the integrability that the expectations presuppose. The one-step estimate (4.8) is shared with mission 4 of this series (Theorem 4.1, convex setting); a proof of it serves both.

Difficulty

The telescoping that turns the one-step bound into the rate is elementary once the weights $t+2$ are chosen. The work lies in two places. First, (4.8) itself: it combines the strong convexity of the subproblem, the one-sided accuracy (B2) used in expectation, the Lipschitz bound (B4) at the random point $x_{t+1}$ (so the exceptional null set must not depend on that point), Cauchy–Schwarz, and Lemma 4.1. Second, the passage from one step with $x_t$ held fixed to expectations over the whole run: this needs the independence of $\xi_t$ from $\xi_0,\dots,\xi_{t-1}$ (Fubini on the product measure) and integrability of $r$ , $\|x_t-x^*\|^2$ and $\varphi(x_{t+1})$ along the run, none of which is stated on the page. A natural first attempt, bounding $\varphi$ at the average by the average of $\varphi$ before checking that the average lies in $D$ , is valid only because the weights sum to one and $D$ is convex by (B3).

Formalization scope

Carrier and extended values. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The extended-valued $r$ is encoded by its domain D and its real values on D; closedness is closedness of $\{(x,t):x\in D,\ r(x)\le t\}$ . $\mu$ -strong convexity is $(-\mu)$ -weak convexity: convexity of $\psi-\frac\mu2\|\cdot\|^2$ on D.
Randomness. The $T+1$ samples are a point of $\Omega^{T+1}$ under Measure.pi; expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion, so a junk value $0$ cannot make a bound hold. $\mathbb E_t$ in (4.8) is the integral over one fresh sample with $x_t$ held fixed.
Iterates. The update is a jointly measurable map that lies in $D$ and is a minimizer of the subproblem for almost every sample; the run is driven by it. Measurability of the update and $x_0\in U$ are added hypotheses. The parameter $\bar\rho$ of Algorithm 4.1 does not affect the iterates (any $\bar\rho\in(-\mu,\mu/2)$ is admissible for all $t$ ) and does not appear. $x^*$ is any minimizer of $\varphi=f+r$ over $D$ .
Constant correction. The proof of (4.8) on p. 21 bounds the $\delta$ -terms by $2\mathsf L^2/\beta_t$ and divides by $(\beta_t-\eta)/2$ , which gives $4\mathsf L^2/(\beta_t(\beta_t-\eta))$ ; the display prints $2\mathsf L^2/(\beta_t(\beta_t-\eta))$ , which fails on a one-dimensional example. Carried through the proof of Theorem 4.2, the corrected constant gives $2\mathsf L^2/\beta_t$ in the first display (printed $\mathsf L^2/\beta_t$ ) and $16\mathsf L^2/(\mu(T+2))$ in the theorem (printed $8\mathsf L^2$ ). The Lean states the proof's constants; the milestone texts are quoted as printed. Whether the printed $8\mathsf L^2$ bound holds by a sharper argument is open here.
Trivializations ruled out. The stepsize is fixed to $\beta_t=\mu(t+1)/2$ , the update is constrained to the argmin, $x^*$ minimizes $\varphi$ (not $f$ ), and the modulus is $-\mu$ , not $\mu$ ( $\mu$ -weak convexity would make the theorem false).
Contributions welcome. A proof of (4.8) from Assumption B, the Fubini/independence step for the run, and integrability lemmas for argmin selections are reusable across the series.

Selected references

D. Davis, D. Drusvyatskiy, Stochastic model-based minimization of weakly convex functions, SIAM J. Optim. 29(1):207–239, 2019; arXiv:1803.06523v3. https://arxiv.org/abs/1803.06523
M. Schmidt, N. Le Roux, F. Bach, A simpler approach to obtaining an O(1/t) convergence rate for the projected stochastic subgradient method, arXiv:1212.2002, 2012 (cited as [62] in the paper). https://arxiv.org/abs/1212.2002

6 thms1 active userReviewed

Analysis Stochastic Systems·Captain: mikedeng1

Affine Volterra Processes 1: Nonnegative Weak Solutions of Stochastic Volterra Equations with Resolvent-Monotone KernelsResearch Paper

Motivation

Many stochastic models use a process whose response to a disturbance depends on the time elapsed since that disturbance. An ordinary stochastic differential equation uses only the current state and instantaneous coefficients. A stochastic Volterra equation instead weights its past drift and noise through a convolution kernel. Such equations include the constant kernel as a familiar limiting case, while singular or decaying kernels allow different memory patterns. The paper Affine Volterra processes studies this class to obtain non-Markovian models that retain tractable affine transform formulas. Before any transform can be used for a nonnegative state variable, the underlying equation must actually admit a solution that stays nonnegative. Abi Jaber, Larsson and Pulido, §§1–3.

The mission focuses on the paper's existence and invariance theorem, Theorem 3.6 of the pinned preprint. It is a separate question from uniqueness or explicit transforms: the coefficients are only continuous with linear growth, so classical contraction arguments for Lipschitz coefficients do not directly settle it. The proof also has to preserve the boundary of the nonnegative orthant despite a drift and noise term that depend on the entire past. Abi Jaber, Larsson and Pulido, Theorems 3.3–3.6.

Setting

Fix dimensions $d,m\ge0$ . The kernel $K$ is a deterministic function from nonnegative time to real $d\times d$ matrices. The drift $b$ maps $\mathbb R^d$ to $\mathbb R^d$ , and the diffusion coefficient $\sigma$ maps $\mathbb R^d$ to real $d\times m$ matrices. Given a deterministic initial state $x_0$ and an $m$ -dimensional Brownian motion $W$ , a continuous adapted process $X$ solves

X_t=x_0+\int_0^t K(t-s)b(X_s)\,ds+ \int_0^t K(t-s)\sigma(X_s)\,dW_s,\qquad t\ge0.

The deterministic and stochastic terms are matrix-vector convolutions: an event at time $s$ has an effect at time $t$ weighted by $K(t-s)$ . A weak solution is allowed to choose its stochastic basis and Brownian motion. A strong solution is adapted to the completed filtration generated by its prescribed Brownian motion. All bases satisfy the usual completeness and right-continuity conditions. The equation is read at each fixed time almost surely, with $X$ having continuous sample paths. Abi Jaber, Larsson and Pulido, (1.1), §3.

The paper's condition (2.5) asks each scalar kernel entry to be locally square-integrable and to satisfy two estimates of order $h^\gamma$ as $h\downarrow0$ : the integral of its square over $[0,h]$ , and the squared $L^2$ difference between its time shift by $h$ and itself over each finite interval. The exponent satisfies $0<\gamma\le2$ and may differ by entry. For the goal, $K$ is diagonal. Each diagonal entry $K_i$ is nonnegative, nonzero, nonincreasing and continuous on positive time. Its resolvent of the first kind $L_i$ is a nonnegative measure whose convolution with $K_i$ is the constant one; condition (3.4) also requires the interval mass $L_i([s,s+t])$ to be nonincreasing in $s$ for every $t\ge0$ . Abi Jaber, Larsson and Pulido, (2.5), (2.13), (3.4).

Formalization targets

Nonnegative weak existence

The goal is Theorem 3.6. Write $\mathbb R^d_+=\{x\in\mathbb R^d:x_i\ge0\text{ for all }i\}$ . Suppose $K$ is diagonal and satisfies (2.5) and (3.4) componentwise. Suppose $b$ and $\sigma$ are continuous, satisfy $\max\{|b(x)|,\|\sigma(x)\|\}\le c_{\mathrm{LG}}(1+|x|)$ , and obey the boundary condition for every $x\in\mathbb R^d$ :

x_i=0\quad\Longrightarrow\quad b_i(x)\ge0\ \text{and}\ \sigma_{ik}(x)=0\quad\text{for every }k.

Then the target is

\forall x_0\in\mathbb R^d_+,\quad \exists\text{ a continuous weak solution }X\text{ of (1.1) with }X_t\in\mathbb R^d_+.

The milestone list records the paper's moment bound, strong existence for Lipschitz coefficients, and general weak existence with a first-kind resolvent. They are numbered results from the same preprint and establish distinct parts of the existence framework. Abi Jaber, Larsson and Pulido, Lemma 3.1 and Theorems 3.3, 3.4, 3.6.

Significance

The conclusion says more than finite-time nonnegativity of a proposed process: it asserts that a stochastic basis, Brownian motion and continuous solution actually exist for every nonnegative initial condition under the stated kernel and boundary assumptions. This supports later use of the affine transform results on state spaces with nonnegative coordinates. The paper treats this existence theorem as one of the main inputs to its square-root and rough-volatility examples. Abi Jaber, Larsson and Pulido, §§3, 6.

The theorem is already proved in the source paper. The formalization task is to state and eventually verify that known result in Lean, including the exact memory-kernel condition and the stochastic basis chosen by weak existence. The published Brownian and Itô-integral definitions are reused. A verified solution would leave reusable definitions for Volterra kernels, first-kind resolvents, and weak convolution equations, as well as machine-checked statements for the supporting existence theorems.

Difficulty

For Lipschitz coefficients, the paper obtains a unique strong solution. The goal permits only continuous coefficients of linear growth. Approximating them by better-behaved coefficients does not by itself guarantee that a limit solves the original convolution equation or remains in the nonnegative orthant. The stochastic convolution depends on the full history through $K(t-s)$ , and the boundary condition must be propagated through that memory. A direct appeal to an ordinary SDE invariance theorem therefore does not cover the claim. The first-kind resolvent and the monotonicity in (3.4) are central to the stated assumptions. Abi Jaber, Larsson and Pulido, proofs of Theorems 3.4 and 3.6.

Formalization scope

Lean uses EthierKurtz.SDEState d, a Euclidean $d$ -vector, for states; real matrices for $K$ and $\sigma$ ; nonnegative real process time; and real arguments for deterministic kernels and interval integrals. Local $L^2$ membership is componentwise, which is equivalent to membership under any norm on the finite-dimensional matrix space. The matrix norm in linear growth is the Euclidean operator norm. The big- $O$ bounds in (2.5) are taken as $h$ tends to zero from the right. Each diagonal kernel has its own exponent and its own positive resolvent measure. A general matrix first-kind resolvent is encoded entrywise as the difference of two measures finite on compact positive-time intervals, so it may have infinite total mass.

The weak-solution predicate existentially quantifies the stochastic basis, Brownian motion and continuous process. Each stochastic convolution has a witness satisfying the published Brownian Itô relation; an unconstrained process cannot witness the equation. Drift terms carry interval integrability, avoiding a default-zero value for a nonintegrable integral. The stochastic basis is complete at time zero and right-continuous. The goal asserts orthant membership at every fixed time almost surely; continuous paths yield an orthant-valued version. The zero-time equation and empty-index cases are included. Contributions that formalize stochastic-convolution continuity, compactness of path laws, first-kind resolvent calculus, or invariance of the orthant are in scope.

Selected references

E. Abi Jaber, M. Larsson and S. Pulido, Affine Volterra processes, arXiv:1708.08796v3, 2019. Preprint

12 thms1 active userReviewed