Mixed i.i.d. families

A family is mixed i.i.d. when there is a measurable random probability measure ν : Ω → ProbabilityMeasure α such that every finite block of distinct coordinates has, as its law, the ν-mixture of the corresponding product measure, and every coordinate is μ-a.e. measurable. MixedIIDWith μ X ν names the witness ν; MixedIID is the existential wrapper.

⚠ This is a property of the unconditional finite-dimensional laws: the mixture identity constrains each finite block's marginal law, never the joint law of (ν, X). It is therefore not conditional independence, and is deliberately not named ConditionallyIID — that name belongs to the genuine joint-law disintegration Law(ν, block) = ∫ δ_{ν ω} ⊗ (ν ω)^{⊗m} dμ(ω) (Kallenberg 2005, §1.1 eq. (2)), which strictly strengthens the identity below at a fixed ν: for a nondegenerate mixing law an independent copy of a directing measure also witnesses MixedIIDWith, while the family is not conditionally i.i.d. given it. Following the roadmap's terminology, a ν witnessing only the mixture identity is a mixing representative; directing measure is reserved for the conditional predicate's witness.

The index type is arbitrary, matching ConditionallyIIDWith: the definition quantifies only over injective selections Fin m → ι, and nothing in it uses the order structure of ℕ. Sequence-level users get the ι = ℕ case by unification.

Exchangeability splits along that line. At an arbitrary index type the mixture identity gives MixedIIDWith.exchangeableFamily, in TauCeti.Probability.Exchangeability.Family; the sequence-level MixedIIDWith.exchangeable and .exchangeableAt, which conclude the ℕ-indexed Exchangeable predicate, stay in MixedIID/Implications.lean.

The other consequences over ℕ — prefixLaw_eq_mixture, blockLaw_eq_prefixLaw_of_injective, contractability, the path-law representation, and mixing-law uniqueness — remain sequence-level, because those genuinely use prefixes, shifts, or ℕ-indexed products.

This file adds the Layer 0 mixed-i.i.d. definitions and destructors, together with the Layer 1 rectangle-factorization characterization used by the common de Finetti ending. The exchangeability implications live in two places, along the same line as above: the sequence-level MixedIIDWith.exchangeable and .exchangeableAt, which conclude the ℕ-indexed Exchangeable, are in MixedIID/Implications.lean; the index-generic MixedIIDWith.exchangeableFamily and MixedIID.exchangeableFamily, which conclude ExchangeableFamily, are in Exchangeability/Family.lean beside the conditional analogue they mirror.

These declarations follow the roadmap signatures in TauCetiRoadmap/Exchangeability/README.md and TauCetiRoadmap/Exchangeability/Suggested.lean, Layer 0, refining the existential MixedIID of the roadmap into a named-witness relation (MixedIIDWith) plus its existential wrapper. They are adapted from the cameronfreer/exchangeability Layer 0 sources pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22, with Tau Ceti API names and hypotheses.

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

Mixed i.i.d.-ness with a specified mixing representative ν: the coordinates are a.e. measurable, the random measure ν is measurable, and along every finite selection k of distinct coordinates the block law is the ν-mixture of the product measure ProbabilityMeasure.pi (fun _ => ν ω). Distinctness (Function.Injective k) is what product laws need, in contrast with the order condition StrictMono of Contractable.

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 mixture 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.MixedIIDWith.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 → blockLaw μ X k = μ.bind fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) : MixedIIDWith μ X ν

Constructor: a.e. measurable coordinates and a measurable mixing representative together with the finite-block mixture identity.

@[simp]

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

Simp normal form for MixedIIDWith.

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

Mixed i.i.d.-ness: existence of a mixing representative.

Equations

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

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

Constructor from a mixing representative together with its witness.

@[simp]

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

Simp normal form for the existential wrapper MixedIID.

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

The mixing representative of a MixedIIDWith witness is measurable.

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

The defining finite-block mixture identity of a MixedIIDWith witness: along an injective selection the block law is the ν-mixture of the product measure. The prefix specialization is MixedIIDWith.prefixLaw_eq_mixture.

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

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

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

Coordinatewise a.e. measurability from mixed i.i.d.-ness, without naming a representative. The conclusion does not mention the mixing representative, so this is the natural level; the witness-level MixedIIDWith.aemeasurable is its specialization.

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

A MixedIID family has a mixing representative.

theorem TauCeti.Probability.mixedIIDWith_of_forall_rectangles {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hν : Measurable ν) (h_rect : ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → (blockLaw μ X k) (Set.univ.pi B) = ∫⁻ (ω : Ω), ∏ i : Fin m, ↑(ν ω) (B i) ∂μ) : MixedIIDWith μ X ν

A family with a.e. measurable coordinates is MixedIIDWith μ X ν once every injective finite block has the same rectangle values as the corresponding random product-measure mixture.

theorem TauCeti.Probability.MixedIIDWith.blockLaw_univ_pi {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) {m : ℕ} (k : Fin m → ι) (hk : Function.Injective k) (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : (blockLaw μ X k) (Set.univ.pi B) = ∫⁻ (ω : Ω), ∏ i : Fin m, ↑(ν ω) (B i) ∂μ

A MixedIIDWith witness gives the expected rectangle factorization for every injective finite block.

theorem TauCeti.Probability.mixedIIDWith_iff_forall_rectangles {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} : MixedIIDWith μ X ν ↔ (∀ (i : ι), AEMeasurable (X i) μ) ∧ Measurable ν ∧ ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → (blockLaw μ X k) (Set.univ.pi B) = ∫⁻ (ω : Ω), ∏ i : Fin m, ↑(ν ω) (B i) ∂μ

Rectangle factorization is equivalent to the named MixedIIDWith relation, for a family with a.e. measurable coordinates.

theorem TauCeti.Probability.mixedIID_iff_exists_forall_rectangles {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} : MixedIID μ X ↔ ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), (∀ (i : ι), AEMeasurable (X i) μ) ∧ Measurable ν ∧ ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → (blockLaw μ X k) (Set.univ.pi B) = ∫⁻ (ω : Ω), ∏ i : Fin m, ↑(ν ω) (B i) ∂μ

Rectangle factorization is equivalent to the existential MixedIID relation.

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

Reindexing a mixing representative along an injection. A finite injective selection from the reindexed family is a finite injective selection from the original, so the mixture identity is inherited with the same witness.

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

Reindexing a mixed i.i.d. family along an injection, existential form.