Dependencies

The statement \(\mathrm{Cov}(N_1,N_2)(s) \sim c(q)\sqrt s\) with \(c(1/2) = 0.099 \pm 0.003\) (Monte Carlo), as a named Prop-valued definition — no truth claim is made; anyone wishing to use it must supply a proof of covConjecture explicitly.

A named countable dense subset \(\mathcal{D} \subseteq \mathcal{S}(\mathbb {R},\mathbb {R})\), chosen once from separability, together with the countable-reduction principle: for a continuous linear functional \(F\) and a continuous seminorm \(q\), the bound \(|F\varphi | \le q(\varphi )\) on any dense set of \(\varphi \) already implies it for every \(\varphi \), since the bound cuts out a closed set. This is the measurability hook used downstream.

The Hermite functions are \(h_n(x) = c_n H_n(x)\, e^{-x^2/4}\), where \(H_n\) is the probabilists’ Hermite polynomial (Mathlib’s Polynomial.hermite, monic, orthogonal for the weight \(e^{-x^2/2}\)) and \(c_n = \bigl(\sqrt{n!\, \sqrt{2\pi }}\bigr)^{-1}\) is derived so that the family is \(L^2\)-normalized for Lebesgue measure. The orthogonality relation \(\int H_m H_n e^{-x^2/2}\, dx = \delta _{mn}\, n!\, \sqrt{2\pi }\) is proved by induction from a Rodrigues-type recurrence, and yields \(\int h_m h_n\, dx = \delta _{mn}\). Each \(h_n\) is bundled as a Schwartz function (polynomial times Gaussian decay).

The harmonic oscillator \(A f = -f'' + (x^2/4 + 1/2)\, f\) is a continuous linear map \(\mathcal{S}(\mathbb {R},\mathbb {R}) \to \mathcal{S}(\mathbb {R},\mathbb {R})\), built from Mathlib’s Laplacian CLM and multiplication by the temperate-growth multiplier \(x^2/4 + 1/2\). It is symmetric for the \(L^2\) pairing, \(\int (Af)\, g = \int f\, (Ag)\), and the Hermite functions are its eigenfunctions: \(A h_n = (n+1)\, h_n\), proved from the ladder identities for \(h_n\).

The dual \(\mathrm{SchDual}\) is the space of continuous linear functionals \(\mathcal{S}(\mathbb {R},\mathbb {R}) \to \mathbb {R}\) carrying Mathlib’s topology of pointwise (weak-\(*\)) convergence (PointwiseConvergenceCLM). For a seminorm \(q\) on \(\mathcal{S}(\mathbb {R},\mathbb {R})\), the polar ball is \(\mathrm{polarBall}(q) = \{ F \in \mathrm{SchDual} \mid \forall \varphi ,\ |F\varphi | \le q(\varphi )\} \); it contains \(0\) and is monotone in \(q\).

The \(n\)-th Hermite coefficient \(\varphi \mapsto \int h_n \varphi \) is a continuous linear functional on \(\mathcal{S}(\mathbb {R},\mathbb {R})\), and the level-\(r\) Hermite–Sobolev seminorm is \(\| \varphi \| _r = \bigl(\sum _n (n+1)^{2r} \langle h_n, \varphi \rangle ^2\bigr)^{1/2}\); the defining series is summable because coefficient decay \(|\langle h_n, \varphi \rangle | \lesssim (n+1)^{-r}\) at every order follows from powers of the oscillator via the eigenrelation and self-adjointness. The same quantity is packaged as a bundled Seminorm by factoring through the weighted coefficient map into \(\ell ^2\).

The finite-\(n\) table of eq. (eq:nrates) with \(\beta _n = q^{1-2n}+q^{2n-1}\), \(\sigma _n = (q^{n-1}-q^{1-n})^2\), encoded through the real parameter \(r = q^n\) (so every real \(r\), not only integer \(n\), is covered).

The two-species interacting particle system on \(\mathbb Z\) with states \(\{ 0,1,2,3\} \) per site and the \(n=\infty \) jump-rate table of eq. (eq:rates): hops at rates \(1, q^2\), pair moves at \(1, q^4\), swap at \(q^2\), merge at \(1-q^2\), split at \(q^2(1-q^2)\).

\(\operatorname {aldousQ}(P,X,\mathcal{F},d,e)\) is the supremum, over real-valued \(\mathcal{F}\)-stopping times \(\tau \le 1\) and deterministic shifts \(0\le \delta \le d\), of \(P\{ \, e\le |X_{\min (\tau +\delta ,1)}-X_\tau |\, \} \), valued in \([0,\infty ]\). Note the truncation: the shifted time is \(\min (\tau +\delta ,1)\), so the increment never looks past the horizon (for Skoro-valued processes this is consistent with the flat-right encoding). The quantity is monotone in the shift budget \(d\), and any single admissible pair \((\tau ,\delta )\) bounds it from below (le_aldousQ_of_stoppingTime).

For \(f,g\colon \mathbb {R}\to \mathbb {R}\), \(\operatorname {supDiff}(f,g)\) is the supremum of \(|f(t)-g(t)|\) over \(t\in [0,1]\). Billingsley’s metric is \(d^\circ (f,g)=\inf _{\lambda }\max \bigl(\| \lambda \| ^\circ ,\; \operatorname {supDiff}(f\circ \lambda ,\, g)\bigr)\), the infimum running over time changes \(\lambda \) of finite log-slope norm. This is the \(J_1\)-metric whose Cauchy sequences are well behaved (unlike the more elementary \(J_1\) metric with \(\sup _t|\lambda t-t|\) in place of \(\| \lambda \| ^\circ \)).

Billingsley’s modulus \(w'_f(\delta )\) is formalized as the infimum of all \(\varepsilon \ge 0\) admitting a finite partition \(0=t_0{\lt}t_1{\lt}\dots {\lt}t_n=1\) whose cells all have length \({\gt}\delta \) and on each of whose half-open cells \([t_i,t_{i+1})\) the oscillation from the left endpoint value satisfies \(|f(x)-f(t_i)|\le \varepsilon \). Note the nonstandard every-cell convention: every cell (not all but the last) must be longer than \(\delta \); this is harmless for the \(\delta \to 0\) limit, since any finite partition is \(\delta \)-sparse for \(\delta \) below its minimal gap. The modulus is nonnegative and monotone in \(\delta \).

A function \(f\colon \mathbb {R}\to \mathbb {R}\) is càdlàg on \([0,1]\) if it is right-continuous at every \(t\in [0,1)\) and has a left limit at every \(t\in (0,1]\). The Skorokhod space is formalized as the structure Skoro: an honest function on all of \(\mathbb {R}\) that is càdlàg on \([0,1]\), carries an explicit boundedness witness on \([0,1]\) (automatic for càdlàg paths, but bundled so the sups in the metric are genuine reals), and is flat outside \([0,1]\) — constant \(=f(0)\) on \((-\infty ,0]\) and constant \(=f(1)\) on \([1,\infty )\). The flat encoding keeps the usual topology of \(\mathbb {R}\) on the source and makes \(d^\circ (f,g)=0\) imply equality on the nose, so no quotient is needed.

\(\operatorname {supNorm} f\) is the supremum of \(|f(t)|\) over \(t\in [0,1]\) (defined as \(\operatorname {supDiff}(f,0)\)). It is \(1\)-Lipschitz for \(d^\circ \) (\(|\operatorname {supNorm} f-\operatorname {supNorm} g|\le d^\circ (f,g)\), because a time change permutes the values on \([0,1]\)), hence continuous and Borel measurable. This is the functional through which uniform boundedness enters the tightness criteria.

A time change is a structure bundling a map \(\lambda \colon \mathbb {R}\to \mathbb {R}\) that on \([0,1]\) is a strictly increasing continuous bijection fixing \(0\) and \(1\), and is flat outside \([0,1]\) (matching the path encoding of Definition 6.1). Its log-slope norm \(\| \lambda \| ^\circ \) is the supremum of \(\bigl|\log \frac{\lambda t-\lambda s}{t-s}\bigr|\) over \(0\le s{\lt}t\le 1\), and FiniteNorm records that this set of log-slopes is bounded above (the class \(\Lambda ^\circ \)). Composition TimeChange.comp and the inverse TimeChange.symm (via Set.invFunOn) are provided in place of a literal group instance.

The same-species two-particle dual kernel obeys \(p_t(\xi ,\xi ') \le C(q)/(1+t)\). Now unconditional: the kernel is synthesised as the Schütz reflection series asepKernel q := Bethe.asepReflect 1 q^2, and the bound follows from TypeDDecoupling.Bethe.asepReflect_decay with no extra hypothesis.

The exclusion contact condition forces the reflection amplitude \(S = -\frac{r_R-(r_R+r_L)z_2+r_Lz_1z_2}{r_R-(r_R+r_L)z_1+r_Lz_1z_2}\); the geometric reflection series (ratio \(\rho = r_L/r_R\)) satisfies the free equation off contact, the boundary identity, and decays like \(C/(1+t)\).

The joint \(q\)-Laplace observable from the block equals the dual pair’s hitting probability on \(\mathbb Z\), with boundary constant \(k=0\). Sorry-free via the documented continuity hypothesis hcont; the finite-\(L\) core and the limit mechanism are proved.

The identity holds on every finite lattice, by matrix-exponential intertwining and exact block evaluation (modulo its named two-particle interlacing hypothesis).

\(M^f_t = f(\eta _t)-f(\eta _0)-\int _0^t Lf(\eta _s)ds\) is a martingale against Mathlib’s \(\mathbb R\)-indexed Martingale (core TypeDDecoupling.dynkin_martingale, from a faithful Markov–Feller bundle), the bracket is definitionally the carré-du-champ time integral (dynkinBracketDef; the identification with the predictable bracket is the cited Ethier–Kurtz Ch. 4 fact), and the integrated covariance identity \(\mathbb E[M^f_tM^g_t] = \mathbb E\int _0^t \Gamma (f,g)(\eta _s)ds\) is proved (core TypeDDecoupling.dynkin_L2). The former opaque predicates are retired.

\(\| V_z^{(\mathrm{dr})}\| ^2_{L^2(\varpi )} \le \varepsilon _N = (q_N^{-4|\Lambda |}-1)^2 = O(N^{-2}) \to 0\), uniformly over \(z\) in the field window, via the exact identity \(A_z = q^{-2(L_1+L_2)}V_z\) and the projection inequality (core TypeDDecoupling.DressedMass.dressedMass_bond_le); the dressed mass is realised concretely on the regime-A window with \(q_N = 1-1/(N+2)^2\).

The finite-\(N\) ground truth making the bracket hypothesis of 3.13 faithful for the stationary single-species WASEP under the Bernoulli(\(\rho \)) product weight: exact equilibrium mean \(2\chi D\| \varphi '\| ^2\) with \(D = (1+q^2)/2\), variance \(O(1/N)\), and \(L^2\) concentration of the time-integrated bracket under stationarity.

With \(\Theta ^N = N^{-1}\sum _x \varphi '(x/N)^2 V_x\): \(\mathbb E_\nu [(\Theta ^N)^2] \le C(\varphi )N^{-1}\), via the exact cancellation \(\mathbb E[V_xV_y]=0\) for \(|x-y|\ge 2\) and \(|V|\le 1\) (EqvarOrth.expect_sq_le). The boundedness hypothesis on \(\varphi '\) is genuinely needed (the bare statement over arbitrary coefficients is false).

Each single-species fluctuation field converges to the Gaussian OU/EW field with diagonal bracket \(2\chi Dt\| \partial \varphi \| ^2\), \(\chi = \rho (1-\rho )\). Proved outright as the single-field case of 3.12 (same faithful hypotheses); the Dittrich–Gärtner reference is demoted to a classical-instantiation citation.

From the de-opaqued bracket condition mpConvBracket — per test function \(\varphi \) and time \(t\), a martingale-difference array with deterministic bracket \(2\chi Dt\, \sigma (\varphi )\) and a stopped/truncated companion — the pairing characteristic function of \(Z_t^N\) converges to the centered Gaussian \(\exp (-(2\chi Dt\, \sigma (\varphi ))u^2/2)\); via the stopped-array adapter and the project’s own martingale CLT.

For a driftless, finite-range, reversible walk on \(\mathbb Z\) with measure bounds \(c_1 \le m \le c_2\), exit rate \(\le \Lambda \) and nearest-neighbour conductance \(\ge \delta {\gt} 0\): \(\sup _r \mathbb P(X_t = r) \le C/\sqrt{1+t}\) with \(C = C(c_1,c_2,\delta ,\Lambda ,\varrho )\) explicit. Carries the faithful a-priori hypothesis \(p \le 1\); the full Nash/CKS argument runs on the exponential semigroup (TypeDDecouplingCKS.free_bound), with \(p\) identified with the semigroup kernel by a weighted-\(\ell ^1\) Grönwall uniqueness argument.

For independent integer-valued \(Y_1,\dots ,Y_n\): \(\sup _x \mathbb P(\sum _j Y_j = x) \le C\big(\sum _j(1-\mathcal Q(Y_j))\big)^{-1/2}\) with universal \(C\). Proved from scratch (lattice Esseen + product-over-gaps), core TypeDDecoupling.KR.KR_abstract.

The vectors \(e^r_j = (j+1)^{-r}\, h_j\) form the \(\| \cdot \| _r\)-orthonormal system, and \(\| e^r_j\| _q = (j+1)^{q-r}\). Whenever \(q + 1 \le r\), the squares are summable: \(\sum _j \| e^r_j\| _q^2 = \sum _j (j+1)^{2(q-r)} {\lt} \infty \). This is the nuclearity input (the inclusion between consecutive levels of the chain is Hilbert–Schmidt) consumed by the Gaussian-averaging step of Mitoma’s argument.

Let \(M : \mathcal{S}(\mathbb {R},\mathbb {R}) \to \mathbb {R}\) be nonnegative, even, subadditive and lower semicontinuous, with \(M(n^{-1}\varphi ) \to 0\) as \(n \to \infty \) for every fixed \(\varphi \). Then \(M\) is continuous at \(0\). The proof is a Baire-category argument on the Fréchet space \(\mathcal{S}\): the closed sets \(\{ \varphi \mid \forall m \ge k,\ M(m^{-1}\varphi ) \le \varepsilon \} \) cover the space, so one has nonempty interior, and subadditivity converts this into a neighborhood of \(0\) on which \(M\) is small.

The 1D Agmon bound, the discrete Nash inequality \(\| f\| _2^6 \le 4\| f\| _1^4\| \nabla f\| _2^2\), the ODE iteration \(u' \le -\kappa u^3 \Rightarrow u \le 1/\sqrt{2\kappa t}\), and the pointwise assembly.

\(\langle V_x, \eta _{i,y}-\rho _i\rangle = 0\) for every species \(i\) and sites \(x,y\): \(V_x\) has no order-one component, its lowest order being two. Proved by the general involution argument EqvarOrth.expect_V_mul_occ_eq_zero (swapping the other species across the bond reverses the sign of \(V_x\) while fixing the blocking weight), realised concretely as the covariance ewCrossDensityCov over a finite blocking-measure window.

For the relative walk with sticky origin (split rate \(\nu _{\mathrm{sp}} = 2q^2(1-q^2)\), merge rate \(1-q^2\)), uniformly over \(q \in [q_0,1)\) in the window \(\nu _{\mathrm{sp}} t \le K\): \(\mathbb P(R_t = r) \le C(K,q_0)/\sqrt{1+t} + \delta _{r,0}e^{-\nu _{\mathrm{sp}}t}\). Sorry-free: the excursion/renewal representation enters as the single documented hypothesis bundle hrenew (occupation, zero-decomposition, renewal integral); all convolution assemblies and the \(q\)-uniform constant are proved.

With \(\beta _i = \alpha _i/(1+\alpha _i)\): the blocking measure and the reweighted measure have the same sector conditionals, uniformly comparable sector masses (\(\log M \le 2C_0\), \(C_0 = A(1+\tfrac {8\beta }{1-\beta })\), \(A = 18cK^2\) under the regime-A scaling), and the correlation transfer inequality holds. Replaces a FALSE original (the uncompensated comparison has \(M = e^{\Theta (N)}\)); cores TypeDDecoupling.Sector.sector_comparison_single, TypeDDecoupling.Sector.correlation_transfer.

The forward generator of a finite-range walk with bounded exit rates is a bounded operator on \(\ell ^1(\mathbb Z)\) (\(\| A\| \le 2\Lambda \)); its exponential semigroup satisfies positivity, mass conservation, Chapman–Kolmogorov, reversibility, and the energy identity \(u' = -2\mathcal E\) (continued in the CKS files).

For finite-norm time changes one has \(\| \lambda ^{-1}\| ^\circ =\| \lambda \| ^\circ \) and \(\| \lambda \circ \mu \| ^\circ \le \| \lambda \| ^\circ +\| \mu \| ^\circ \), together with the closure facts that inverses and compositions of finite-norm time changes again have finite norm. These are exactly the two norm identities needed for the symmetry and triangle inequality of \(d^\circ \), and (via timeChange_dist_id_le) the bound \(|\lambda t-t|\le e^{\| \lambda \| ^\circ }-1\) used throughout.

For every càdlàg \(f\) and \(\varepsilon {\gt}0\) there is a finite partition \(0=t_0{\lt}\dots {\lt}t_n=1\) with left-endpoint oscillation \({\lt}\varepsilon \) on every cell (a greedy left-to-right construction; termination uses the existence of left limits). As a consequence, for càdlàg \(f\) the modulus satisfies \(w'_f(\delta )\to 0\) as \(\delta \to 0^+\). This is the technical primitive behind separability, compactness, and the measurability of paths.

Conditionally on the unsigned skeleton, the sum coordinate’s largest atom is \(\le C(\delta )/\sqrt{1+M}\); the ambiguous-jump count dominates a Poisson and \(\mathbb P(M {\lt} t/2) \le e^{-ct}\) with \(c = (1-\log 2)/2\). (Statement strengthened: universal constant.)

For the recurrent reversible walk agreeing off a finite set with the symmetric rate-\(a\) walk: \(\tau _r(s) \sim m(r)\sqrt{s/(\pi a)}\).

\(\mathbb E_\nu [\langle M_1^N,M_2^N\rangle (\varphi ,t)^2] \le C(\varphi ,c)\, t\, (N^{-1} + N^{-2}\log _+(tN^2) + t\, \varepsilon _N) \to 0\) (condition (X)). Sorry-free from the abstract estimate TypeDDecoupling.Conc.conc_master; the process-level inputs (transfer bound, mass-sector kernel split, equal-time bound, stationarity identity) enter as the named hypothesis hproc. The truncated \(\log _+\) is a fidelity repair: the bare \(\log \) would be false for small \(t\).

Under the blocking measure the cross mobility and cross compressibility vanish identically in the fugacities: \(\mathbb E_\nu [V_x] = 0\) and \(\mathrm{Cov}_\nu (\eta _{1,x},\eta _{2,y}) = 0\).

At every \(n\) (and every real \(q^n\)), each species’ marginal current is that of an autonomous single-species ASEP: the species-\(1\) transfer rates are independent of the species-\(2\) occupancy, with the \(n\)-dependence a pure time change \(\beta _n\).

\(\Gamma _i^N(\varphi ,\cdot ) \to D\, Y_i(\Delta \varphi ,\cdot )\) in \(L^2\) (condition (D)). Quantitative cores proved outright: summation-by-parts + Taylor (TypeDDecoupling.Drift.drift_sbp_bound) and the correction second moment (TypeDDecoupling.Drift.corr_second_moment); the \(\mathcal S'(\mathbb R)\) wrapper enters as the hypothesis hpin.

Restated as a genuine theorem over probability spaces (no longer a citation): a family \((X_i)\) of \(D([0,1];\mathbb R)\)-valued random elements on probability spaces \((\Omega _i, P_i)\), each adapted to a right-continuous filtration, whose laws are (i) uniformly bounded in sup-norm in probability and (ii) satisfy the Aldous stopping-time condition (\(\alpha _i(\delta ,\varepsilon ) \to 0\) uniformly in \(i\)), has tight pushforward laws on the Skorokhod space (IsTightMeasureSet). Proved by direct application of SkorokhodBasic.aldous_tightness (6.15).

For all densities \(\rho _1,\rho _2 \in (0,1)\), \(\langle W_{i,x}, B_z\rangle = 0\) for every \(z\), where \(B_z = (\eta _{1,z}-\rho _1)(\eta _{2,z}-\rho _2)\). Proved from the equilibrium product (independence) structure of the blocking measure (the EWModel structure): the species-\(i\) current depends only on species-\(i\) occupations, so it factorizes against the opposite-species centred field, whose mean vanishes.

For a continuous seminorm \(q\) and a dense set \(D\), membership \(F \in \mathrm{polarBall}(q)\) is equivalent to the bound \(|F\varphi | \le q(\varphi )\) holding for \(\varphi \in D\) only. Specialized to the named countable dense set \(\mathcal{D}\), the confinement event becomes a countable intersection of evaluation events, which is the measurability input for the probabilistic core.

The special seminorms \(\mathrm{ratSeminorm}(c, s) = c \cdot \sup _{(k,n) \in s} p_{k,n}\), indexed by \(c \in \mathbb {R}_{\ge 0}\) and finite sets \(s \subseteq \mathbb {N} \times \mathbb {N}\), are continuous, and their polar balls form a cofinal family: every pointwise-bounded family \((\mathcal{F}_i)\) in the dual is contained in a single compact polar ball \(\mathrm{polarBall}(\mathrm{ratSeminorm}(c,s))\). This combines the Banach–Steinhaus dominating-seminorm corollary with the characterization of continuous seminorms on a space with seminorms.

\(\mathrm{Corr}(G_1^+,G_2^+) = \frac{\pi }{8(\pi -1)c}[1-2e^{-4c}+I_0(4c)-L_0(4c)]\), with besselI0/struveL0 as explicit power series.

\((X_1,X_2)(T)/\sqrt{2T}\) converges to the mixture law with \(U \sim \min (\mathrm{Exp}(4c),1)\). Sorry-free via the documented process-level hypothesis bundle htwo.

\(\mathrm{Corr}(X_1,X_2) \to \rho (c) = (1-e^{-4c})/(4c)\), with monotonicity, the \(c\to 0\) and \(c\to \infty \) limits, and the \(1/(4c)\) tail.

The exact contact representation: \(\mathbb E[q^{2N_i}]\) and \(\mathrm{Cov}(q^{2N_1},q^{2N_2})\) as absolutely convergent dual sums, the covariance generated entirely by contact.

The \(n=\infty \) type D ASEP is self-dual with respect to the orthogonal \(q\)-Krawtchouk product duality; the \(\alpha \to 0\) coefficient extraction yields the bounded triangular duality \(D^{\mathrm{tri}}\). (Sorry-free assembly from the cited CFG20/REU interlacing inputs, stated in TypeDDecouplingDuality.lean.)

If, for every \(\varphi \in \mathcal S(\mathbb R)\), the path processes \(t\mapsto \langle Z_N(t),\varphi \rangle \) have tight laws on \(D([0,1];\mathbb R)\), then for every \(\eta {\gt}0\) the processes are confined, uniformly in \(N\) and with probability \(\ge 1-\eta \), in a single compact polar ball of the pointwise dual \(\mathcal S'(\mathbb R)\) (Kallianpur–Xiong compact-confinement form of Mitoma’s theorem; the classical iff against a topology on \(D([0,1];\mathcal S')\) is deliberately not formalized). Proved from the Hermite–Sobolev nuclear chain and the uniform confinement theorem; formerly the project’s one remaining citation sorry, now discharged (fidelity-repair note in the Lean docstring).

A process whose Dynkin drift converges to \(DZ(\Delta \varphi )\) (mpConvDrift), whose bracket converges to \(2\chi Dt\| \partial \varphi \| ^2\) (mpConvBracket), and which is Mitoma-tight, converges in law to the stationary OU solution. The Gaussian/uniqueness core is proved from 3.11; only the path-space existence/convergence content enters as the single documented bundle MPPathBundle (riding on the Mitoma/Aldous leaves and the heat-semigroup identification). Sorry-free.

Under \(q = 1-c/N^2\) the rescaled density-fluctuation pair is tight in \(D([0,T];\mathcal S'(\mathbb R))\) and converges to two independent stationary Edwards–Wilkinson (OU) fields, at arbitrary densities; the limiting cross bracket vanishes (condition (X)) and the corrected sector comparison holds. Rewired to two real-tightness hypotheses \(ht_1, ht_2\) (component tightness of the evaluated processes — exactly what 3.10 produces), fed through 3.9 for the \(\mathcal S'\)-tightness; the OU limits come from 3.12 and 3.13, the decoupling from 3.5, 3.6 and 3.4. The declaration itself is sorry-free; it inherits the project’s single remaining citation sorry transitively through its use of 3.9.

If \(\omega (\lambda ) = \int _0^\infty e^{-\lambda t}p(t)\, dt \sim c\lambda ^{-\rho }\) as \(\lambda \downarrow 0\) with \(p \ge 0\), then \(\int _0^s p \sim c\, s^\rho /\Gamma (\rho +1)\) as \(s \to \infty \). (Tauberian direction, general \(\rho {\gt} 0\); core TypeDDecouplingKaramata.tauberian_isEquivalent.)

The type D two-particle dual kernel obeys \(p_u(\xi ,\xi ') \le C[(1+u)^{-1} + e^{-\nu _{\mathrm{sp}}u}(1+u)^{-1/2}]\). Sorry-free assembly: the kernel is factored through sum/relative marginals (hypothesis hfact), whose bounds are the cited inputs 2.6/2.4.

Pointwise convergence of characteristic functions to that of a given probability measure implies weak convergence (identified-limit form), in one and two dimensions. (Mathlib master has since gained LevyConvergence.lean, post-dating this project’s pin — ours remains load-bearing at the pin.)

For every \(n\) and each species the standardized current converges to \(F_2\). Sorry-free; reduces to the cited single-species step-ASEP input (carried as a hypothesis) via 1.3.

A martingale difference array with deterministic vanishing jump bound and bracket \(\to \sigma ^2\) has \(\mathbb E[e^{iuS_n}] \to e^{-u^2\sigma ^2/2}\), hence converges in law to \(N(0,\sigma ^2)\) (TypeDDecoupling.Levy.mcleish_clt_unconditional discharges the Lévy hypothesis).

If a family \((\mathcal{F}_i)_{i \in \iota }\) of continuous linear functionals on \(\mathcal{S}(\mathbb {R},\mathbb {R})\) is pointwise bounded (for each \(\varphi \) there is \(C\) with \(|\mathcal{F}_i \varphi | \le C\) for all \(i\)), then there is a single continuous seminorm \(q\) with \(|\mathcal{F}_i \varphi | \le q(\varphi )\) for all \(i\) and \(\varphi \). This is Banach–Steinhaus in dominating-seminorm form, available because \(\mathcal{S}\) is barrelled. As a companion, a countable pointwise supremum \(\varphi \mapsto \sup _i |\mathcal{F}_i \varphi |\) whose seminorm family is bounded above is itself continuous.

Setting: a countable nonempty time set \(T\), probability spaces \((\Omega _i, P_i)_{i \in \iota }\), and measurable dual-valued processes \(Z_i : T \to \Omega _i \to \mathrm{SchDual}\), under hypothesis (H): for every test function \(\varphi \) and \(\varepsilon {\gt} 0\) there is \(a {\gt} 0\) with \(P_i\{ \omega \mid \exists t,\ a {\lt} |Z_i(t,\omega )\varphi |\} \le \varepsilon \) uniformly in \(i\). Then for every \(\varepsilon {\gt} 0\) there are \(q \in \mathbb {N}\) and \(\delta {\gt} 0\) such that \(\sup _i \int \sup _t \bigl\| 1 - e^{i\, Z_i(t,\omega )\varphi }\bigr\| \, dP_i(\omega ) \le \varepsilon + 2\, \| \varphi \| _q^2/\delta ^2\) for all \(\varphi \). The proof applies Xia’s lemma to the functional \(M(\varphi ) = \sup _i \int \sup _t \frac{|Z\varphi |}{1+|Z\varphi |}\, dP_i\) and converts the resulting Schwartz neighborhood into a Hermite–Sobolev ball via the two-sided domination.

Under the measurability hypothesis and the per-test-function uniform sup-tightness hypothesis (H), for every \(\eta {\gt} 0\) there are \(q \in \mathbb {N}\) and \(B {\gt} 0\) such that the polar ball \(K = \mathrm{polarBall}\bigl(B \cdot \| \cdot \| _{q+1}\bigr)\) is compact in the pointwise dual, and for every \(i\), \(P_i\bigl\{ \omega \, \big|\, \exists t \in T,\ Z_i(t,\omega ) \notin K\bigr\} \le \eta \). That is, the processes stay in one fixed compact dual ball, uniformly over the countable time set and uniformly in \(i\), with probability at least \(1-\eta \). The proof chooses \(C\) large in the Gaussian-averaging bound and identifies bounded coefficient partial sums with polar-ball membership. This is the uniform dual-ball confinement at the heart of Mitoma’s tightness criterion for \(\mathcal{S}'\)-valued processes.

For real normed spaces \(E\), \(F\), the uniformity of Mathlib’s canonical Schwartz space \(\mathcal{S}(E,F)\) is countably generated, coming from the \(\mathbb {N}\times \mathbb {N}\)-indexed seminorm family \(p_{k,n}(\varphi ) = \sup _x \| x\| ^k \| D^n\varphi (x)\| \). When \(F\) is complete, \(\mathcal{S}(E,F)\) is a complete space for this uniformity: the analytic heart is that a sequence of \(C^\infty \) functions converging pointwise, with all iterated derivatives converging uniformly, has a \(C^\infty \) limit whose iterated derivatives are those uniform limits. Via Mathlib’s metrization of countably generated uniformities, the Baire and barrelled-space instances follow, all attached to the canonical topology with no re-metrization.

Under the same measurability hypothesis and hypothesis (H): for every \(\varepsilon {\gt} 0\) there are \(q\) and \(\delta {\gt} 0\) such that for all \(C {\gt} 0\) and all \(i\), \(P_i\bigl\{ \omega \, \big|\, \exists t\, \exists N,\ C^2 {\lt} \sum _{j {\lt} N} \langle Z_i(t,\omega ), e^{q+1}_j\rangle ^2 \bigr\} \le \kappa \bigl(\varepsilon + \tfrac {2}{\delta ^2} \cdot \tfrac {S_{q,q+1}}{C^2}\bigr)\), where \(\kappa = \sqrt{e}/(\sqrt{e}-1)\) is the Badrikian constant and \(S_{q,q+1} = \sum _j \| e^{q+1}_j\| _q^2\) is the (finite) Hilbert–Schmidt constant. The proof averages the characteristic-functional bound over finite-dimensional Gaussian test functions \(\varphi _y = \sum _{j{\lt}N} y_j e^{q+1}_j\) with \(y \sim \mathcal{N}(0, C^{-2})^{\otimes N}\) and uses a Badrikian-type indicator estimate.

Any \(f \in L^2(\mathbb {R})\) with \(\langle h_n, f\rangle = 0\) for all \(n\) is zero. The analytic heart is Fourier-based: orthogonality to all \(h_n\) kills all moments of \(g = f \cdot e^{-x^2/4}\), hence (by dominated expansion of the Fourier kernel into its power series) \(\widehat{g} \equiv 0\), and \(L^1\)-Fourier injectivity gives \(g = 0\) a.e. Together with orthonormality this packages the Hermite functions as a HilbertBasis \(\mathbb {N} \to L^2(\mathbb {R})\), with the usual Fourier–Hermite expansion and Parseval identity.

For a continuous seminorm \(q\), the polar ball \(\mathrm{polarBall}(q)\) is compact in the pointwise topology. The proof pushes through the embedding of \(\mathrm{SchDual}\) into the product space \(\mathcal{S}(\mathbb {R},\mathbb {R}) \to \mathbb {R}\): the image is the intersection of the closed coordinatewise linearity conditions with the pointwise bound, inside the Tychonoff-compact box \(\prod _\varphi [-q(\varphi ), q(\varphi )]\), and a pointwise limit obeying the bound is automatically continuous because it is dominated by the continuous seminorm \(q\). No Ascoli-type argument is needed.

The weighted-derivative maps \(\varphi \mapsto (x \mapsto |x|^k \, \varphi ^{(n)}(x))\) land in \(C_0(\mathbb {R},\mathbb {R})\) by Schwartz decay, realize the Schwartz seminorms as sup-norms, and jointly give a linear topological embedding of \(\mathcal{S}(\mathbb {R},\mathbb {R})\) into the countable product \(\prod _{(k,n)} C_0(\mathbb {R},\mathbb {R})\). The space \(C_0(\mathbb {R},\mathbb {R})\) is separable (via an isometric embedding into \(C(\mathbb {R}^+,\mathbb {R})\) on the one-point compactification, which is second countable), so the product is second countable and second countability transfers back along the embedding. Combined with the countably generated uniformity, \(\mathcal{S}(\mathbb {R},\mathbb {R})\) is separable and second countable on its canonical topology.

Each Hermite–Sobolev seminorm is continuous for the canonical Schwartz topology: for every \(r\) there are \(C \ge 0\) and a finite set \(s\) of indices with \(\| \varphi \| _r \le C \cdot \sup _{(k,n) \in s} p_{k,n}(\varphi )\). Conversely, every canonical Schwartz seminorm is dominated by a single Hermite–Sobolev level: \(p_{k,m}(\varphi ) \le C\, \| \varphi \| _r\) for some \(C \ge 0\) and \(r\) (obtained by trading powers of \(x\) and derivatives against oscillator powers). Hence the countable Hilbertian chain \((\| \cdot \| _r)_{r \in \mathbb {N}}\) generates the Schwartz topology.

Let \((X_i)_{i\in \iota }\) be \(D\)-valued measurable random elements on probability spaces \((\Omega _i,P_i)\), each adapted to a right-continuous filtration \(\mathcal{F}_i\). Assume (i) uniform sup-norm tightness: for every \(\eta {\gt}0\) there is \(a\) with \(P_i\{ a\le \operatorname {supNorm}X_i\} \le \eta \) for all \(i\); and (ii) the Aldous condition: for all \(\varepsilon ,\eta {\gt}0\) there is \(\delta {\gt}0\) with \(\alpha _i(\delta ,\varepsilon )\le \eta \) uniformly in \(i\). Then the family of laws \(\{ (P_i)_*X_i\} \) is tight on \(D\). The proof is Aldous’s genuine two-scale argument (Billingsley (16.24)ff): the measurable witness superset for the modulus level sets is an interior bad set of close consecutive crossings plus a boundary shift-average detector, whose masses are controlled by \(\alpha \) at two scales via a raw interval Lebesgue average over the shift; a single-scale variant was refuted by counterexample during formalization.

Second-moment form of the criterion: if, uniformly over the family, over stopping times \(\tau \le 1\) and shifts \(0\le \delta \le d\), the truncated increments satisfy \(\mathbb {E}\bigl[(X_{\min (\tau +\delta ,1)}-X_\tau )^2\bigr]\le M(d)\) with \(M(d)\to 0\) as \(d\to 0^+\) (plus a.e.-measurability of the increments and the uniform sup-norm bound), then the laws are tight on \(D\). It combines Chebyshev’s inequality inside the Aldous supremum (aldousQ_le_of_second_moment) with Theorem 6.15.

Let \(A\subseteq D\) be uniformly bounded (\(|f(t)|\le M\) for all \(f\in A\), \(t\in [0,1]\)) and have uniformly decaying modulus: for every \(\varepsilon {\gt}0\) there is \(\delta \in (0,1)\) with \(w'_f(\delta ){\lt}\varepsilon \) for all \(f\in A\). Then \(A\) is totally bounded (an explicit finite net of rational step functions is constructed), and hence, by completeness, \(\overline{A}\) is compact. Only the sufficiency direction of Billingsley’s Theorem 12.3 is formalized; it is the direction consumed by tightness.

For a process \(X\) and \(s,\varepsilon \), \(\operatorname {crossTime}(X,s,\varepsilon )\) is the first time \(t{\gt}s\) with \(|X_t-X_s|{\gt}\varepsilon \), valued in \(\mathbb {R}\cup \{ \top \} \) (\(\top \) if no crossing occurs); for a right-continuous adapted process it is a stopping time of the right-continuous augmentation \(\mathcal{F}^+\) of the filtration. The iterated crossing sequence of a path \(f\in D\) is \(\operatorname {crossSeq}(\varepsilon ,f)_0=0\) and \(\operatorname {crossSeq}(\varepsilon ,f)_{k+1}=\min (\operatorname {crossTime}(\dots )\! \downharpoonright _1,1)\), clamped to \([0,1]\) and set to \(1\) when no further crossing exists. For a measurable \(D\)-valued random element adapted to a right-continuous filtration (\(\mathcal{F}^+=\mathcal{F}\)), every \(\operatorname {crossSeq}\) iterate is an \(\mathcal{F}\)-stopping time; this is the supply of stopping times fed into Aldous’s criterion.

Every coordinate evaluation \(f\mapsto f(t)\) is Borel measurable on \(D\), although it is continuous only at paths continuous at \(t\): the proof exhibits \(f(t)\) as the pointwise limit of the integral averages \(\operatorname {intAvg}_n(t,f)=(n{+}1)\int _t^{t+1/(n+1)}f\), which are \(d^\circ \)-continuous by dominated convergence along Skorokhod time changes. Consequently the rational-coordinate map \(\operatorname {evalRat}\colon D\to (\mathbb {Q}\to \mathbb {R})\) is an injective measurable map between standard Borel spaces, hence a measurable embedding: the Borel \(\sigma \)-algebra of \(D\) coincides with the cylinder \(\sigma \)-algebra. The bridge lemma follows: \(X\colon \Omega \to D\) is measurable iff every coordinate \(\omega \mapsto X(\omega )(t)\) is measurable, and laws on \(D\) are determined by their rational finite-dimensional distributions (ext_of_map_evalRat). (The modulus \(f\mapsto w'_f(\delta )\) itself is not proved measurable — the intended statement survives only inside a comment block — and, by design, nothing below needs it.)

\(d^\circ \) is symmetric, satisfies the triangle inequality (via the composition bound on log-slope norms), and separates points: \(d^\circ (f,g)=0\) forces \(f=g\) as elements of Skoro (agreement first at continuity points and at the endpoints, then everywhere on \([0,1]\) by right-density of continuity points and right-continuity, then on all of \(\mathbb {R}\) by flatness). This yields a genuine MetricSpace instance on Skoro, with no quotient construction.

Every rapidly Cauchy sequence (\(d^\circ (u_k,u_{k+1}){\lt}2^{-k}\)) converges: this is Billingsley’s Theorem 12.2 via the \(\sigma _\infty \) infinite-composition argument, in which the composed time changes converge (geometric log-slope control) and the time-changed paths converge uniformly. Combined with separability — the countable dense family of step functions with rational cut points and rational values, produced from the partition lemma and a piecewise-linear time-change alignment — this makes \(D([0,1],\mathbb {R})\) a complete separable metric space, and the CompleteSpace, SecondCountableTopology and PolishSpace instances are installed.

Let \(S\) be a set of measures on \(D\) such that (i) for every \(\eta {\gt}0\) there is \(a\) with \(\mu \{ f: a\le \operatorname {supNorm} f\} \le \eta \) for all \(\mu \in S\), and (ii) for all \(\varepsilon {\gt}0\) and \(\eta {\gt}0\) there is \(\delta \in (0,1)\) with \(\mu \{ f:\varepsilon \le w'_f(\delta )\} \le \eta \) for all \(\mu \in S\). Then \(S\) is tight (IsTightMeasureSet), with compact sets supplied by Theorem 6.9. Notably, no measurability of the sup-norm or modulus level sets is used — only monotonicity and countable subadditivity of measures — so downstream applications may bound the (outer) mass of the modulus level sets by that of any measurable superset.

A locked-then-diagonal martingale array with random change point \(M_n/k_n \to U\) converges at the characteristic-function level to the \(U\)-mixture of correlation-\(u\) bivariate normals.