Factorizing a whole block over an invariant event

Iterating the one-coordinate decoupling across a block of length r.

The inductive step takes a block of length r + 1 and peels its last coordinate, replacing 𝟙_{B_r}(x_r) — the factor at index Fin.last r — by its conditional expectation given the shift-invariant σ-algebra, leaving a block of length r. The factors already peeled do not vanish: they accumulate as an invariants-measurable weight, which is exactly what the weighted decoupling chain carries.

Main results

All three in the ContractableLaw namespace:

• setIntegral_weight_mul_blockIndicatorProd_prefix_eq_prod_condExp — the induction, in conditional-expectation form, against an invariants-measurable weight;
• setIntegral_weight_mul_blockIndicatorProd_prefix_eq_prod_invariantConditionalProbabilityMeasure — the same with each conditional expectation replaced by the invariant conditional law it computes;
• setIntegral_blockIndicatorProd_prefix_eq_prod_invariantConditionalProbabilityMeasure — its w = 1 specialisation, which is the form a cylinder-mass computation consumes.

Why the conditional expectation, not the witness

The induction carries its accumulated factors as the weight of the next step, and the weighted transport demands a weight that is strictly measurable for MeasurableSpace.invariants (shift α). A conditional expectation is, by stronglyMeasurable_condExp. The invariant conditional law ν(B) is only characterised up to a null set, so it cannot serve. Conversion happens once, at the end.

Everything stays in ℝ; the crossing to ℝ≥0∞ belongs to the common ending, not here.

Relation to the other BlockFactorization files

DeFinetti/BlockFactorization.lean and DeFinetti/ViaL2/BlockFactorization.lean prove the corresponding step for the martingale and L² routes, conditioning on the tail rather than on the shift-invariant σ-algebra. Nothing is shared: the two σ-algebras can differ, with invariants_shift_lt_pathTail witnessing strictness over Bool-valued paths, and this file imports neither.

Source

The Koopman route follows Kallenberg's first proof (see References). No material is adapted from cameronfreer/exchangeability; the induction here is assembled from this repository's own weighted decoupling chain in ViaKoopman/Decoupling.lean.

References

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

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

A block factorizes over an invariant event, in conditional-expectation form.

Peeling the last coordinate replaces 𝟙_{B_r}(x_r) by its conditional expectation given the shift-invariant σ-algebra; the factors already peeled ride along as the weight of the next step, which is why the whole chain is stated against one.

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

The block factorization, with the factors named as the invariant conditional law.

The conditional expectations of the theorem above are replaced by the invariant conditional law they compute. The weight is unchanged: the conversion is a pointwise a.e. identity between the factors, so it does not care what multiplies them.

theorem TauCeti.Probability.ContractableLaw.setIntegral_blockIndicatorProd_prefix_eq_prod_invariantConditionalProbabilityMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ContractableLaw ρ) {A : Set (ℕ → α)} (hA : MeasurableSet A) (r : ℕ) (B : Fin r → Set α) (hB : ∀ (i : Fin r), MeasurableSet (B i)) : ∫ (x : ℕ → α) in A, ∏ i : Fin r, (B i).indicator (fun (x : α) => 1) (x ↑i) ∂ρ = ∫ (x : ℕ → α) in A, ∏ i : Fin r, (↑(invariantConditionalProbabilityMeasure ρ x)).real (B i) ∂ρ

The unweighted form, which is what a cylinder-mass computation consumes: the w = 1 specialisation of the theorem above.