Indicator form of the conditional law of a contractable coordinate

TauCeti.Probability.Exchangeability.CondExp shows that for a contractable process X the conditional expectations of f ∘ X j and f ∘ X k given the future — or given the process tail — agree, for an arbitrary measurable real observable f. This file records the indicator specializations Contractable.condExp_indicator_future_eq and Contractable.condExp_indicator_tailProcess_eq, which are the shape the de Finetti directing-measure construction and the finite-block factorizations consume.

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_indicator_future_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) {B : Set α} (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ X j | tailFamily X r] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X k | tailFamily X r]

Indicator form of Contractable.condExp_comp_future_ae_eq, the shape the finite-block factorizations use.

theorem TauCeti.Probability.Contractable.condExp_indicator_tailProcess_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 : ℕ} {B : Set α} (hB : MeasurableSet B) : μ[(B.indicator fun (x : α) => 1) ∘ X j | tailProcess X] =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X k | tailProcess X]

Indicator form of Contractable.condExp_comp_tailProcess_ae_eq, the shape the directing-measure construction uses.