Cesàro Pair Factorization via MET

This file proves the pair factorization lemma for conditional expectations using Mean Ergodic Theorem (MET) and exchangeability.

Main result:

• condexp_pair_factorization_MET: For exchangeable measures, CE[f(ω₀)·g(ω₁)|ℐ] factors into CE[f(ω₀)|ℐ]·CE[g(ω₀)|ℐ].

Proof strategy (CORRECTED - avoids false k=0 lag constancy):

1. Apply tower property directly on g₁ (via Cesàro from index 1): CE[f(ω₀)·g(ω₁)|ℐ] = CE[f(ω₀)·CE[g(ω₀)|ℐ]|ℐ] (uses h_tower_of_lagConst_from_one which only needs k ≥ 1 lag constancy)
2. Apply pull-out property: CE[f(ω₀)·CE[g(ω₀)|ℐ]|ℐ] = CE[g(ω₀)|ℐ]·CE[f(ω₀)|ℐ] (CE[g(ω₀)|ℐ] is ℐ-measurable)

Key insight: This requires EXCHANGEABILITY (via hExch), not just stationarity.

Split from: CesaroConvergence.lean (lines 1561-2014)

Local notation

theorem Exchangeability.DeFinetti.ViaKoopman.condexp_pair_factorization_MET {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure Ω[α]} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [Nonempty α] (hσ : MeasureTheory.MeasurePreserving PathSpace.shift μ μ) (hExch : ∀ (π : Equiv.Perm ℕ), MeasureTheory.Measure.map (reindex π) μ = μ) (f g : α → ℝ) (hf_meas : Measurable f) (hf_bd : ∃ (C : ℝ), ∀ (x : α), |f x| ≤ C) (hg_meas : Measurable g) (hg_bd : ∃ (C : ℝ), ∀ (x : α), |g x| ≤ C) : μ[fun (ω : Ω[α]) => f (ω 0) * g (ω 1)|shiftInvariantSigma] =ᵐ[μ] fun (ω : Ω[α]) => μ[fun (ω : Ω[α]) => f (ω 0)|shiftInvariantSigma] ω * μ[fun (ω : Ω[α]) => g (ω 0)|shiftInvariantSigma] ω

Pair factorization via MET + Exchangeability (Kallenberg's approach).

For EXCHANGEABLE measures μ on path space, the conditional expectation of f(ω₀)·g(ω₁) given the shift-invariant σ-algebra factors into the product of the individual conditional expectations.

Proof strategy (CORRECTED - avoids false k=0 lag constancy):

1. Apply tower property directly on g₁ (via Cesàro from index 1): CE[f(ω₀)·g(ω₁)|ℐ] = CE[f(ω₀)·CE[g(ω₀)|ℐ]|ℐ] (uses h_tower_of_lagConst_from_one which only needs k ≥ 1 lag constancy)
2. Apply pull-out property: CE[f(ω₀)·CE[g(ω₀)|ℐ]|ℐ] = CE[g(ω₀)|ℐ]·CE[f(ω₀)|ℐ] (CE[g(ω₀)|ℐ] is ℐ-measurable)

Key insight: This requires EXCHANGEABILITY (via hExch), not just stationarity. The original k=0 lag constancy approach was FALSE. See Infrastructure.lean for details.