Cramér-Wold Theorem #
We prove the Cramér-Wold theorem.
Main statement #
tendstoInDistribution_iff_tendstoInDistribution_inner: ForE-valued random variablesX : ℕ → Ω → EandX' : Ω' → E, convergence in distribution ofXunderPtoX'underP'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.