All missions

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.

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.

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:

1. Lemma 1: the integral operator $L$ of $K$ equals $\int\psi_\omega\otimes\psi_\omega\,d\pi(\omega)$.
2. Lemma 2: the component of the regression function orthogonal to the range of $L$ is invisible to every random-features predictor, almost surely.
3. Proposition 4 (Cordes), Proposition 9 (interpolation $\|XA^\sigma\|\le\|X\|^{1-\sigma}\|XA\|^\sigma$) and Proposition 8 (a multiplicative bound between regularized operators).
4. 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.
5. 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

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

1. 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.
2. §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$.
3. 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))$.
4. 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

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:

1. $\mu$ and every $\mu_m$ are the unique invariant probability measures of $\mathcal P$ and $\mathcal P_m$.
2. 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

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

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:

1. (B1) i.i.d. samples $\xi_0,\xi_1,\dots\sim P$ can be drawn;
2. (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$;
3. (B3) $f_x(\cdot,\xi)+r$ is $\eta$-weakly convex for every $x\in U$ and almost every $\xi$;
4. (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

1. Lemma 4.1: $\varphi$ is $(\tau+\eta)$-weakly convex and $|f(x)-f(y)|\le\mathsf L\|x-y\|$ on $U$.
2. 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)}.$$

3. 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