Displacing the last coordinate of a block

The step that decouples one factor from a block, over an invariant event.

Appending the coordinate r + m to the prefix 0, 1, …, r - 1 gives a strictly increasing selection for every m, so the block transport makes the set-integral of the resulting product independent of m. Averaging over m < n therefore leaves the left-hand side unchanged while turning the right-hand side into a Birkhoff average of 𝟙_B ∘ (· r) under the shift — which is where the mean ergodic theorem enters.

Source

The Koopman route to de Finetti follows Kallenberg's first proof (see References). No material is adapted from cameronfreer/exchangeability: that development carries its own ViaKoopman subtree covering this argument, but the lemmas here are assembled from Tau Ceti's own pieces — the invariant block transport of PathSpace/Invariant/BlockTransport.lean, the L¹ mean ergodic bridge of Ergodic/CondExpProjection.lean, and the invariant conditional law of ViaKoopman/InvariantConditionalLaw.lean.

References

• O. Kallenberg, Probabilistic Symmetries and Invariance Principles, Springer, 2005, Chapter 1, Theorem 1.1.

Main results

• ContractableLaw.condExp_indicator_coord_ae_eq_invariantConditionalProbabilityMeasure — the invariant conditional law computes the conditional expectation of every coordinate indicator, not just the first;
• ContractableLaw.setIntegral_weight_mul_prefix_mul_indicator_eq_condExp — over an invariant event, the weighted integral of 𝟙_B at coordinate r equals the weighted integral of its conditional expectation given the shift-invariant σ-algebra. This form needs no standard-Borel hypothesis;
• setIntegral_weight_mul_prefix_mul_indicator_eq_invariantConditionalProbabilityMeasure (same namespace) — and, where the witness exists, that limit is the invariant conditional law ν(B).

The transport and averaging stages behind these — the displacement identity, its Birkhoff-average form, the coordinate/Birkhoff bridge and the L¹ convergence — are private: they are steps of this file's argument, not API.

The displacement and averaging lemmas carry an invariants-measurable weight w, as do the two decoupling interfaces; the coordinate/Birkhoff bridge and the L¹ convergence do not, since neither mentions a weight. The weight is what makes the chain usable in an induction across a block: the factors already peeled off accumulate as exactly such a weight, which an unweighted form cannot express.

The limit passage itself is one private estimate, tendsto_setIntegral_mul_of_tendsto_integral_abs: L¹ convergence plus |p| ≤ 1 gives convergence of the weighted set-integrals. Keeping it separate localises the integrability obligations instead of rediscovering them inside the Koopman calculation.

The condExp form is the one an induction consumes, because stronglyMeasurable_condExp makes it strictly measurable for the invariants σ-algebra, which is what the weight hypothesis demands; the ν form is only an a.e. identity and cannot serve as a weight. Conversion happens once, at the end.

This is the engine of the Koopman factorization: the m-independence is what allows the average over m to be inserted for free, and that average is what the ergodic theorem consumes.

The induction on r that iterates this decoupling across a whole block is ViaKoopman/BlockFactorization.lean, and the ℝ≥0∞ ending it feeds is ViaKoopman/CylinderMass.lean.

theorem TauCeti.Probability.ContractableLaw.condExp_indicator_coord_ae_eq_invariantConditionalProbabilityMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ContractableLaw ρ) {B : Set α} (hB : MeasurableSet B) (r : ℕ) : ρ[fun (y : ℕ → α) => B.indicator (fun (x : α) => 1) (y r) | MeasurableSpace.invariants (shift α)] =ᵐ[ρ] fun (x : ℕ → α) => (↑(invariantConditionalProbabilityMeasure ρ x)).real B

The invariant conditional law computes every coordinate, not just the first. Combining the witness's characteristic property at coordinate 0 with the transport fact that all coordinates agree over invariant events. This is what lets the Birkhoff limit at coordinate r be named as the witness.

theorem TauCeti.Probability.ContractableLaw.setIntegral_weight_mul_prefix_mul_indicator_eq_condExp {α : Type u_1} [MeasurableSpace α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ContractableLaw ρ) {r : ℕ} {w : (ℕ → α) → ℝ} (hw : Measurable w) (hw_bdd : ∀ᵐ (x : ℕ → α) ∂ρ, |w x| ≤ 1) {g : (Fin r → α) → ℝ} (hg : Measurable g) (hg_bdd : ∀ (y : Fin r → α), |g y| ≤ 1) {B : Set α} (hB : MeasurableSet B) {A : Set (ℕ → α)} (hA : MeasurableSet A) : ∫ (x : ℕ → α) in A, w x * (g (prefixProj α r x) * B.indicator (fun (x : α) => 1) (x r)) ∂ρ = ∫ (x : ℕ → α) in A, w x * (g (prefixProj α r x) * ρ[fun (y : ℕ → α) => B.indicator (fun (x : α) => 1) (y r) | MeasurableSpace.invariants (shift α)] x) ∂ρ

The last coordinate decouples into the invariant conditional expectation. Over an invariant event, the weighted integral of 𝟙_B at coordinate r equals the weighted integral of its conditional expectation given the shift-invariant σ-algebra. No standard-Borel hypothesis is needed, since no witness is named; that is the following theorem.

Where the two halves meet: the averaged sequence is constant in n by ContractableLaw.setIntegral_weight_mul_prefix_mul_indicator_eq_birkhoffAverage, and the same sequence converges to the right-hand side by the L¹ mean ergodic theorem; a sequence has one limit.

theorem TauCeti.Probability.ContractableLaw.setIntegral_weight_mul_prefix_mul_indicator_eq_invariantConditionalProbabilityMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ContractableLaw ρ) {r : ℕ} {w : (ℕ → α) → ℝ} (hw : Measurable w) (hw_bdd : ∀ᵐ (x : ℕ → α) ∂ρ, |w x| ≤ 1) {g : (Fin r → α) → ℝ} (hg : Measurable g) (hg_bdd : ∀ (y : Fin r → α), |g y| ≤ 1) {B : Set α} (hB : MeasurableSet B) {A : Set (ℕ → α)} (hA : MeasurableSet A) : ∫ (x : ℕ → α) in A, w x * (g (prefixProj α r x) * B.indicator (fun (x : α) => 1) (x r)) ∂ρ = ∫ (x : ℕ → α) in A, w x * (g (prefixProj α r x) * (↑(invariantConditionalProbabilityMeasure ρ x)).real B) ∂ρ

Naming the limit as the invariant conditional law. The condExp form above says the last coordinate decouples; this says what it decouples into.