The block-cylinder mass, in the shape the common ending consumes

The Koopman route's pieces assembled into the single hypothesis that conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral asks for.

The block reduction moves an arbitrary strictly increasing selection onto the prefix; the block factorization turns the prefix cylinder's mass into an integral of a product of conditional expectations; naming those as the invariant conditional law and crossing once into ℝ≥0∞ gives the identity.

Main results

• ContractableLaw.measure_inter_blockCylinder_eq_setLIntegral_of_measurableSet_invariants — over any shift-invariant event, the block-cylinder mass is the integral of the product of the invariant conditional law's values.

A consumer wanting the hcore hypothesis of conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral applies this to a witness event, whose invariance is measurable_invariants_invariantConditionalProbabilityMeasure.

The crossing to ℝ≥0∞ happens exactly once, here, through the route-neutral TauCeti.MeasureTheory.ofReal_integral_prod_toReal_eq_lintegral_prod; everything upstream is real-valued. Integrability of the witness product is obtained from the conditional-expectation product it is a.e. equal to, which avoids needing measurability of the witness evaluation directly.

Source

The Koopman route follows Kallenberg's first proof (see References). No material is adapted from cameronfreer/exchangeability; this assembles Tau Ceti's own block reduction, block factorization and ℝ≥0∞ bridge.

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.measure_inter_blockCylinder_eq_setLIntegral_of_measurableSet_invariants {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (hρ : ContractableLaw ρ) {r : ℕ} {k : Fin r → ℕ} (hk : StrictMono k) {A : Set (ℕ → α)} (hA_inv : MeasurableSet A) {B : Fin r → Set α} (hB : ∀ (i : Fin r), MeasurableSet (B i)) : ρ (A ∩ blockCylinder (fun (j : ℕ) (x : ℕ → α) => x j) k B) = ∫⁻ (x : ℕ → α) in A, ∏ i : Fin r, ↑(invariantConditionalProbabilityMeasure ρ x) (B i) ∂ρ

The block-cylinder mass over an invariant event. Over any shift-invariant event, the mass of a block cylinder is the integral of the product of the invariant conditional law's values on the coordinate sets.