Prefix-deletion conditional-expectation identity (Kallenberg 1.3 input)

For a contractable process X, this file proves the "prefix-deletion" conditional-expectation identity feeding the de Finetti martingale route: for r ≤ m and a measurable B,

μ[𝟙_{(X r)⁻¹ B} | σ(U) ⊔ σ(W)] =ᵐ[μ] μ[𝟙_{(X r)⁻¹ B} | σ(W)],

where U ω = (X 0 ω, …, X (r-1) ω) is the length-r prefix and W = processShift X (m+1) is the far tail from time m+1. Informally, X r is conditionally independent of the prefix given the far tail, so conditioning the X r-indicator on σ(U) ⊔ σ(W) collapses to conditioning on σ(W).

Main results

The public interface consists of two theorems:

• Contractable.condIndep_coord_prefix_tail — the primary conditional-independence statement: for a contractable process and r ≤ m, X r is conditionally independent of the prefix U given the far tail W = processShift X (m+1), packaged as a ProbabilityTheory.CondIndep object.
• Contractable.condExp_indicator_prefix_sup_tail_eq — the prefix-deletion drop-info identity read off from that conditional independence: for r ≤ m and a measurable B, μ[𝟙_{(X r)⁻¹ B} | σ(U) ⊔ σ(W)] =ᵐ μ[𝟙_{(X r)⁻¹ B} | σ(W)].

The contractability-specific pair-law equality feeding the argument is internal proof machinery, kept private to this module. The generic contraction-independence (Kallenberg 1.3) L² engine and the conditional-independence projection step are imported from TauCeti.Probability.Independence.Conditional.

Adapted from cameronfreer/exchangeability (DeFinetti/ViaMartingale/PairLawEquality.lean, Probability/TripleLawDropInfo/*, Probability/CondIndep/*).

The two reindexing maps

Prefix-tail split as a measurable equivalence

Pair-law equality from contractability

Conditional independence and the prefix-deletion identity (main target)

theorem TauCeti.Probability.Contractable.condIndep_coord_prefix_tail {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m : ℕ} (hrm : r ≤ m) : have U := fun (ω : Ω) (i : Fin r) => X (↑i) ω; let W := processShift X (m + 1); ProbabilityTheory.CondIndep (MeasurableSpace.comap W inferInstance) (MeasurableSpace.comap (X r) inferInstance) (MeasurableSpace.comap U inferInstance) ⋯ μ

Prefix/tail conditional independence. For a contractable process and r ≤ m, the value X r is conditionally independent of the length-r prefix U given the far tail W = processShift X (m+1), packaged as Mathlib's ProbabilityTheory.CondIndep object. This is the primary result; the prefix-deletion drop-info identity is read off from it below.

theorem TauCeti.Probability.Contractable.condExp_indicator_prefix_sup_tail_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω] [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hContr : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r m : ℕ} (hrm : r ≤ m) {B : Set α} (hB : MeasurableSet B) : have Y := X r; have U := fun (ω : Ω) (i : Fin r) => X (↑i) ω; have W := processShift X (m + 1); μ[(Y ⁻¹' B).indicator fun (x : Ω) => 1 | MeasurableSpace.comap U inferInstance ⊔ MeasurableSpace.comap W inferInstance] =ᵐ[μ] μ[(Y ⁻¹' B).indicator fun (x : Ω) => 1 | MeasurableSpace.comap W inferInstance]

Prefix-deletion conditional-expectation identity. For a contractable process and r ≤ m, conditioning the indicator of X r on σ(U) ⊔ σ(W) equals conditioning on σ(W), where U is the length-r prefix and W = processShift X (m+1) is the far tail. This is read off from the prefix/tail conditional independence Contractable.condIndep_coord_prefix_tail.