Closure of centered Gaussian random variables in L² #
This file supplies the analytic closure step needed when passing from finite Fourier sums to the mollified noise. The proof is by characteristic functions, with the convergence estimate
|exp (itXₙ) - exp (itX)| ≤ |t| |Xₙ - X|.
In particular, no independence or representation of the Gaussian variables on a common canonical probability space is used.
theorem
Anderson4D.eLpNorm_two_toReal_sq
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
(f : Ω → ℝ)
(hf : MeasureTheory.MemLp f 2 μ)
:
For a real L² function, the square of its L² seminorm is its
second absolute moment.
theorem
Anderson4D.variance_eq_eLpNorm_two_toReal_sq
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(f : Ω → ℝ)
(hf : MeasureTheory.MemLp f 2 μ)
(hcenter : ∫ (ω : Ω), f ω ∂μ = 0)
:
The variance of a centered real L² function is the square of its
L² seminorm.
theorem
Anderson4D.hasGaussianLaw_of_tendsto_eLpNorm_two
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(X : ℕ → Ω → ℝ)
(Y : Ω → ℝ)
(hX : ∀ (n : ℕ), ProbabilityTheory.HasGaussianLaw (X n) μ)
(hcenter : ∀ (n : ℕ), ∫ (ω : Ω), X n ω ∂μ = 0)
(hmem : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ)
(hY : MeasureTheory.MemLp Y 2 μ)
(hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (X n - Y) 2 μ) Filter.atTop (nhds 0))
:
Centered real Gaussian laws are closed under L² convergence on a
fixed probability space.
The convergence hypothesis is stated directly in eLpNorm; this is the
form produced by the summable Fourier-series API.