theorem
MethodOfMoments.method_of_moments
{Ω : ℕ → Type u_1}
[(n : ℕ) → MeasurableSpace (Ω n)]
(X : (n : ℕ) → Ω n → ℝ)
(μ : (n : ℕ) → MeasureTheory.Measure (Ω n))
[∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)]
(hmom :
∀ k > 0,
Filter.Tendsto (fun (n : ℕ) => ProbabilityTheory.moment (X n) k (μ n)) Filter.atTop
(nhds (ProbabilityTheory.moment id k (ProbabilityTheory.gaussianReal 0 1))))
:
Method of moments (Theorem 4.5.4): if a sequence of random variables has moments of every positive order converging to those of the standard Gaussian, then it converges in distribution to the standard Gaussian.