Cramér-Wold Theorem

We prove the Cramér-Wold theorem.

Main statement

• tendstoInDistribution_iff_tendstoInDistribution_inner: For E-valued random variables X : ℕ → Ω → E and X' : Ω' → E, convergence in distribution of X under P to X' under P' is equivalent to convergence in distribution of all their scalar projections.

theorem tendstoInDistribution_iff_tendstoInDistribution_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {X' : Ω' → E} {X : ℕ → Ω → E} (hX' : AEMeasurable X' P') (hX : ∀ (n : ℕ), AEMeasurable (X n) P) : MeasureTheory.TendstoInDistribution X Filter.atTop X' (fun (x : ℕ) => P) P' ↔ ∀ (t : E), MeasureTheory.TendstoInDistribution (fun (x1 : ℕ) (x2 : Ω) => inner ℝ (X x1 x2) t) Filter.atTop (fun (x : Ω') => inner ℝ (X' x) t) (fun (x : ℕ) => P) P'

The Cramér-Wold theorem: convergence in distribution of a sequence of random variables taking values in a finite-dimensional real inner product space is equivalent to convergence in distribution of all its scalar projections.

theorem TendstoInDistribution.of_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {X' : Ω' → E} {X : ℕ → Ω → E} (hX' : AEMeasurable X' P') (hX : ∀ (n : ℕ), AEMeasurable (X n) P) : (∀ (t : E), MeasureTheory.TendstoInDistribution (fun (x1 : ℕ) (x2 : Ω) => inner ℝ (X x1 x2) t) Filter.atTop (fun (x : Ω') => inner ℝ (X' x) t) (fun (x : ℕ) => P) P') → MeasureTheory.TendstoInDistribution X Filter.atTop X' (fun (x : ℕ) => P) P'

Alias of the reverse direction of tendstoInDistribution_iff_tendstoInDistribution_inner.

---

The Cramér-Wold theorem: convergence in distribution of a sequence of random variables taking values in a finite-dimensional real inner product space is equivalent to convergence in distribution of all its scalar projections.