Same-noise second integral

Abstract

Symmetric product-space kernels have a unique continuous centered-square integral on the same Gaussian noise.

Theorem 1.1 (Rank-one kernel totality).

$\forall X \in T y p e, S i g ma X \in MeasurableSpace (X), m u \in Measure (X), h f ini t e \in IsFiniteMeasure (m u), \forall k \in Lp (R e a l, 2, prod (m u, m u)), \forall h or t h o g o na l \in (\forall f \in Lp (R e a l, 2, m u), \forall g \in Lp (R e a l, 2, m u), inner (rankOne (m u, f, g), k) = 0), k = 0$

Proof. Machine-checked in Lean as D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.rankOne_total (✓ 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 product-space L2 kernel orthogonal to every actual rank-one class is zero. Rectangle indicators and product-measure uniqueness establish the identification used by the actual integral-operator consumer.

Theorem 1.2 (Rank-one coordinate swap).

$\forall X \in T y p e, S i g ma X \in MeasurableSpace (X), m u \in Measure (X), h f ini t e \in IsFiniteMeasure (m u), \forall f \in Lp (R e a l, 2, m u), \forall g \in Lp (R e a l, 2, m u), kernelFlip (m u, rankOne (m u, f, g)) = rankOne (m u, g, f)$

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

Source. Repository-derived.

Commentary.

Coordinate swap exchanges the factors of the actual product-measure rank-one kernel. The actual integral-operator symmetry proof consumes this identity.

Theorem 1.3 (Original diagonal image).

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

Source. Repository-derived.

Commentary.

The continuous second integral sends each actual diagonal kernel to the centered square of the same original W. The constant vector supplies the centered Y square in the finite-frequency remainder.

Theorem 1.4 (Cosine vector representative).

$\forall m u \in Measure (R e a l), \forall h f ini t e \in IsFiniteMeasure (m u), \forall v \in R e a l, AEEq (coeFn (cosineVector (m u, v)), (x : R e a l \mapsto cos (\frac{pi ( )}{2} \cdot v \cdot x)), m u)$

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

Source. Repository-derived.

Commentary.

For each real frequency v and finite spatial measure, the cosine L2 class equals cos((pi/2)vx) almost everywhere. This statement concerns each fixed frequency.

Theorem 1.5 (Sine vector representative).

$\forall m u \in Measure (R e a l), \forall h f ini t e \in IsFiniteMeasure (m u), \forall v \in R e a l, AEEq (coeFn (sineVector (m u, v)), (x : R e a l \mapsto sin (\frac{pi ( )}{2} \cdot v \cdot x)), m u)$

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

Source. Repository-derived.

Commentary.

For each real frequency v and finite spatial measure, the sine L2 class equals sin((pi/2)vx) almost everywhere. Both trigonometric vectors are inputs to the same real Gaussian isometry.

Theorem 1.6 (Spatial square integral).

$\forall m u \in Measure (R e a l), \forall h f ini t e \in IsFiniteMeasure (m u), \forall f \in Lp (R e a l, 2, m u), norm (f)^{2} = integral ((x : R e a l \mapsto evaluation (f, x)^{2}), m u)$

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

Source. Repository-derived.

Commentary.

The squared norm of each real spatial L2 class is the integral of its representative squared. For the constant class this identifies its squared norm with the actual unnormalized spatial mass.

Theorem 1.7 (Constant vector representative).

$\forall m u \in Measure (R e a l), \forall h f ini t e \in IsFiniteMeasure (m u), AEEq (coeFn (oneVector (m u)), (x : R e a l \mapsto 1), m u)$

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

Source. Repository-derived.

Commentary.

For every finite measure on the real line, the constant L2 vector has representative one almost everywhere. Its diagonal product therefore represents the constant spatial kernel.

Theorem 1.8 (Density in the actual symmetric space).

$\forall X \in T y p e, S i g ma X \in MeasurableSpace (X), m u \in Measure (X), h f ini t e \in IsFiniteMeasure (m u), DenseRange (finiteKernelMap (m u))$

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

Source. Repository-derived.

Commentary.

For every finite measure mu on any measurable space X, the range of the finite diagonal-kernel map is dense in the fixed subspace of coordinate swap in L2(mu times mu). No normalization, positive mass or finite-dimensional restriction is imposed.

A kernel orthogonal to every rank-one class has zero integral on every measurable rectangle. Rectangles generate the product sigma algebra; complements and disjoint countable unions preserve zero integrals. The kernel therefore vanishes almost everywhere. For a symmetric kernel, polarization of diagonal generators and invariance of inner products under swap reduce diagonal orthogonality to rank-one orthogonality. The symmetric subspace is closed and complete.

Theorem 1.9 (Continuous extension and characterization).

$\forall X \in T y p e, S i g ma X \in MeasurableSpace (X), m u \in Measure (X), h f ini t e \in IsFiniteMeasure (m u), O m e g a \in T y p e, S i g ma O m e g a \in MeasurableSpace (O m e g a), P \in Measure (O m e g a), h p ro b \in IsProbabilityMeasure (P), W \in LinearIsometry (R e a l, Lp (R e a l, 2, m u), Lp (R e a l, 2, P)), hW \in (\forall f \in Lp (R e a l, 2, m u), HasLaw (representative (apply (W, f)), gaussianReal (0, toNNReal (norm (f)^{2})), P)), (((\forall k \in symmetricKernel (m u), Integral (P, (o m e g a : O m e g a \mapsto evaluation (apply (secondIntegral (m u, P, W, hW), k), o m e g a))) = 0) \land (\forall k \in symmetricKernel (m u), \forall l \in symmetricKernel (m u), inner (apply (secondIntegral (m u, P, W, hW), k), apply (secondIntegral (m u, P, W, hW), l)) = 2 \cdot inner (k, l))) \land (\forall k \in symmetricKernel (m u), norm (apply (secondIntegral (m u, P, W, hW), k)) = sqrt (2) \cdot norm (k))) \land (\forall J \in ContinuousLinearMap (R e a l, symmetricKernel (m u), Lp (R e a l, 2, P)), (\forall f \in Lp (R e a l, 2, m u), apply (J, diagonalKernel (m u, f)) = centeredSquare (m u, P, W, hW, f)) \Rightarrow J = secondIntegral (m u, P, W, hW))$

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

Source. Repository-derived.

Commentary.

Let P be a probability measure and W a fixed real linear isometry from L2(mu) to L2(P), with each W(f) having centered Gaussian law of variance ||f||^2. The second integral extends the finite coefficient assignment continuously to the full actual symmetric product-space L2 subspace.

Every output has mean zero. For arbitrary symmetric kernels k and l its covariance is 2 inner(k,l), and its norm is sqrt(2)||k||. It is the unique continuous real linear map sending each diagonal kernel f(x)f(y) to the actual class W(f)^2-||f||^2. Density passes the finite Gram identity and mean to the full space. Every random variable uses the original W and P.

Theorem 1.10 (Actual symmetrized products).

$\forall X \in T y p e, S i g ma X \in MeasurableSpace (X), m u \in Measure (X), h f ini t e \in IsFiniteMeasure (m u), O m e g a \in T y p e, S i g ma O m e g a \in MeasurableSpace (O m e g a), P \in Measure (O m e g a), h p ro b \in IsProbabilityMeasure (P), W \in LinearIsometry (R e a l, Lp (R e a l, 2, m u), Lp (R e a l, 2, P)), hW \in (\forall f \in Lp (R e a l, 2, m u), HasLaw (representative (apply (W, f)), gaussianReal (0, toNNReal (norm (f)^{2})), P)), \forall f \in Lp (R e a l, 2, m u), \forall g \in Lp (R e a l, 2, m u), AlmostEverywhere (prod (m u, m u), (z : Prod (X, X) \mapsto evaluation (val (symmetrizedKernel (m u, f, g)), z) = \frac{evaluation ( f , fst ( z ) ) \cdot evaluation ( g , snd ( z ) ) + evaluation ( g , fst ( z ) ) \cdot evaluation ( f , snd ( z ) )}{2})) \land AlmostEverywhere (P, (o m e g a : O m e g a \mapsto evaluation (apply (secondIntegral (m u, P, W, hW), symmetrizedKernel (m u, f, g)), o m e g a) = evaluation (apply (W, f), o m e g a) \cdot evaluation (apply (W, g), o m e g a) - inner (f, g)))$

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

Source. Repository-derived.

Commentary.

For all f and g in L2(mu), symmetrizedKernel(f,g) has the product-measure representative (f(x)g(y)+g(x)f(y))/2. Its second integral has the almost-everywhere representative W(f)W(g)-inner(f,g) on the original probability space. Both conclusions include zero vectors, zero measure and linearly dependent vectors.

Theorem 1.11 (Exact finite Gram identity).

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

Source. Repository-derived.

Commentary.

Let mu be any finite measure, P a probability law, and W a fixed real linear isometry from H=L2(mu) to L2(P). Assume every W(f) has Gaussian law N(0,||f||^2). Spatial measure is not normalized. The rank-one class r(f,g) is represented by f(x)g(y) in L2(mu times mu); the symmetric subspace is the kernel of flip minus identity.

For finite real coefficients c on H, let e(c) be the sum of c(h)r(h,h) and j(c) the sum of c(h)(W(h)^2-||h||^2). Exact scalar fourth moments and the sum-and-difference polarization give the centered-square covariance 2 inner(f,g)^2. Fubini gives the spatial rank-one inner products. Consequently inner(j(c),j(b))=2 inner(e(c),e(b)).

The identity implies ||j(c)||=sqrt(2)||e(c)|| and e(c)=0 implies j(c)=0. Quotienting by the kernel of e therefore defines a bounded real linear map on the actual finite-kernel range. This map uses the given W and P throughout.

Theorem 1.12 (Consumed finite norm bound).

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

Source. Repository-derived.

Commentary.

For each finite coefficient vector c, the same-noise map satisfies ||j(c)|| <= sqrt(2)||e(c)||. This consequence of finiteGram is consumed by finiteSecondIntegral_apply, secondIntegral_apply and GaussianFrequencyKernel.quadraticFrequency_representation. It supplies the boundedness premise for the actual extension and adds no mathematical content credit.

Theorem 1.13 (Actual trigonometric frequency).

$\forall m u \in Measure (R e a l), h f ini t e \in IsFiniteMeasure (m u), O m e g a \in T y p e, S i g ma O m e g a \in MeasurableSpace (O m e g a), P \in Measure (O m e g a), h p ro b \in IsProbabilityMeasure (P), W \in LinearIsometry (R e a l, Lp (R e a l, 2, m u), Lp (R e a l, 2, P)), hW \in (\forall f \in Lp (R e a l, 2, m u), HasLaw (representative (apply (W, f)), gaussianReal (0, toNNReal (norm (f)^{2})), P)), \forall v \in R e a l, AlmostEverywhere (P, (o m e g a : O m e g a \mapsto evaluation (finiteSecondIntegral (m u, P, W, hW), frequencyKernel (m u, v), o m e g a) = evaluation (W, cosineVector (m u, v), o m e g a)^{2} + evaluation (W, sineVector (m u, v), o m e g a)^{2} - evaluation (W, oneVector (m u), o m e g a)^{2}))$

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

Source. Repository-derived.

Commentary.

For every real v, set c_v(x)=cos((pi/2)vx), s_v(x)=sin((pi/2)vx) and let 1 be the constant spatial vector. The finite coefficient vector consists of c_v and s_v with coefficient one and 1 with coefficient minus one. Its symmetric kernel has the actual representative cos((pi/2)v(x-y))-1.

The norm-square sum ||c_v||^2+||s_v||^2=||1||^2 equals the original spatial mass. Centering therefore cancels exactly. The finite second integral has the almost-everywhere representative W(c_v)^2+W(s_v)^2-W(1)^2, which is |F(v)|^2-Y^2 for F(v)=W(c_v)-iW(s_v) and Y=W(1).

The finite frequency identity agrees with the continuous extension on its actual finite-kernel input. Frequency integration and the singular logarithmic kernel require additional analytic statements; common continuous paths and process convergence require separate probability results.

References

Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.cosineVector_coe
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.finiteBound
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.finiteFrequency_sameNoise
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.finiteGram
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.finiteKernelMap_dense
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.kernelFlip_rankOne
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.norm_sq_integral
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.oneVector_coe
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.rankOne_total
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.secondIntegral_characterization
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.secondIntegral_diagonal
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.secondIntegral_product
Truth anchor: D5/S3/Fourier/Asymptotics/SameNoiseSecondChaos.sineVector_coe
Dependency: D5/S3/Fourier/Asymptotics/CountableGaussianQuadraticFourthMoment

Keyboard shortcuts

trureturing — Discovering truth

Same-noise second integral

Abstract

References