The mass of a directing-measure event met with a block cylinder

One lemma, the integration step shared by the routes that condition on the tail σ-algebra:

μ ((ν ⁻¹' S) ∩ blockCylinder X k B) = ∫⁻ ω in ν ⁻¹' S, ∏ i, directingMeasure μ X ω (B i) ∂μ

given the conditional factorization of the block along k. That factorization is a hypothesis, not a conclusion: this file proves none of it, and so depends on no route that establishes it. Each route supplies its own — the martingale route from TailFactorization, the L² route from ViaL2/BlockFactorization.lean — and both then instantiate this lemma. The Koopman route conditions on the shift-invariant σ-algebra and builds a different witness, so it does not reach this file at all.

That is the whole point of stating it this way. The routes are required to stay independent at the level of imports, so the shared material has to be the part that neither proves: here, the bookkeeping that turns an a.e. identity of conditional expectations into an identity of measures.

The argument is three steps. A directing-measure event is tail-measurable, so testing the factorization against it is setIntegral_condExp. The cylinder's mass is the integral of its indicator, which is integral_blockIndicatorProd read against the restricted measure. And the conversion to ℝ≥0∞ happens once, at the end, via ofReal_integral_eq_lintegral_prod_directingMeasure.

The result feeds conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral, whose hcore hypothesis it is in exactly this shape.

theorem TauCeti.Probability.measure_inter_blockCylinder_eq_setLIntegral_of_condExp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r : ℕ} {k : Fin r → ℕ} {B : Fin r → Set α} (hB : ∀ (i : Fin r), MeasurableSet (B i)) (hfac : μ[blockIndicatorProd X k B | tailProcess X] =ᵐ[μ] fun (ω : Ω) => ∏ i : Fin r, (directingMeasure μ X ω).real (B i)) {S : Set (MeasureTheory.ProbabilityMeasure α)} (hS : MeasurableSet S) : μ (directingProbabilityMeasure μ X ⁻¹' S ∩ blockCylinder X k B) = ∫⁻ (ω : Ω) in directingProbabilityMeasure μ X ⁻¹' S, ∏ i : Fin r, (directingMeasure μ X ω) (B i) ∂μ

The mass of a directing-measure event met with a block cylinder, given the conditional factorization of that block along k.

The factorization is a hypothesis, so this lemma is neutral between the routes that establish it. Note that neither Contractable μ X nor [StandardBorelSpace Ω] appears: both are needed only to produce hfac, never to integrate it.