Conditional law of a contractable selection given the tail

For a contractable process X, the conditional law of a selection of coordinates given the future, or given the tail, does not depend on which coordinates were selected. Four results, stated for an arbitrary measurable real observable f:

• Contractable.condExp_block_comp_future_ae_eq — for two strictly monotone blocks of the same length lying below a cutoff c, the conditional expectations of f along each block, given the future σ-algebra tailFamily X c, agree a.e.
• Contractable.condExp_comp_future_ae_eq — its single-coordinate case, for heads j, k below the cutoff.
• Contractable.condExp_block_comp_tailProcess_ae_eq — the block form conditioning on the process tail tailProcess X.
• Contractable.condExp_comp_tailProcess_ae_eq — its single-coordinate case, the "extreme members agree on the tail" step.

The block forms are what a route needs in order to replace one selection by another underneath a tail conditioning. The mechanism is distributional: both selections are appended to the same future, and contractability equates the joint laws. Nothing here makes a tail event invariant under reindexing.

All are facts about contractable processes alone, so they live in the shared exchangeability layer: the L² route's Cesàro bridge consumes the general form, while the indicator specializations the de Finetti directing-measure construction consumes are in TauCeti.Probability.DeFinetti.CondExpConvergence.

Adapted from cameronfreer/exchangeability (DeFinetti/ViaMartingale/CondExpConvergence.lean, condexp_convergence and extreme_members_equal_on_tail_via_tower, pin e0532e59ceff23edab44dda9ab0655debbc9cc22).

theorem TauCeti.Probability.Contractable.condExp_block_comp_future_ae_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r c : ℕ} {k l : Fin r → ℕ} (hk : StrictMono k) (hl : StrictMono l) (hkc : ∀ (i : Fin r), k i < c) (hlc : ∀ (i : Fin r), l i < c) {f : (Fin r → α) → ℝ} (hf : Measurable f) : μ[fun (ω : Ω) => f fun (i : Fin r) => X (k i) ω | tailFamily X c] =ᵐ[μ] μ[fun (ω : Ω) => f fun (i : Fin r) => X (l i) ω | tailFamily X c]

Future-conditioned selection invariance for finite blocks. Two strictly monotone selections of the same length, both lying below a cutoff c, have the same conditional law given the future tailFamily X c.

theorem TauCeti.Probability.Contractable.condExp_block_comp_tailProcess_ae_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r : ℕ} {k l : Fin r → ℕ} (hk : StrictMono k) (hl : StrictMono l) {f : (Fin r → α) → ℝ} (hf : Measurable f) : μ[fun (ω : Ω) => f fun (i : Fin r) => X (k i) ω | tailProcess X] =ᵐ[μ] μ[fun (ω : Ω) => f fun (i : Fin r) => X (l i) ω | tailProcess X]

Tail-conditioned selection invariance for finite blocks. For a contractable process, any two strictly monotone selections of the same length have the same conditional law given the process tail.

The mechanism is distributional, not pointwise: nothing here asserts that a tail event is invariant under reindexing — it is not.

theorem TauCeti.Probability.Contractable.condExp_comp_future_ae_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {r j k : ℕ} (hj : j < r) (hk : k < r) {f : α → ℝ} (hf : Measurable f) : μ[fun (ω : Ω) => f (X j ω) | tailFamily X r] =ᵐ[μ] μ[fun (ω : Ω) => f (X k ω) | tailFamily X r]

Conditional law of head coordinates given the future. For a contractable process and two head indices j, k below a cutoff r, the conditional expectations of f ∘ X j and f ∘ X k given the future σ-algebra tailFamily X r agree almost everywhere.

The single-coordinate case of Contractable.condExp_block_comp_future_ae_eq.

theorem TauCeti.Probability.Contractable.condExp_comp_tailProcess_ae_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) {j k : ℕ} {f : α → ℝ} (hf : Measurable f) : μ[fun (ω : Ω) => f (X j ω) | tailProcess X] =ᵐ[μ] μ[fun (ω : Ω) => f (X k ω) | tailProcess X]

Extreme members agree on the tail. For a contractable process and arbitrary coordinates j, k, the conditional expectations of f ∘ X j and f ∘ X k given the process tail σ-algebra tailProcess X agree almost everywhere.

The single-coordinate case of Contractable.condExp_block_comp_tailProcess_ae_eq: a one-element selection is vacuously strictly monotone.