The coding representation of an exchangeable sequence

De Finetti's theorem describes an exchangeable sequence by a conditional law: there is a random probability measure ν such that, given ν, the coordinates are i.i.d. ν. This file converts that description into a functional one. Writing ϑ for a sequence of independent uniform variables on the unit interval, independent of ν, there is a single jointly measurable

f : ProbabilityMeasure α → I → α

with

(ν, X) =ᵈ (ν, (f ν ϑᵢ)ᵢ).

Thus, in distribution, an exchangeable sequence is a fixed measurable function of one random parameter — its directing measure — and an independent i.i.d. uniform noise sequence, with all the randomness of the sequence carried by the noise. This is the sequence case of the representations in the Aldous–Hoover family, and the shape in which those representations are stated.

The function is unitIntervalCoding α of TauCeti.Probability.Kernel.Randomization, the same one for every process on α; only the law of the parameter changes. The converse holds for an arbitrary jointly measurable f, without a standard Borel hypothesis and for an arbitrary parameter space and arbitrary exchangeable noise (exchangeableLaw_map_prod_coding), so the two together characterize exchangeability (exchangeableLaw_iff_exists_coding).

Main results

• TauCeti.Probability.map_prod_unitIntervalCoding_eq_deFinettiBarycenter and TauCeti.Probability.map_prod_unitIntervalCoding_eq_iidMixtureLaw — coding a mixing law by uniform noise reproduces the de Finetti barycenter, and, keeping the parameter, the canonical conditionally i.i.d. law.
• TauCeti.Probability.ConditionallyIIDWith.jointPathLaw_eq_map_unitIntervalCoding — the joint law of a directing measure and its process is the law of the coded pair.
• TauCeti.Probability.deFinetti_coding — the representation: the joint law of an exchangeable process and its directing measure is the law of the coded parameter-noise pair.
• TauCeti.Probability.ExchangeableLaw.exists_eq_map_unitIntervalCoding and TauCeti.Probability.exchangeableLaw_iff_exists_coding — the path-law forms, the second an equivalence.
• TauCeti.Probability.ConditionallyIIDWith.map_comp_eq_map_unitIntervalCoding_of_ae_eq and TauCeti.Probability.ConditionallyIIDWith.exists_map_comp_eq_map_unitIntervalCoding — coding given observed coordinates: once observed coordinates determine the directing measure, the remaining coordinates are coded from them by fresh i.i.d. uniform noise.
• TauCeti.Probability.Exchangeable.exists_map_comp_eq_map_coding_of_prodMk — the same coding for a sequence exchangeable over a random element Z, with Z among the observed data.

Implementation

Everything reduces to one identity about Measure.prod: a parameter drawn from π together with independent i.i.d. noise, pushed through a map carrying the noise law to P t, has the canonical law iidMixtureLaw (map_prod_infinitePi_eq_iidMixtureLaw). At the coding map this is map_volume_unitIntervalCoding, and forgetting the parameter gives the barycenter. No new measure theory is needed: the analytic content is Mathlib's ProbabilityTheory.Kernel.exists_measurable_map_eq_unitInterval and the probabilistic content is the already-proved de Finetti theorem.

This advances TauCetiRoadmap/Exchangeability/README.md, Layer 8, "exchangeable arrays and the Aldous–Hoover representation": a functional representation is the form those theorems take, and the sequence case built here is the base of that tower. No material is adapted from cameronfreer/exchangeability, which stops at the conditional-law form of de Finetti.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1, Proposition 1.4.
• O. Kallenberg, Foundations of Modern Probability, 3rd ed., Lemma 4.22.

theorem TauCeti.Probability.measurable_unitIntervalCodingPath {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] : Measurable fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) (i : ℕ) => unitIntervalCoding α p.1 (p.2 i)

Joint measurability of the canonical coordinatewise coding map.

@[simp]

theorem TauCeti.Probability.map_prod_unitIntervalCoding_eq_iidMixtureLaw {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) : MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) => (p.1, fun (i : ℕ) => unitIntervalCoding α p.1 (p.2 i))) (π.prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume)) = iidMixtureLaw π id

Coding a mixing law, keeping the parameter. Retaining the drawn probability measure as a coordinate, the same construction produces the canonical conditionally i.i.d. law iidMixtureLaw: the parameter is not merely a mixing representative of the coded sequence but its directing measure.

@[simp]

theorem TauCeti.Probability.map_prod_unitIntervalCoding_eq_deFinettiBarycenter {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) : MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) (i : ℕ) => unitIntervalCoding α p.1 (p.2 i)) (π.prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume)) = deFinettiBarycenter π

Coding a mixing law. Drawing a probability measure from π, then coding an independent i.i.d. uniform sequence by it, produces the de Finetti barycenter of π.

theorem TauCeti.Probability.ConditionallyIIDWith.jointPathLaw_eq_map_unitIntervalCoding {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) : jointPathLaw μ X ν = MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) => (p.1, fun (i : ℕ) => unitIntervalCoding α p.1 (p.2 i))) ((MeasureTheory.Measure.map ν μ).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))

The coding representation of a conditionally i.i.d. process. The joint law of a directing measure and the whole path is the joint law of a parameter drawn from the mixing law and the path obtained by coding independent uniform noise by that parameter.

Keeping the directing measure as a coordinate is what makes this a representation of the process and not merely of its path law.

theorem TauCeti.Probability.deFinetti_coding {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) (hX : Exchangeable μ X) : ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), ConditionallyIIDWith μ X ν ∧ jointPathLaw μ X ν = MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) => (p.1, fun (i : ℕ) => unitIntervalCoding α p.1 (p.2 i))) ((MeasureTheory.Measure.map ν μ).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))

The coding representation of an exchangeable process. An exchangeable sequence in a nonempty standard Borel space has a directing measure ν — it is conditionally i.i.d. ν — such that the joint law of (ν, X) equals the law of the pair obtained by applying one fixed measurable map coordinatewise to ν and independent i.i.d. uniform noise.

This is the functional form of de Finetti's theorem: all the randomness of the sequence beyond its directing measure is the uniform noise.

theorem TauCeti.Probability.ExchangeableLaw.exists_eq_map_unitIntervalCoding {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] (hρ : ExchangeableLaw ρ) : ∃ (π : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α)), ρ = MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) (i : ℕ) => unitIntervalCoding α p.1 (p.2 i)) ((↑π).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))

The coding representation of an exchangeable path law. An exchangeable probability measure on ℕ → α is the law of a coded i.i.d. uniform sequence, for a mixing law on ProbabilityMeasure α.

theorem TauCeti.Probability.exchangeableLaw_iff_exists_coding {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsProbabilityMeasure ρ] : ExchangeableLaw ρ ↔ ∃ (π : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α)) (f : MeasureTheory.ProbabilityMeasure α → ↑unitInterval → α), Measurable (Function.uncurry f) ∧ ρ = MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) (i : ℕ) => f p.1 (p.2 i)) ((↑π).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))

Exchangeability is exactly codability. A probability law on ℕ → α, with α nonempty standard Borel, is exchangeable iff it is the law of a jointly measurable function of a random parameter and an independent i.i.d. uniform sequence, applied coordinatewise.

The forward direction produces the canonical coding map unitIntervalCoding α and takes the parameter to be the directing measure itself; the converse holds for an arbitrary jointly measurable f.

theorem TauCeti.Probability.exists_pathLaw_eq_map_unitIntervalCoding {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) (hX : Exchangeable μ X) : ∃ (π : MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α)), pathLaw μ X = MeasureTheory.Measure.map (fun (p : MeasureTheory.ProbabilityMeasure α × (ℕ → ↑unitInterval)) (i : ℕ) => unitIntervalCoding α p.1 (p.2 i)) ((↑π).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => MeasureTheory.volume))

The path-law form of deFinetti_coding: the law of an exchangeable process is the law of a coded i.i.d. uniform sequence.

theorem TauCeti.Probability.ConditionallyIIDWith.map_directing_comp_eq_map_unitIntervalCoding {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {ι : Type u_3} {κ : Type u_4} {e : ι → ℕ} {g : κ → ℕ} (hg : Function.Injective g) (heg : Disjoint (Set.range e) (Set.range g)) : MeasureTheory.Measure.map (fun (ω : Ω) => ((ν ω, fun (a : ι) => X (e a) ω), fun (b : κ) => X (g b) ω)) μ = MeasureTheory.Measure.map (fun (q : (MeasureTheory.ProbabilityMeasure α × (ι → α)) × (κ → ↑unitInterval)) => (q.1, fun (b : κ) => unitIntervalCoding α q.1.1 (q.2 b))) ((MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (a : ι) => X (e a) ω)) μ).prod (MeasureTheory.Measure.infinitePi fun (x : κ) => MeasureTheory.volume))

Coding the unobserved coordinates, keeping the directing measure. For a conditionally i.i.d. process, the coordinates along an injective g are, jointly with the directing measure and the coordinates along any e whose range avoids that of g, obtained by coding fresh i.i.d. uniform variables by the directing measure. The selection e need not be injective.

theorem TauCeti.Probability.ConditionallyIIDWith.map_comp_eq_map_unitIntervalCoding_of_ae_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {ι : Type u_3} {κ : Type u_4} {γ : Type u_5} [MeasurableSpace γ] {e : ι → ℕ} {g : κ → ℕ} (hg : Function.Injective g) (heg : Disjoint (Set.range e) (Set.range g)) {φ : (ι → α) → γ} (hφ : Measurable φ) {G : γ → MeasureTheory.ProbabilityMeasure α} (hG : Measurable G) (hνG : ν =ᵐ[μ] fun (ω : Ω) => G (φ fun (a : ι) => X (e a) ω)) : MeasureTheory.Measure.map (fun (ω : Ω) => (φ fun (a : ι) => X (e a) ω, fun (b : κ) => X (g b) ω)) μ = MeasureTheory.Measure.map (fun (p : γ × (κ → ↑unitInterval)) => (p.1, fun (b : κ) => unitIntervalCoding α (G p.1) (p.2 b))) ((MeasureTheory.Measure.map (fun (ω : Ω) => φ fun (a : ι) => X (e a) ω) μ).prod (MeasureTheory.Measure.infinitePi fun (x : κ) => MeasureTheory.volume))

Coding the unobserved coordinates from an observed statistic. Let Y = φ (X ∘ e) be a measurable statistic of the coordinates along e which determines the directing measure almost surely, ν = G Y. Then the coordinates along an injective g whose range avoids that of e are jointly distributed with Y as the coding of fresh i.i.d. uniform variables by G Y: given Y, they are i.i.d. with law G Y.

theorem TauCeti.Probability.ConditionallyIIDWith.exists_map_comp_eq_map_unitIntervalCoding {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {κ : Type u_3} {e : ℕ → ℕ} {g : κ → ℕ} (he : Function.Injective e) (hg : Function.Injective g) (heg : Disjoint (Set.range e) (Set.range g)) : ∃ (G : (ℕ → α) → MeasureTheory.ProbabilityMeasure α), Measurable G ∧ (ν =ᵐ[μ] fun (ω : Ω) => G fun (a : ℕ) => X (e a) ω) ∧ MeasureTheory.Measure.map (fun (ω : Ω) => (fun (a : ℕ) => X (e a) ω, fun (b : κ) => X (g b) ω)) μ = MeasureTheory.Measure.map (fun (p : (ℕ → α) × (κ → ↑unitInterval)) => (p.1, fun (b : κ) => unitIntervalCoding α (G p.1) (p.2 b))) ((MeasureTheory.Measure.map (fun (ω : Ω) (a : ℕ) => X (e a) ω) μ).prod (MeasureTheory.Measure.infinitePi fun (x : κ) => MeasureTheory.volume))

Coding the unobserved coordinates from infinitely many observed ones. The coordinates along an injective e determine the directing measure through a measurable map G, and the coordinates along an injective g whose range avoids that of e are coded from the observed ones by G and fresh i.i.d. uniform variables.

theorem TauCeti.Probability.Exchangeable.exists_map_comp_eq_map_coding_of_prodMk {Ω : Type u_1} [MeasurableSpace Ω] {γ : Type u_3} {β : Type u_4} [MeasurableSpace γ] [StandardBorelSpace γ] [Nonempty γ] [MeasurableSpace β] [StandardBorelSpace β] [Nonempty β] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {Z : Ω → γ} {Y : ℕ → Ω → β} (hZY : Exchangeable μ fun (n : ℕ) (ω : Ω) => (Z ω, Y n ω)) (hZ : AEMeasurable Z μ) (hY : ∀ (n : ℕ), AEMeasurable (Y n) μ) {κ : Type u_5} {e : ℕ → ℕ} {g : κ → ℕ} (he : Function.Injective e) (hg : Function.Injective g) (heg : Disjoint (Set.range e) (Set.range g)) : ∃ (v : γ × (ℕ → β) → ↑unitInterval → β), Measurable (Function.uncurry v) ∧ MeasureTheory.Measure.map (fun (ω : Ω) => ((Z ω, fun (a : ℕ) => Y (e a) ω), fun (b : κ) => Y (g b) ω)) μ = MeasureTheory.Measure.map (fun (p : (γ × (ℕ → β)) × (κ → ↑unitInterval)) => (p.1, fun (b : κ) => v p.1 (p.2 b))) ((MeasureTheory.Measure.map (fun (ω : Ω) => (Z ω, fun (a : ℕ) => Y (e a) ω)) μ).prod (MeasureTheory.Measure.infinitePi fun (x : κ) => MeasureTheory.volume))

Coding a sequence exchangeable over a random element. Let Z be a random element and Y a sequence such that the pairs (Z, Y n) form an exchangeable sequence; equivalently, the law of Y is invariant under finite permutations jointly with Z. Then, along injective e and g with disjoint ranges, the coordinates along g are coded from Z and the coordinates along e by one measurable map applied to fresh i.i.d. uniform variables.

Conditioning on Z as well as on Y ∘ e is what the exchangeability over Z buys: the coded coordinates are conditionally i.i.d. given (Z, Y ∘ e), not merely given Y ∘ e.