Finite exchangeability as sampling without replacement

This file identifies every shorter marginal of a finite exchangeable process with sampling without replacement from its observed finite population.

The general sampling laws and their collision bounds live in TauCeti.Probability.PopulationSampling.Finite. Given a population law ρ : Measure (κ → α), sampleWithoutReplacement ρ first draws x ∼ ρ, independently draws a uniform injective selection k : ι → κ, and returns x ∘ k.

The main theorem says that if the first n coordinates of a process are exchangeable, then sampling m ≤ n entries without replacement from that random n-tuple has exactly the original m-prefix law. This is the representation half of the finite de Finetti argument: the companion with-replacement law is the product of the empirical measure, and the collision estimate in TauCeti.Probability.UniformSampling then controls their difference.

The proof averages the exchangeable law over all injective selections. Every selection has the same law by ExchangeableAt.blockLaw_eq_prefixLaw_of_injective, so the average has that law too.

Main declarations

• ExchangeableAt.sampleWithoutReplacement_eq_prefixLaw — the finite exchangeable without-replacement representation.

References

• P. Diaconis and D. Freedman, “Finite exchangeable sequences”, Annals of Probability 8 (1980), 745–764.

No material is adapted from cameronfreer/exchangeability; its three de Finetti routes concern infinite exchangeable sequences rather than quantitative finite approximation.

theorem TauCeti.Probability.ExchangeableAt.sampleWithoutReplacement_eq_prefixLaw {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {m n : ℕ} (h : ExchangeableAt μ X n) (hmn : m ≤ n) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) : sampleWithoutReplacement (prefixLaw μ X n) = prefixLaw μ X m

Finite exchangeability is sampling without replacement. If the first n coordinates are exchangeable, then drawing m ≤ n distinct positions uniformly from that random n-tuple has exactly the law of the first m coordinates.

This is an equality of measures, not merely an eventwise bound. The later finite de Finetti bound compares its left-hand side with sampling with replacement, using the collision estimate in UniformSampling.lean.