An i.i.d. sequence is mixed i.i.d., exchangeable, and contractable

This file discharges the first worked example of the Exchangeability roadmap (TauCetiRoadmap/Exchangeability/README.md, "Worked examples"):

The law of an i.i.d. sequence is MixedIID, Exchangeable, and Contractable.

For a sequence X : ℕ → Ω → α on a probability space whose coordinates are independent (ProbabilityTheory.iIndepFun X μ) and identically distributed (∀ i, IdentDistrib (X i) (X 0) μ μ), the constant random measure ω ↦ law of X 0 is a mixing representative: MixedIIDWith.of_iIndepFun_identDistrib. Exchangeability and contractability then follow from the Layer 0 implications MixedIIDWith.exchangeable and MixedIIDWith.contractable.

Only the conclusions Exchangeable and Contractable need ℕ. The mixed-i.i.d. results hold for a family over an arbitrary index type: MixedIIDWith.of_iIndepFun_map_eq takes the common law as a parameter, and MixedIIDWith.of_iIndepFun_identDistrib_at takes a caller-supplied reference coordinate in place of 0. The unsuffixed of_iIndepFun_identDistrib forms are their ℕ specializations.

The mathematical content is the block-law identity: along an injective selection k : Fin m → ℕ the coordinates X ∘ k are independent (a subfamily of an independent family, ProbabilityTheory.iIndepFun.precomp) with common law μ.map (X 0), so their joint law is the m-fold product Measure.pi (fun _ => μ.map (X 0)) (ProbabilityTheory.iIndepFun.map_fun_eq_pi_map); this is exactly the value of the mixture against a constant mixing representative. The example validates the Layer 0 mixed-i.i.d. API on the canonical i.i.d. case and needs no material from cameronfreer/exchangeability.

The roadmap's worked-example entry also asks for the sharper statement that an i.i.d. sequence is genuinely ConditionallyIID, with this constant measure as its directing measure. That is TauCeti.Probability.ConditionallyIIDWith.of_iIndepFun_identDistrib, in TauCeti/Probability/Exchangeability/ConditionallyIID/Const.lean, which upgrades the mixture form below; the same file records that a constant witness makes the two predicates equivalent.

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

Independent coordinates with a common named law are mixed i.i.d., at an arbitrary index type. Naming the common law as a parameter avoids nominating a reference coordinate, which an abstract index type does not supply; over ℕ that reference is X 0, and MixedIIDWith.of_iIndepFun_identDistrib recovers that form.

theorem TauCeti.Probability.MixedIIDWith.of_iIndepFun_identDistrib_at {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (i₀ : ι) (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ι), ProbabilityTheory.IdentDistrib (X i) (X i₀) μ μ) : MixedIIDWith μ X fun (x : Ω) => ⟨MeasureTheory.Measure.map (X i₀) μ, ⋯⟩

Independent, identically distributed coordinates are mixed i.i.d., at an arbitrary index type, with the common law μ.map (X i₀) as constant mixing representative.

i₀ is a caller-supplied reference coordinate: an abstract index type provides none, and IdentDistrib needs one to compare against. MixedIIDWith.of_iIndepFun_map_eq avoids it entirely by naming the law instead, and is the better entry point when the law is already known.

theorem TauCeti.Probability.MixedIIDWith.of_iIndepFun_identDistrib {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : MixedIIDWith μ X fun (x : Ω) => ⟨MeasureTheory.Measure.map (X 0) μ, ⋯⟩

An i.i.d. sequence is mixed i.i.d., with the common law μ.map (X 0) as constant mixing representative. The ℕ-indexed specialization of MixedIIDWith.of_iIndepFun_identDistrib_at at the reference coordinate 0.

theorem TauCeti.Probability.MixedIID.of_iIndepFun_identDistrib_at {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (i₀ : ι) (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ι), ProbabilityTheory.IdentDistrib (X i) (X i₀) μ μ) : MixedIID μ X

An i.i.d. family is mixed i.i.d. (existential mixing-representative form), at an arbitrary index type, with i₀ the caller-supplied reference coordinate.

theorem TauCeti.Probability.MixedIID.of_iIndepFun_identDistrib {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : MixedIID μ X

An i.i.d. sequence is mixed i.i.d. (existential form), the ℕ-indexed specialization at the reference coordinate 0.

theorem TauCeti.Probability.Exchangeable.of_iIndepFun_identDistrib {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : Exchangeable μ X

An i.i.d. sequence is exchangeable. Sequence-level, and necessarily so: Exchangeable is defined for X : ℕ → Ω → α, so no reference-index parameter would generalize it. The family-level statement is MixedIIDWith.exchangeableFamily.

theorem TauCeti.Probability.Contractable.of_iIndepFun_identDistrib {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hindep : ProbabilityTheory.iIndepFun X μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) : Contractable μ X

An i.i.d. sequence is contractable.