Closure of Gaussian laws under L² limits

TheoremClosure of real Gaussian laws under L² limits#✓fully proved

If each X n is a real Gaussian random variable and X n → Y in L²(P), then Y is Gaussian.

theorem HasGaussianLaw.of_tendsto_eLpNorm_real
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {X : ℕ → Ω → ℝ} {Y : Ω → ℝ}
    (hX : ∀ n, HasGaussianLaw (X n) P) (hY : AEStronglyMeasurable Y P)
    (h : Tendsto (fun n ↦ eLpNorm (X n - Y) 2 P) atTop (𝓝 0)) : HasGaussianLaw Y P

Used by 1

Used byClosure of Gaussian laws under L² limits

TheoremClosure of Gaussian laws under L² limits#✓fully proved

If each X n is a Gaussian random vector in a separable Banach space E and X n → Y in L²(P), then Y is Gaussian.

theorem HasGaussianLaw.of_tendsto_eLpNorm
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E]
    {X : ℕ → Ω → E} {Y : Ω → E}
    (hX : ∀ n, HasGaussianLaw (X n) P) (hY : AEStronglyMeasurable Y P)
    (h : Tendsto (fun n ↦ eLpNorm (X n - Y) 2 P) atTop (𝓝 0)) : HasGaussianLaw Y P

Uses 1 · Used by 1

Proof usesClosure of real Gaussian laws under L² limits

Used byClosure of Gaussian processes under L² limits

TheoremClosure of Gaussian processes under L² limits#✓fully proved

If each X n is a real Gaussian process and X n t → Y t in L²(P) for every t, then Y is a Gaussian process.

theorem IsGaussianProcess.of_tendsto_eLpNorm
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {T : Type*} {X : ℕ → T → Ω → ℝ} {Y : T → Ω → ℝ}
    (hX : ∀ n, IsGaussianProcess (X n) P) (hY : ∀ t, AEStronglyMeasurable (Y t) P)
    (h : ∀ t, Tendsto (fun n ↦ eLpNorm (X n t - Y t) 2 P) atTop (𝓝 0)) :
    IsGaussianProcess Y P

Uses 1 · Used by 1

Proof usesClosure of Gaussian laws under L² limits

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremContinuity of the second moment pairing in L²#✓fully proved

If X n → Y and Z n → W in L²(P) (all square integrable), then E[X n Z n] → E[Y W].

theorem tendsto_integral_mul_of_tendsto_eLpNorm
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {X Z : ℕ → Ω → ℝ} {Y W : Ω → ℝ}
    (hX : ∀ n, MemLp (X n) 2 P) (hZ : ∀ n, MemLp (Z n) 2 P) (hY : MemLp Y 2 P)
    (hW : MemLp W 2 P)
    (h1 : Tendsto (fun n ↦ eLpNorm (X n - Y) 2 P) atTop (𝓝 0))
    (h2 : Tendsto (fun n ↦ eLpNorm (Z n - W) 2 P) atTop (𝓝 0)) :
    Tendsto (fun n ↦ ∫ ω, X n ω * Z n ω ∂P) atTop (𝓝 (∫ ω, Y ω * W ω ∂P))

Used by 1

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.