Constant directing measures: the degenerate case of de Finetti

At a constant random measure ω ↦ p, the conditional and mixture identities coincide. Thus an i.i.d. sequence is conditionally i.i.d. with its common law as a constant directing measure.

The equivalence itself holds at an arbitrary index type (conditionallyIIDWith_const_of_mixedIIDWith, conditionallyIIDWith_const_iff_mixedIIDWith). The named-law constant-witness API is likewise index-generic: MixedIIDWith.iIndepFun_of_const, mixedIIDWith_const_iff_iIndepFun_and_map_eq, and MixedIIDWith.of_iIndepFun_map_eq all take an arbitrary index type. Independence itself never needed ℕ — Mathlib's ProbabilityTheory.iIndepFun is stated generically — the forward direction enumerates finite subsets by some bijection with Fin s.card rather than by an order, and the reverse direction takes the common law as a parameter instead of reconstructing it from a reference coordinate.

The of_iIndepFun_identDistrib forms come in two shapes. The _at versions take a caller-supplied reference coordinate i₀ and hold at an arbitrary index type; the unsuffixed ones are their ℕ-indexed specializations at 0, kept because that is the ergonomic form for sequences and because existing callers use it.

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

At a constant ν the conditional identity is free. The joint law of (p, block) is the block law pushed forward by Prod.mk p, and the disintegration δ_p ⊗ p^{⊗m} is the product law pushed forward by the same map, so the mixture identity already gives the joint one.

theorem TauCeti.Probability.conditionallyIIDWith_const_iff_mixedIIDWith {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {p : MeasureTheory.ProbabilityMeasure α} : (ConditionallyIIDWith μ X fun (x : Ω) => p) ↔ MixedIIDWith μ X fun (x : Ω) => p

The two de Finetti predicates agree at a constant witness. In general only mixedIIDWith_of_conditionallyIIDWith is available and the two need not agree; at a constant ν the converse holds too, so they coincide.

theorem TauCeti.Probability.conditionallyIIDWith_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 α} : (ConditionallyIIDWith μ X fun (x : Ω) => p) ↔ (∀ (i : ι), AEMeasurable (X i) μ) ∧ ProbabilityTheory.iIndepFun X μ ∧ ∀ (i : ι), MeasureTheory.Measure.map (X i) μ = ↑p

A constant directing measure means plain i.i.d.: fun _ => p witnesses ConditionallyIIDWith exactly when the coordinates are a.e. measurable and independent and each has law p.

theorem TauCeti.Probability.ConditionallyIIDWith.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₀) μ μ) : ConditionallyIIDWith μ X fun (x : Ω) => ⟨MeasureTheory.Measure.map (X i₀) μ, ⋯⟩

Independent, identically distributed coordinates are conditionally i.i.d., at an arbitrary index type, with the common law μ.map (X i₀) as constant directing measure. Conditional rather than merely mixture-level: at a constant witness the two identities coincide.

theorem TauCeti.Probability.ConditionallyIIDWith.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) μ μ) : ConditionallyIIDWith μ X fun (x : Ω) => ⟨MeasureTheory.Measure.map (X 0) μ, ⋯⟩

An i.i.d. sequence is conditionally i.i.d., with its common law as constant directing measure. The ℕ-indexed specialization at the reference coordinate 0.

theorem TauCeti.Probability.ConditionallyIID.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₀) μ μ) : ConditionallyIID μ X

An i.i.d. family is conditionally i.i.d. (existential directing-measure form), at an arbitrary index type, with i₀ the caller-supplied reference coordinate. The ℕ specialization follows.

theorem TauCeti.Probability.ConditionallyIID.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) μ μ) : ConditionallyIID μ X

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