Constant mixing measures

This file characterizes MixedIIDWith for a constant mixing representative. It is equivalent to plain independence with common marginal law.

Main results

• MixedIIDWith.blockLaw_eq_pi_of_const, MixedIIDWith.map_eq_of_const — what a constant mixing representative says: every injective block law is the m-fold product of p, and every coordinate has law p. Coordinate a.e. measurability is not special to a constant representative; MixedIIDWith carries it by definition.
• mixedIIDWith_const_iff_iIndepFun_and_map_eq — a constant p is a mixing representative exactly when the coordinates are a.e. measurable and independent with common law p.

theorem TauCeti.Probability.MixedIIDWith.blockLaw_eq_pi_of_const {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → α} {p : MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X fun (x : Ω) => p) {m : ℕ} (k : Fin m → ι) (hk : Function.Injective k) : blockLaw μ X k = MeasureTheory.Measure.pi fun (x : Fin m) => ↑p

A constant mixing representative says exactly that every injective block law is the corresponding product of p.

theorem TauCeti.Probability.MixedIIDWith.map_eq_of_const {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → α} {p : MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X fun (x : Ω) => p) (i : ι) : MeasureTheory.Measure.map (X i) μ = ↑p

Every coordinate of a family with a constant mixing representative p has law p.

theorem TauCeti.Probability.MixedIIDWith.iIndepFun_of_const {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → α} {p : MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X fun (x : Ω) => p) : ProbabilityTheory.iIndepFun X μ

The coordinates of a process with a constant mixing representative are independent. Along an injective selection the block law is a product measure, and Measure.pi on a finite index set is exactly what independence of that finite subfamily means.

theorem TauCeti.Probability.mixedIIDWith_const_iff_iIndepFun_and_map_eq {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → α} {p : MeasureTheory.ProbabilityMeasure α} : (MixedIIDWith μ X fun (x : Ω) => p) ↔ (∀ (i : ι), AEMeasurable (X i) μ) ∧ ProbabilityTheory.iIndepFun X μ ∧ ∀ (i : ι), MeasureTheory.Measure.map (X i) μ = ↑p

A constant mixing representative means plain i.i.d.: fun _ => p witnesses MixedIIDWith exactly when the coordinates are independent and each has law p.