Exchangeable families

This file extends the sequence-level symmetry predicates to families indexed by an arbitrary type. An ExchangeableFamily has the same law along any two finite injective selections of indices. The existing ConditionallyIIDWith and ConditionallyIID predicates are already index-generic; this file relates them to exchangeable families.

Main results

• exchangeableFamily_iff_exchangeable identifies the family predicate over ℕ with the existing sequence predicate.
• MixedIIDWith.exchangeableFamily and MixedIID.exchangeableFamily give the easy implication from the mixture identity to exchangeability: along any two injective selections the block law is the same mixture of product measures.
• ConditionallyIIDWith.exchangeableFamily and ConditionallyIID.exchangeableFamily give the same implication for the conditional predicate, factored through the mixture one rather than proved again from the joint disintegration.
• ExchangeableFamily.comp_injective reindexes a family along an injection; the corresponding conditional i.i.d. lemmas are in ConditionallyIID.Basic.
• ExchangeableFamily.congr transports the predicate across a coordinatewise a.e. change of family, matching the sequence-level congruences in Exchangeability/Congr.lean.

This is the family exchangeability API needed for the Layer 8 target “de Finetti for other countable index types” in TauCetiRoadmap/Exchangeability/README.md. The countable-index theorem itself is in TauCeti.Probability.DeFinetti.CountableIndex.

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

A family is exchangeable when its law is unchanged after replacing any finite injective selection of indices by another of the same size.

Equations

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

theorem TauCeti.Probability.ExchangeableFamily.intro {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ∀ (m : ℕ) (k l : Fin m → ι), Function.Injective k → Function.Injective l → blockLaw μ X k = blockLaw μ X l) : ExchangeableFamily μ X

Constructor for exchangeability of an arbitrary family.

@[simp]

theorem TauCeti.Probability.exchangeableFamily_iff {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} : ExchangeableFamily μ X ↔ ∀ (m : ℕ) (k l : Fin m → ι), Function.Injective k → Function.Injective l → blockLaw μ X k = blockLaw μ X l

Simp normal form for exchangeability of an arbitrary family.

theorem TauCeti.Probability.ExchangeableFamily.blockLaw_eq {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ExchangeableFamily μ X) {m : ℕ} (k l : Fin m → ι) (hk : Function.Injective k) (hl : Function.Injective l) : blockLaw μ X k = blockLaw μ X l

The finite-block law equality defining an exchangeable family.

theorem TauCeti.Probability.ExchangeableFamily.congr {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ι → Ω → α} (hX : ExchangeableFamily μ X) (h : ∀ (i : ι), X i =ᵐ[μ] Y i) : ExchangeableFamily μ Y

Exchangeability of a family transports along a coordinatewise a.e. change of family: the predicate constrains only block laws, and those are unchanged (blockLaw_congr).

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

A mixed i.i.d. family is exchangeable. Along any two injective selections the block law is the same ν-mixture of product measures, so the two block laws agree.

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

A mixed i.i.d. family is exchangeable, existential form.

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

A conditionally i.i.d. family with a named directing measure is exchangeable: project to the mixture identity, which already forces the block laws to agree.

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

A conditionally i.i.d. family is exchangeable.

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

Exchangeability is preserved by reindexing a family along an injection.

theorem TauCeti.Probability.ExchangeableFamily.map_eq_of_injective {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} (h : ExchangeableFamily μ X) (hX : ∀ (i : ι), AEMeasurable (X i) μ) [Countable κ] {e f : κ → ι} (he : Function.Injective e) (hf : Function.Injective f) : MeasureTheory.Measure.map (fun (ω : Ω) (i : κ) => X (e i) ω) μ = MeasureTheory.Measure.map (fun (ω : Ω) (i : κ) => X (f i) ω) μ

An exchangeable family has one and the same law along any two injective reindexings. The finite-block equalities that define ExchangeableFamily are exactly the finite-dimensional laws of the reindexed families, so finite-dimensional-law uniqueness (ProbabilityTheory.map_eq_iff_forall_finset_map_restrict_eq) upgrades them to equality of the whole laws on κ → α. This is the family-level counterpart of Exchangeable.fullyExchangeable, which is the case κ = ι = ℕ with e a permutation and f = id.

Comparison with the sequence predicates

theorem TauCeti.Probability.ExchangeableFamily.exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : ExchangeableFamily μ X) : Exchangeable μ X

An exchangeable family indexed by ℕ is an exchangeable sequence.

theorem TauCeti.Probability.Exchangeable.exchangeableFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (h : Exchangeable μ X) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : ExchangeableFamily μ X

An exchangeable sequence with a.e. measurable coordinates is exchangeable as an ℕ-indexed family.

theorem TauCeti.Probability.exchangeableFamily_iff_exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : ExchangeableFamily μ X ↔ Exchangeable μ X

For a finite measure and a.e. measurable coordinates, exchangeability as an ℕ-indexed family is equivalent to the existing sequence predicate.