Simultaneous convergence of a product of indicator block averages

For a contractable process on a standard Borel state space, the block averages of finitely many indicators over pairwise disjoint windows converge in L¹, simultaneously, to the product of the corresponding directing-measure evaluations:

∫ |∏ i, blockAverage 𝟙_{B i} (window (n+1) i) - ∏ i, (directingMeasure ω).real (B i)| dμ → 0.

The selections are disjointWindow i, so factor i occupies [(i+1)(n+1), (i+2)(n+1)). Distinct factors never collide (disjointWindow_ne), and the windows move outward as the length grows — which is exactly what fixed starts cannot do, since windows from distinct fixed starts overlap once the common length exceeds the gap between the starts.

Two ingredients meet here.

Each factor converges. The indicator-to-directing-measure convergence in ViaL2/EmpiricalToDirecting.lean accepts any eventually-injective moving selection. The general theorem below therefore takes an arbitrary family of such selections; cross-factor disjointness is not needed for the convergence, only for what the terms mean downstream. The limit does not depend on the selection, so all m factors converge to their directing-measure evaluations against the same directing measure.

The product follows. tendsto_integral_norm_prod_sub_prod turns finitely many L¹ convergences into convergence of the product, and indicators supply the unit-ball bounds it needs on both sides.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 3 — the simultaneous disjoint-window product convergence that the finite-block conditional factorization consumes.

theorem TauCeti.Probability.Contractable.tendsto_integral_abs_prod_blockAverage_indicator_sub_prod_directingMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) {m : ℕ} (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) (k : Fin m → (n : ℕ) → Fin (n + 1) → ℕ) (hk : ∀ (i : Fin m), ∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (k i n)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |∏ i : Fin m, blockAverage (fun (c : ℕ) (ω : Ω) => (B i).indicator (fun (x : α) => 1) (X c ω)) (k i n) ω - ∏ i : Fin m, (directingMeasure μ X ω).real (B i)| ∂μ) Filter.atTop (nhds 0)

Simultaneous convergence of a product of indicator block averages. For a contractable process on a standard Borel state space and finitely many measurable sets B i, each read along its own selection k i, the product of the block averages converges in L¹ to the product of the directing-measure evaluations.

Only each selection's own eventual injectivity is used; nothing here needs the selections to be disjoint from one another. Disjointness matters for what the terms mean downstream, not for the convergence.

theorem TauCeti.Probability.Contractable.tendsto_integral_abs_prod_blockAverage_indicator_disjointWindow_sub_prod_directingMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) {m : ℕ} (B : Fin m → Set α) (hB : ∀ (i : Fin m), MeasurableSet (B i)) : Filter.Tendsto (fun (n : ℕ) => ∫ (ω : Ω), |∏ i : Fin m, blockAverage (fun (c : ℕ) (ω : Ω) => (B i).indicator (fun (x : α) => 1) (X c ω)) (disjointWindow (↑i) n) ω - ∏ i : Fin m, (directingMeasure μ X ω).real (B i)| ∂μ) Filter.atTop (nhds 0)

The disjoint-window instance. The block averages are of indicators, as in the general theorem above; reading factor i along disjointWindow i keeps distinct factors in disjoint blocks at every length, which is the configuration a finite-block factorization consumes.