de Finetti via Koopman operators and the shift-invariant σ-algebra

The summit of the Koopman route.

On path space the witness is invariantConditionalProbabilityMeasure, the conditional law of the first coordinate given MeasurableSpace.invariants (shift α). The block-cylinder mass computed in CylinderMass.lean is exactly the hypothesis conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral consumes, so the path-space statement follows at once; ConditionallyIIDWith.of_pathLaw carries it to an arbitrary space.

Main results

• ContractableLaw.conditionallyIIDWith_invariantConditionalProbabilityMeasure — the path-space form, with its witness;
• conditionallyIID_of_contractable_viaKoopman — a contractable process is conditionally i.i.d.;
• deFinetti_viaKoopman — an exchangeable process is conditionally i.i.d.

How this route differs from L²

The two routes are independent at the import level and stay that way: nothing here reaches DeFinetti/ViaL2. The mathematical difference is in what the block comparison rests on. The L² route compares two selections distributionally, as an a.e. identity of conditional expectations given the tail. This route uses actual invariance of the test event under the shift, and invariants_shift_lt_pathTail shows those σ-algebras genuinely differ — strictly, already over Bool. They are deliberately not unified into one σ-algebra-parametric theorem.

Both routes are finite-measure statements: these wrappers and deFinetti_viaL2 alike ask only for [IsFiniteMeasure μ]. Nothing in the Koopman chain needs more: the mean ergodic input and the witness are both finite-measure statements.

Source

No material is adapted from cameronfreer/exchangeability. Its Koopman development concludes the mixture identity; the results here package Tau Ceti's joint-law disintegration, and are assembled from this repository's own block transport, decoupling and factorization.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 5 (Koopman operators and invariant σ-algebras), whose milestone is deFinetti_viaKoopman.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1.

theorem TauCeti.Probability.ContractableLaw.conditionallyIIDWith_invariantConditionalProbabilityMeasure {α : Type u_2} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ContractableLaw ρ) : ConditionallyIIDWith ρ (fun (j : ℕ) (x : ℕ → α) => x j) (invariantConditionalProbabilityMeasure ρ)

The path-space form. A contractable path law is conditionally i.i.d. with the conditional law of the first coordinate given the shift-invariant σ-algebra as its witness.

theorem TauCeti.Probability.conditionallyIID_of_contractable_viaKoopman {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) : ConditionallyIID μ X

A contractable process is conditionally i.i.d., via the Koopman route.

theorem TauCeti.Probability.deFinetti_viaKoopman {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX : Exchangeable μ X) : ConditionallyIID μ X

de Finetti's theorem via Koopman operators. An exchangeable process on a nonempty standard Borel state space is conditionally i.i.d.