The Cesàro limit of an observable of a contractable process is tail-measurable

Layer 3 of the Exchangeability roadmap reaches weighted_sums_converge_L1_of_memLp: the block averages of a square-integrable observable of a contractable process converge in L¹ to a common limit, along every eventually-injective selection — fixed-start windows and disjoint windows alike. That limit is produced as an abstract L¹ limit, so nothing about where it lives comes for free.

Contractable.exists_tailProcess_measurable_cesaro_limit_of_memLp shows the limit has a tailProcess X-measurable representative, with …_cesaro_limit the bounded-observable corollary.

This file's responsibility is measurability of the limit, deliberately separate from identifying what the limit is: Exchangeability.L2.Cesaro.ToCondExp identifies it with μ[f ∘ X 0 | tailProcess X]. Keeping the two apart is what lets the measurability argument avoid the reverse-martingale theorem entirely.

The argument does not use the reverse-martingale convergence theorem tendsto_ae_condExp_iInf of Layer 4, which is what distinguishes this route from the martingale one. The window starting at r is tailFamily X r-measurable; L¹ convergence gives an a.e.-convergent subsequence, so the limit is AEStronglyMeasurable[tailFamily X r] for every r, and tailProcess X is exactly the infimum of that antitone family.

The roadmap maps Exchangeability/Bridge/CesaroToCondExp.lean in cameronfreer/exchangeability (pin e0532e59ceff23edab44dda9ab0655debbc9cc22) as a Layer 3 source. This file is not adapted from it: the tail-measurability step is assembled from Tau Ceti's existing general helpers aestronglyMeasurable_of_tendsto_ae' and aestronglyMeasurable_iInf_of_antitone (themselves adapted from that repository's Probability/SigmaAlgebraHelpers.lean, and carrying attribution there), rather than by porting a bridge file. The divergence is deliberate: separating tail measurability from the conditional-expectation identification keeps this prerequisite independent of the directing measure.

theorem TauCeti.Probability.Contractable.exists_tailProcess_measurable_cesaro_limit_of_memLp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (i : ℕ), AEMeasurable (X i) μ) {f : α → ℝ} (hf : Measurable f) (hf_L2 : MeasureTheory.MemLp (fun (ω : Ω) => f (X 0 ω)) 2 μ) : ∃ (a : Ω → ℝ), Measurable a ∧ MeasureTheory.MemLp a 1 μ ∧ ∀ (k : (n : ℕ) → Fin (n + 1) → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (k n)) → Filter.Tendsto (fun (m : ℕ) => ∫ (ω : Ω), |blockAverage (fun (i : ℕ) (ω : Ω) => f (X i ω)) (k m) ω - a ω| ∂μ) Filter.atTop (nhds 0)

The Cesàro limit lives on the tail. For a measurable observable f whose composite with a single coordinate is square-integrable, the common L¹ limit of the moving injective block averages supplied by weighted_sums_converge_L1_of_memLp has a tailProcess X-measurable representative.

The limit is the same function for every selection, so the conclusion carries the general form through; fixed starts are only used inside the proof, where placing the limit on tailFamily X r needs a window that begins at r.

theorem TauCeti.Probability.Contractable.exists_tailProcess_measurable_cesaro_limit {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (i : ℕ), AEMeasurable (X i) μ) {f : α → ℝ} (hf : Measurable f) (hf_bdd : ∃ (C : ℝ), ∀ (x : α), ‖f x‖ ≤ C) : ∃ (a : Ω → ℝ), Measurable a ∧ MeasureTheory.MemLp a 1 μ ∧ ∀ (k : (n : ℕ) → Fin (n + 1) → ℕ), (∀ᶠ (n : ℕ) in Filter.atTop, Function.Injective (k n)) → Filter.Tendsto (fun (m : ℕ) => ∫ (ω : Ω), |blockAverage (fun (i : ℕ) (ω : Ω) => f (X i ω)) (k m) ω - a ω| ∂μ) Filter.atTop (nhds 0)

Bounded-observable form. A uniform bound gives square-integrability of the composite on a finite measure space, so this is the direct entry point for bounded observables — matching the shape in which weighted_sums_converge_L1 states the underlying convergence.