The Cesàro limit of an observable is its conditional expectation given the process tail

Layer 3 of the Exchangeability roadmap produces the Cesàro limit of an observable of a contractable process twice over: weighted_sums_converge_L1_of_memLp gives it as an abstract L¹ limit, and Contractable.exists_tailProcess_measurable_cesaro_limit_of_memLp places it on the process tail tailProcess X. Neither says what the limit is.

This file identifies it:

• Contractable.condExp_blockAverage_tailProcess_ae_eq — every block average of f ∘ X has the same conditional expectation given tailProcess X as the single coordinate f ∘ X 0;
• Contractable.tendsto_integral_abs_blockAverage_sub_condExp_of_memLp — the block averages converge in L¹ to μ[f ∘ X 0 | tailProcess X] along every eventually injective moving selection, fixed starts (fixedStart) and disjoint windows (disjointWindow) alike, with Contractable.tendsto_integral_abs_blockAverage_sub_condExp the bounded-observable form;
• Contractable.ae_eq_condExp_tailProcess_of_tendsto_integral_abs — consequently any L¹ limit of those block averages, along any eventually injective selection, is a.e. that conditional expectation.

Both ingredients are already in place, and the argument is short. Contractability makes all coordinates share a conditional law given the tail (Contractable.condExp_comp_tailProcess_ae_eq), so the conditional expectation of every window is μ[f ∘ X 0 | tailProcess X]; the limit is tail-measurable, hence its own conditional expectation; and conditional expectation is L¹-continuous (TauCeti.MeasureTheory.condExp_ae_eq_of_forall_condExp_ae_eq_of_tendsto_eLpNorm). No reverse-martingale convergence theorem is used, which is what keeps this on the L² route rather than the martingale one.

The roadmap maps Exchangeability/Bridge/CesaroToCondExp.lean in cameronfreer/exchangeability (pin e0532e59ceff23edab44dda9ab0655debbc9cc22) as the Layer 3 source for this bridge. No material is ported from it: the identification here is assembled from Tau Ceti's own tail-measurability result and its L¹-continuity lemma, and it conditions on the process tail tailProcess X throughout.

theorem TauCeti.Probability.Contractable.condExp_blockAverage_tailProcess_ae_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), Measurable (X i)) {f : α → ℝ} (hf : Measurable f) (hf_int : MeasureTheory.Integrable (fun (ω : Ω) => f (X 0 ω)) μ) {n : ℕ} (k : Fin (n + 1) → ℕ) : μ[blockAverage (fun (i : ℕ) (ω : Ω) => f (X i ω)) k | tailProcess X] =ᵐ[μ] μ[fun (ω : Ω) => f (X 0 ω) | tailProcess X]

Block averages do not move the conditional expectation given the tail. For a contractable process all coordinates share a conditional law given tailProcess X, so the conditional expectation of the average of any nonempty finite block of f ∘ X is the conditional expectation of a single coordinate.

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

The block averages converge to a conditional expectation. For a measurable observable f whose composite with a single coordinate is square-integrable, the block averages of f ∘ X along a contractable process converge in L¹ to μ[f ∘ X 0 | tailProcess X], for every selection k that is injective for all sufficiently large lengths — the selection may move with the length.

This is the identification the Layer 3 route needs: the limit supplied by weighted_sums_converge_L1_of_memLp is not merely tail-measurable, it is the conditional expectation of a single coordinate given the tail.

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

Bounded-observable form. A uniform bound gives square-integrability of the composite on a finite measure space, matching the entry point of weighted_sums_converge_L1.

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

Any L¹ limit of the block averages is the conditional expectation. The identification form: along any eventually injective selection, an L¹ limit is a.e. unique, so it must be the conditional expectation the windows already converge to.