Documentation

TauCeti.Probability.Exchangeability.Family

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 MixedIIDWith and MixedIID predicates are already index-generic; this file relates them to exchangeable families.

Main results #

The de Finetti theorem for countably infinite index types is in TauCeti.Probability.DeFinetti.CountableIndex.

source
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.
Instances For
    source
    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.

    source
    @[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.

    source
    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.

    source
    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).

    source
    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.

    source
    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.

    source
    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.

    source
    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 #

    source
    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.

    source
    theorem TauCeti.Probability.Exchangeable.exchangeableFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {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.

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

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