Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual kernel spectral construction

Abstract

Actual integral kernels have complete same-noise spectral series, including nullspace and zero variance.

Theorem 1.1 (Actual kernel pairing).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.integral_operator_pairing (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

For every finite measure and every continuous kernel factory with the actual a.e. integral representation, Fubini identifies the operator pairing with the product-space rank-one pairing. Integrability follows from the two actual L2 classes.

Theorem 1.2 (Kernel identification).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.integral_operator_injective (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

Equality of actual integral operators implies equality of their L2 kernels. The proof consumes the pairing identity and the original rank-one totality supplier; it introduces no identification premise.

Theorem 1.3 (Actual rank-one operator).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.integral_operator_diagonal (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

A diagonal kernel acts by f times inner(f,g) on the original spatial Hilbert space. This consumed helper identifies every finite approximation used to prove compactness.

Theorem 1.4 (Kernel symmetry).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.integral_operator_symmetric (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

The fixed subspace of coordinate swap gives a symmetric actual operator. Swap is an isometry on the same product measure, and the rank-one swap supplier is consumed in the proof.

Theorem 1.5 (Compactness from actual kernels).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.integral_operator_compact (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

Dense finite diagonal-kernel sums map to genuine finite-rank operators. Continuity of the kernel factory and the closedness of compact operators pass compactness to every actual symmetric L2 kernel. Compactness is constructed, not assumed.

Theorem 1.6 (Complete countable eigenfamily).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.integral_operator_eigenbasis (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

Nonzero eigenspaces use the pinned finite-dimensional eigenspace theorem and finite orthonormal bases. Their Hilbert bases and the zero-eigenspace Hilbert basis are assembled using the pinned compact spectral totality theorem. The zero eigenspace is retained. Orthonormality and separability make the resulting family countable, including empty and zero-operator cases.

Theorem 1.7 (Diagonal orthonormality).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.diagonal_orthonormal (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

An orthonormal spatial family gives an orthonormal family of diagonal kernels under the product-measure inner product.

Theorem 1.8 (Complete actual kernel series).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.kernel_hasSum_of_eigenbasis (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

Bessel gives square summability of actual diagonal-kernel coefficients. Its convergent kernel series has the same action on every eigenbasis vector as the original operator. Completeness and kernel-to-operator injectivity identify the limit with the original K. No kernel HasSum is supplied as a premise.

Theorem 1.9 (Consumed same-noise transport).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.same_noise_series_of_kernel_hasSum (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

This conditional transport helper is consumed by actual_same_noise_spectral after kernel HasSum is constructed. It maps the kernel series through the original secondIntegral and derives exact square sum, variance and operator-norm bounds.

Theorem 1.10 (Joint laws of the original W).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.same_noise_finite_joint (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

Every scalar linear combination of the finite coordinates is an evaluation of the same W, almost everywhere. The pinned Gaussian linear-functional characterization yields the finite joint Gaussian law on the same P. No product noise or joint-Gaussian premise is introduced. Empty families and arbitrary old fixed vectors remain in scope.

Theorem 1.11 (Finite row independence).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.same_noise_finite_independence (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

The constructed finite joint law and orthonormal covariance identity give independence on the original P. This consumed helper extends to the countable spectral row by finite restrictions; no independence from old vectors or between rows is claimed.

Theorem 1.12 (Actual same-noise spectral representation).

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/ActualSpectralSeries.actual_same_noise_spectral (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. David Nualart and Giovanni Peccati (2005). Central limit theorems for sequences of multiple stochastic integrals. DOI: 10.1214/009117904000000621. URL: https://arxiv.org/pdf/math/0503598v1.

Commentary.

For every actual symmetric kernel, the construction returns a complete countable orthonormal eigenbasis, the complete kernel HasSum, exact coefficient square sum equal to the kernel norm squared and variance divided by two, coefficient and supremum operator bounds, and the actual infinite L2(P) second-integral series. Its standard Gaussian coordinates are independent within the row and jointly Gaussian with every finite old-vector append under the original W and P. Zero coefficients, nullspace and zero variance are included. Each row may have its own eigenbasis. This result does not assert the original covariance asymptotics, real-filter limit, increment estimates, path tightness, completed-field mixing or full original process goal.

References