Block averages of an indicator converge to the directing measure

Contractable.tendsto_integral_abs_blockAverage_sub_condExp identifies the L¹ limit of the block averages of an observable with μ[f ∘ X 0 | tailProcess X], along any selection that is injective for all sufficiently large lengths — the selection may move with the length. directingMeasure_ae_eq_condExp identifies ω ↦ (directingMeasure μ X ω).real B with the same conditional expectation when the observable is the indicator 𝟙_B. Composing the two gives the statement in the form the L² route consumes: the empirical averages of 𝟙_B ∘ X converge in L¹ to the directing measure's evaluation at B.

Fixed-start windows (fixedStart r) and disjoint windows (disjointWindow c) are both instances. The disjoint ones are what a finite-block factorization needs, and fixed starts cannot supply them: windows from two distinct fixed starts overlap once the common length exceeds the gap between the starts. The limit does not depend on the selection, so every one of them converges to the same directing-measure evaluation.

The point is that no directing measure is constructed here. directingMeasure is Mathlib's condDistrib conditioned on tailProcess X, which the martingale route also uses but does not own; this file only observes that the L² averaging limit lands on it.

theorem TauCeti.Probability.Contractable.tendsto_integral_abs_blockAverage_indicator_sub_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)) {B : Set α} (hB : MeasurableSet B) (k : (n : ℕ) → Fin (n + 1) → ℕ) (hk : ∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (k n)) : Filter.Tendsto (fun (m : ℕ) => ∫ (ω : Ω), |blockAverage (fun (i : ℕ) (ω : Ω) => B.indicator (fun (x : α) => 1) (X i ω)) (k m) ω - (directingMeasure μ X ω).real B| ∂μ) Filter.atTop (nhds 0)

The block averages of an indicator converge to the directing measure. For a contractable process on a standard Borel state space and a measurable set B, the block averages of 𝟙_B ∘ X along any eventually-injective selection converge in L¹ to ω ↦ (directingMeasure μ X ω).real B.

The selection may move with the length, so this covers the disjoint windows a block factorization needs as well as fixed-start ones; the limit is the same for every selection.