The conditional summit from contractability

A contractable process valued in a nonempty standard Borel space is conditionally i.i.d.: there is a directing measure given which every finite distinct block is i.i.d., as a joint-law disintegration.

Main results

• conditionallyIIDWith_of_contractable_pathSpace — the summit on path space, at the canonical directing measure. DeFinetti/Theorem.lean derives the sample-space form from it.

Implementation

The predicate ConditionallyIIDWith asks for a joint-law identity, so the block identities of the mixture route are not enough: the directing measure must survive alongside the block. Three layers supply that, all private.

The set-integral identity. The mass on the tail event ν ⁻¹' S meeting a prefix block cylinder is the integral of the directing-measure product over that event. Since ν is tailProcess-measurable, ν ⁻¹' S is a tail event, so setIntegral_condExp may be tested against it and the prefix factorization replaces the conditional expectation. The real/ℝ≥0∞ conversion it runs on is DirectingMeasure/Integral.lean, shared with BlockFactorization.

Symmetry transport. A finitely supported permutation realising an injective selection on the initial segment carries the prefix identity to that selection. It fixes ν, because tail events lie in the exchangeable σ-algebra, and it preserves the measure, because contractability gives exchangeability — so the directing-measure event rides along untouched. This needs no sorting of the selection: the permutation realises arbitrary injective selections directly.

Path space. Both of the above run on ℕ → α, which is standard Borel whenever α is. That is what keeps [StandardBorelSpace Ω] out of the exported statement: conditionallyIID_of_conditionallyIID_pathLaw carries the conclusion back to an arbitrary sample space.

The joint rectangles are then fed to conditionallyIID_of_jointRectangles.

This advances TauCetiRoadmap/Exchangeability/README.md, Layer 6 — the conditional summit.

Sources

The mathematical theorem is Kallenberg, Probabilistic Symmetries and Invariance Principles (2005), Theorem 1.1, in its conditional form.

The joint-law upgrade formalized here is new to this development. cameronfreer/exchangeability proves a conditionallyIID_bind_of_contractable, but under that repository's legacy naming ConditionallyIID denotes the mixture identity — what TauCeti calls MixedIID — so it establishes a strictly weaker statement, already available here as mixedIID_of_contractable. The directing-measure joint-rectangle factorization and its symmetry transport were built from TauCeti's own tail-factorization and exchangeable-σ-algebra API; no material is adapted.

theorem TauCeti.Probability.conditionallyIIDWith_of_contractable_pathSpace {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ fun (j : ℕ) (x : ℕ → α) => x j) : ConditionallyIIDWith μ (fun (j : ℕ) (x : ℕ → α) => x j) (directingProbabilityMeasure μ fun (j : ℕ) (x : ℕ → α) => x j)

The conditional summit on path space, at the canonical directing measure. A contractable coordinate process on a standard Borel state space is conditionally i.i.d. with witness the tail conditional law directingProbabilityMeasure.

Stated at the named witness rather than existentially: the directing measure is the object the conditional predicate is about, so discarding it would lose the identity downstream users need.