The finite-block factorization, via L²

For a contractable process on a standard Borel state space, the conditional law of any finite strictly monotone block, given the process tail, factorizes into the directing measure's marginals:

μ[blockIndicatorProd X k B | tailProcess X] =ᵐ[μ] ∏ i, (directingMeasure μ X ·).real (B i).

This is the single theorem the file provides. Integrating it over a tail event is what supplies hcore, the hypothesis of conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral, and hence ConditionallyIIDWith μ X (directingProbabilityMeasure μ X); that integration step is separate and does not live here.

Why this route exists

DeFinetti/BlockFactorization.lean proves the same factorization through the reverse martingale convergence theorem. This file reaches it from the L² averaging library instead, and imports neither that module nor TailFactorization, JointRectangle or Martingale.Convergence — the point of the viaL2 route is that the factorization does not need a martingale.

Two inputs meet, and neither knows about the other:

Selection invariance. Contractable.condExp_block_comp_tailProcess_ae_eq says the conditional law of a block given the tail is the same for every strictly monotone selection of that length. The tuples appearing in a product of disjoint-window block averages are exactly such selections — factor i reads its own window, and the windows are ordered, so window_lt_window makes each tuple strictly monotone.

Averaging. prod_blockAverage_window_eq_expect writes a product of disjoint-window block averages as a plain average over those tuples, so conditioning it on the tail returns the single common value. Meanwhile the same product converges in L¹ to ∏ i, (directingMeasure ω).real (B i) by the disjoint-window convergence theorem in ViaL2/WindowProduct.lean. A constant sequence that converges must equal its limit, which is the factorization.

Relation to the martingale route

DeFinetti/BlockFactorization.lean proves condExp_blockIndicatorProd_prefix_ae_eq_prod_directingMeasure, the same factorization for the prefix selection, through TailFactorization and reverse-martingale convergence. The overlap is intentional: the two are the corresponding steps of the two roadmap routes. Their names record the difference in what they say — _prefix_ against _strictMono_ — rather than how they are proved; the roadmap's _viaL2 route suffix is reserved for the public route endpoints.

This statement is strictly stronger than the prefix form: it holds for every strictly monotone selection, not only i ↦ i, and does not assume StandardBorelSpace Ω. So the implication does run one way — specializing k to fun i : Fin r => (i : ℕ) turns this into the prefix statement, and any module importing this one can derive it (its StandardBorelSpace Ω hypothesis then being unused). The converse is unavailable, the prefix form being weaker.

What separate proofs buy is therefore not logical independence but independent import closures. A single Lean declaration carries a single proof and a single import closure, so making this theorem the canonical source of the prefix statement would put the L² averaging library beneath the martingale route. The genuinely shared ingredients — tail-conditioned selection invariance, directing-measure integrability, the ℝ≥0∞ conversion — are already factored into neutral modules that both routes import.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 3 — the martingale-free standard-Borel de Finetti route, deFinetti_viaL2.
• Not adapted from the pinned cameronfreer/exchangeability sources: the argument here is built from this repository's L² averaging library and its tail-conditioned selection invariance, and deliberately diverges from that development's ViaL2 material.

theorem TauCeti.Probability.Contractable.condExp_blockIndicatorProd_strictMono_tailProcess_ae_eq_prod_directingMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r : ℕ} {k : Fin r → ℕ} (hk : StrictMono k) {B : Fin r → Set α} (hB : ∀ (i : Fin r), MeasurableSet (B i)) : μ[blockIndicatorProd X k B | tailProcess X] =ᵐ[μ] fun (ω : Ω) => ∏ i : Fin r, (directingMeasure μ X ω).real (B i)

The finite-block factorization, conditionally on the tail. For a contractable process on a standard Borel state space and any strictly monotone block k, the conditional expectation of ∏ i, 𝟙_{B i} ∘ X (k i) given tailProcess X is the product of the directing measure's marginals.