The Cramer-Wold theorem

Source: doi:10.1112/jlms/s1-11.4.290 Authors: Lazar Milikic Status: verified Main declarations: LeanPool.CramerWold.euclideanSpace_measure_eq_of_forall_inner_map_eq Tags: probability, measure-theory, characteristic-functions, cramer-wold MSC: 60B11, 60E10, 28A33

Mathematical overview

This file packages the Cramer-Wold theorem as a reusable family of measure and probability-law extensionality lemmas. The Euclidean-space statements give the classical finite-dimensional theorem. The Banach-space statements use all continuous linear maps to ℝ; the Hilbert-space statements rewrite those projections as scalar products x ↦ ⟪t, x⟫_ℝ.

The proof is a direct characteristic-function argument: equality of all one-dimensional projected laws gives equality of charFunDual, and Mathlib's Measure.ext_of_charFunDual recovers the original finite measure.

theorem LeanPool.CramerWold.measure_eq_of_forall_dual_map_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (L : StrongDual ℝ E), MeasureTheory.Measure.map (⇑L) μ = MeasureTheory.Measure.map (⇑L) ν) : μ = ν

Finite measures on a real Banach space are determined by their one-dimensional continuous-linear projections.

theorem LeanPool.CramerWold.measure_eq_iff_forall_dual_map_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : μ = ν ↔ ∀ (L : StrongDual ℝ E), MeasureTheory.Measure.map (⇑L) μ = MeasureTheory.Measure.map (⇑L) ν

Cramer-Wold as an extensionality criterion for finite measures, in continuous-dual form.

theorem LeanPool.CramerWold.probabilityMeasure_eq_of_forall_dual_map_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (μ ν : MeasureTheory.ProbabilityMeasure E) (h : ∀ (L : StrongDual ℝ E), MeasureTheory.Measure.map ⇑L ↑μ = MeasureTheory.Measure.map ⇑L ↑ν) : μ = ν

Probability measures on a real Banach space are determined by all continuous-linear one-dimensional projections.

theorem LeanPool.CramerWold.probabilityMeasure_eq_iff_forall_dual_map_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (μ ν : MeasureTheory.ProbabilityMeasure E) : μ = ν ↔ ∀ (L : StrongDual ℝ E), MeasureTheory.Measure.map ⇑L ↑μ = MeasureTheory.Measure.map ⇑L ↑ν

Cramer-Wold as an extensionality criterion for probability measures, in continuous-dual form.

theorem LeanPool.CramerWold.charFun_eq_charFun_map_inner_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) (t : E) : MeasureTheory.charFun μ t = MeasureTheory.charFun (MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) μ) 1

The characteristic function at t is the real characteristic function of the scalar projection x ↦ ⟪t, x⟫_ℝ at 1.

theorem LeanPool.CramerWold.measure_eq_of_forall_inner_map_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (t : E), MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) μ = MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) ν) : μ = ν

Finite measures on a real Hilbert space are determined by scalar inner-product projections.

theorem LeanPool.CramerWold.measure_eq_iff_forall_inner_map_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : μ = ν ↔ ∀ (t : E), MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) μ = MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) ν

Cramer-Wold as an extensionality criterion for finite measures on a real Hilbert space.

theorem LeanPool.CramerWold.probabilityMeasure_eq_of_forall_inner_map_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (μ ν : MeasureTheory.ProbabilityMeasure E) (h : ∀ (t : E), MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) ↑μ = MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) ↑ν) : μ = ν

Probability measures on a real Hilbert space are determined by scalar inner-product projections.

theorem LeanPool.CramerWold.probabilityMeasure_eq_iff_forall_inner_map_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] (μ ν : MeasureTheory.ProbabilityMeasure E) : μ = ν ↔ ∀ (t : E), MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) ↑μ = MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) ↑ν

Cramer-Wold as an extensionality criterion for probability measures on a real Hilbert space.

theorem LeanPool.CramerWold.euclideanSpace_measure_eq_of_forall_inner_map_eq {n : ℕ} {μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (t : EuclideanSpace ℝ (Fin n)), MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) μ = MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) ν) : μ = ν

The classical finite-dimensional Cramer-Wold theorem for finite measures on ℝ^n, represented by EuclideanSpace ℝ (Fin n).

theorem LeanPool.CramerWold.euclideanSpace_measure_eq_iff_forall_inner_map_eq {n : ℕ} {μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : μ = ν ↔ ∀ (t : EuclideanSpace ℝ (Fin n)), MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) μ = MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) ν

Cramer-Wold as an extensionality criterion for finite measures on ℝ^n, represented by EuclideanSpace ℝ (Fin n).

theorem LeanPool.CramerWold.euclideanSpace_probabilityMeasure_eq_of_forall_inner_map_eq {n : ℕ} (μ ν : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n))) (h : ∀ (t : EuclideanSpace ℝ (Fin n)), MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) ↑μ = MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) ↑ν) : μ = ν

Probability measures on ℝ^n, represented by EuclideanSpace ℝ (Fin n), are determined by all scalar projections.

theorem LeanPool.CramerWold.euclideanSpace_probabilityMeasure_eq_iff_forall_inner_map_eq {n : ℕ} (μ ν : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n))) : μ = ν ↔ ∀ (t : EuclideanSpace ℝ (Fin n)), MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) ↑μ = MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin n)) => inner ℝ t x) ↑ν

Cramer-Wold as an extensionality criterion for probability measures on ℝ^n, represented by EuclideanSpace ℝ (Fin n).

theorem LeanPool.CramerWold.identDistrib_of_forall_dual_comp_identDistrib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → E} {Y : Ω' → E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] (hX : AEMeasurable X P) (hY : AEMeasurable Y Q) (h : ∀ (L : StrongDual ℝ E), ProbabilityTheory.IdentDistrib (fun (ω : Ω) => L (X ω)) (fun (ω : Ω') => L (Y ω)) P Q) : ProbabilityTheory.IdentDistrib X Y P Q

If all continuous-linear real projections of two random variables are identically distributed, then the random variables themselves are identically distributed.

theorem LeanPool.CramerWold.identDistrib_iff_forall_dual_comp_identDistrib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → E} {Y : Ω' → E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] (hX : AEMeasurable X P) (hY : AEMeasurable Y Q) : ProbabilityTheory.IdentDistrib X Y P Q ↔ ∀ (L : StrongDual ℝ E), ProbabilityTheory.IdentDistrib (fun (ω : Ω) => L (X ω)) (fun (ω : Ω') => L (Y ω)) P Q

Identical distribution is equivalent to identical distribution of every continuous-linear real projection.

theorem LeanPool.CramerWold.law_eq_of_forall_dual_comp_identDistrib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → E} {Y : Ω' → E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] {μ ν : MeasureTheory.Measure E} (hX : ProbabilityTheory.HasLaw X μ P) (hY : ProbabilityTheory.HasLaw Y ν Q) (h : ∀ (L : StrongDual ℝ E), ProbabilityTheory.IdentDistrib (fun (ω : Ω) => L (X ω)) (fun (ω : Ω') => L (Y ω)) P Q) : μ = ν

Equality of laws follows from identical distribution of all continuous-linear real projections of random variables with those laws.

theorem LeanPool.CramerWold.identDistrib_of_forall_inner_comp_identDistrib {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → E} {Y : Ω' → E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] (hX : AEMeasurable X P) (hY : AEMeasurable Y Q) (h : ∀ (t : E), ProbabilityTheory.IdentDistrib (fun (ω : Ω) => inner ℝ t (X ω)) (fun (ω : Ω') => inner ℝ t (Y ω)) P Q) : ProbabilityTheory.IdentDistrib X Y P Q

If all scalar inner-product projections of two random variables are identically distributed, then the random variables themselves are identically distributed.

theorem LeanPool.CramerWold.identDistrib_iff_forall_inner_comp_identDistrib {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → E} {Y : Ω' → E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] (hX : AEMeasurable X P) (hY : AEMeasurable Y Q) : ProbabilityTheory.IdentDistrib X Y P Q ↔ ∀ (t : E), ProbabilityTheory.IdentDistrib (fun (ω : Ω) => inner ℝ t (X ω)) (fun (ω : Ω') => inner ℝ t (Y ω)) P Q

Identical distribution is equivalent to identical distribution of every scalar inner-product projection.

theorem LeanPool.CramerWold.law_eq_of_forall_inner_comp_identDistrib {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} {Q : MeasureTheory.Measure Ω'} {X : Ω → E} {Y : Ω' → E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure Q] {μ ν : MeasureTheory.Measure E} (hX : ProbabilityTheory.HasLaw X μ P) (hY : ProbabilityTheory.HasLaw Y ν Q) (h : ∀ (t : E), ProbabilityTheory.IdentDistrib (fun (ω : Ω) => inner ℝ t (X ω)) (fun (ω : Ω') => inner ℝ t (Y ω)) P Q) : μ = ν

Equality of laws follows from identical distribution of all scalar inner-product projections of random variables with those laws.

theorem LeanPool.CramerWold.hasLaw_of_forall_dual_comp_hasLaw {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → E} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X P) (h : ∀ (L : StrongDual ℝ E), ProbabilityTheory.HasLaw (fun (ω : Ω) => L (X ω)) (MeasureTheory.Measure.map (⇑L) μ) P) : ProbabilityTheory.HasLaw X μ P

A random variable has law μ if all of its continuous-linear real projections have the corresponding projected laws of μ.

theorem LeanPool.CramerWold.hasLaw_iff_forall_dual_comp_hasLaw {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → E} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X P) : ProbabilityTheory.HasLaw X μ P ↔ ∀ (L : StrongDual ℝ E), ProbabilityTheory.HasLaw (fun (ω : Ω) => L (X ω)) (MeasureTheory.Measure.map (⇑L) μ) P

A random variable has law μ iff every continuous-linear real projection has the projected law of μ.

theorem LeanPool.CramerWold.hasLaw_of_forall_inner_comp_hasLaw {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → E} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X P) (h : ∀ (t : E), ProbabilityTheory.HasLaw (fun (ω : Ω) => inner ℝ t (X ω)) (MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) μ) P) : ProbabilityTheory.HasLaw X μ P

A random variable has law μ if all of its scalar inner-product projections have the corresponding projected laws of μ.

theorem LeanPool.CramerWold.hasLaw_iff_forall_inner_comp_hasLaw {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → E} {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] (hX : AEMeasurable X P) : ProbabilityTheory.HasLaw X μ P ↔ ∀ (t : E), ProbabilityTheory.HasLaw (fun (ω : Ω) => inner ℝ t (X ω)) (MeasureTheory.Measure.map (fun (x : E) => inner ℝ t x) μ) P

A random variable has law μ iff every scalar inner-product projection has the projected law of μ.