Conditionally i.i.d. families

The conditional strengthening of the mixture identity: a family is conditionally i.i.d. with directing measure ν when, along every finite selection of distinct coordinates, the joint law of (ν, block) is the disintegration ∫ δ_{ν ω} ⊗ (ν ω)^{⊗m} dμ(ω) — conditionally on ν, the block is i.i.d. ν (Kallenberg 2005, §1.1 eq. (2)). The definition also requires every coordinate to be μ-a.e. measurable and ν itself to be measurable.

Stating it as a joint-law identity means the definition needs no conditional expectations, and sits in the same bind/pi vocabulary as MixedIIDWith.

Why this is stronger than MixedIIDWith

MixedIIDWith μ X ν constrains only each block's marginal law. It therefore does not pin down how X relates to ν: for a nondegenerate mixing law, an independent copy of a directing measure also witnesses MixedIIDWith, while the process is not conditionally i.i.d. given that copy. The arrow runs one way only, and mixedIIDWith_of_conditionallyIIDWith is that arrow — obtained by integrating the ν coordinate out.

Terminology follows the roadmap: a ν witnessing only the mixture identity is a mixing representative, whereas ν here is a genuine directing measure.

Main results

• ConditionallyIIDWith, ConditionallyIID — the index-generic predicate and its existential wrapper, with their constructor, accessor, simp-normal-form, and injective-reindexing API.
• mixedIIDWith_of_conditionallyIIDWith, mixedIID_of_conditionallyIID — the easy projection down to the mixture identity. Both predicates are index-generic, so the projection is too.

This is a Layer 0 contribution to TauCetiRoadmap/Exchangeability/README.md — the conditional predicate for which the roadmap reserves the ConditionallyIID name, together with the easy projection it pins alongside — which rests on the Layer 1 joint-kernel lemma measurable_dirac_prod_probabilityMeasure_pi_const_toMeasure.

The Layer 1 joint-rectangle common ending conditionallyIID_of_jointRectangles lives in TauCeti.Probability.DeFinetti.ConditionalCommonEnding. The Layer 6 summit theorems that conclude this predicate, together with the deFinetti* equivalence handles, live in TauCeti.Probability.DeFinetti.Theorem. A.e. uniqueness of the directing measure (conditionallyIID_ae_unique) lives in TauCeti.Probability.Exchangeability.ConditionallyIID.Unique.

def TauCeti.Probability.ConditionallyIIDWith {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → α) (ν : Ω → MeasureTheory.ProbabilityMeasure α) : Prop

Conditional i.i.d.-ness with a specified directing measure ν: the coordinates are a.e. measurable, the random measure ν is measurable, and along every finite selection k of distinct coordinates the joint law of (ν, block) is the ν-disintegration ∫ δ_{ν ω} ⊗ (ν ω)^{⊗m} dμ(ω).

Constraining the joint law, rather than just the block's marginal, is exactly what makes this the conditional statement: see MixedIIDWith for the marginal-only version and mixedIIDWith_of_conditionallyIIDWith for the arrow between them.

Coordinatewise a.e. measurability is part of the definition because Measure.map sends a function that is not a.e. measurable to a junk Dirac mass, so the joint-law identity alone cannot see measurability; compare ProbabilityTheory.HasLaw in Mathlib.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Probability.ConditionallyIIDWith.intro {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hν : Measurable ν) (h : ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ = μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) : ConditionallyIIDWith μ X ν

Constructor: a.e. measurable coordinates and a measurable directing measure together with the joint-law disintegration.

@[simp]

theorem TauCeti.Probability.conditionallyIIDWith_iff {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} : ConditionallyIIDWith μ X ν ↔ (∀ (i : ι), AEMeasurable (X i) μ) ∧ Measurable ν ∧ ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ = μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)

Simp normal form for ConditionallyIIDWith.

def TauCeti.Probability.ConditionallyIID {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ι → Ω → α) : Prop

Conditional i.i.d.-ness: existence of a directing measure.

Equations

• TauCeti.Probability.ConditionallyIID μ X = ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), TauCeti.Probability.ConditionallyIIDWith μ X ν

theorem TauCeti.Probability.ConditionallyIID.of_directing {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : ConditionallyIID μ X

Constructor from a directing measure together with its witness.

@[simp]

theorem TauCeti.Probability.conditionallyIID_iff {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} : ConditionallyIID μ X ↔ ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), ConditionallyIIDWith μ X ν

Simp normal form for the existential wrapper ConditionallyIID.

theorem TauCeti.Probability.ConditionallyIIDWith.aemeasurable {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) (i : ι) : AEMeasurable (X i) μ

The coordinates of a ConditionallyIIDWith family are a.e. measurable.

theorem TauCeti.Probability.ConditionallyIIDWith.measurable_directing {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : Measurable ν

The directing measure of a ConditionallyIIDWith witness is measurable.

theorem TauCeti.Probability.ConditionallyIIDWith.jointLaw_eq_disintegration {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {m : ℕ} (k : Fin m → ι) (hk : Function.Injective k) : MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ = μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)

The defining joint-law disintegration of a ConditionallyIIDWith witness.

theorem TauCeti.Probability.ConditionallyIID.exists_directing {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ConditionallyIID μ X) : ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), ConditionallyIIDWith μ X ν

A ConditionallyIID family has a directing measure.

theorem TauCeti.Probability.ConditionallyIIDWith.comp_injective {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {f : κ → ι} (hf : Function.Injective f) : ConditionallyIIDWith μ (fun (j : κ) => X (f j)) ν

Conditional i.i.d.-ness with a named directing measure is preserved by reindexing along an injection. The directing measure is unchanged.

theorem TauCeti.Probability.ConditionallyIID.comp_injective {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ConditionallyIID μ X) {f : κ → ι} (hf : Function.Injective f) : ConditionallyIID μ fun (j : κ) => X (f j)

Conditional i.i.d.-ness is preserved by reindexing along an injection.

theorem TauCeti.Probability.mixedIIDWith_of_conditionallyIIDWith {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : MixedIIDWith μ X ν

The easy arrow. A directing measure is in particular a mixing representative: the mixture identity is the joint disintegration with the ν coordinate integrated out.

Taking the second marginal of both sides does exactly that. On the left, Measure.snd_map_prodMk₀ discards the ν coordinate needing only measurability of ν itself, which the predicate supplies. On the right, naturality of bind pushes the marginal inside the mixture, where each δ_{ν ω} factor integrates away.

theorem TauCeti.Probability.mixedIID_of_conditionallyIID {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ConditionallyIID μ X) : MixedIID μ X

The existential form of the easy arrow.

theorem TauCeti.Probability.ConditionallyIID.aemeasurable {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ConditionallyIID μ X) (i : ι) : AEMeasurable (X i) μ

A conditionally i.i.d. family has a.e.-measurable coordinates, so no separate coordinate measurability hypothesis is needed.