Documentation

TauCeti.Probability.Exchangeability.PathSpace.Exchangeable.Sigma

Exchangeable σ-algebra on path space #

This file records the Layer 2 exchangeability-roadmap σ-algebra of path-space events invariant under finitely supported permutations of the time coordinate. It also relates the one-sided path tail σ-algebra to this exchangeable σ-algebra: a tail event is fixed by every finitely supported time permutation.

source
@[implicit_reducible]
def TauCeti.Probability.exchangeableSigma (α : Type u_3) [MeasurableSpace α] :
MeasurableSpace (ℕ → α)

The exchangeable σ-algebra on path space: ambient-measurable events invariant under every finitely supported permutation of the time coordinate.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.mem_exchangeableSigma_iff {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ → α)} :
    MeasurableSet s ↔ MeasurableSet s ∧ ∀ (π : Equiv.Perm ℕ), (MulAction.fixedBy ℕ π)ᶜ.Finite → permReindex π ⁻¹' s = s

    A set is measurable for exchangeableSigma iff it is ambient-measurable and fixed by every finitely supported time permutation.

    source
    theorem TauCeti.Probability.exchangeableSigma_le {α : Type u_1} [MeasurableSpace α] :
    exchangeableSigma α ≤ inferInstance

    The exchangeable σ-algebra is a sub-σ-algebra of the ambient path-space σ-algebra.

    source
    theorem TauCeti.Probability.measurableSet_exchangeableSigma_of_forall_permReindex {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ → α)} (hs_meas : MeasurableSet s) (hs_inv : ∀ (π : Equiv.Perm ℕ), (MulAction.fixedBy ℕ π)ᶜ.Finite → permReindex π ⁻¹' s = s) :
    MeasurableSet s

    An ambient-measurable event fixed by every finitely supported time permutation is measurable for the exchangeable σ-algebra.

    source
    @[simp]
    theorem TauCeti.Probability.MeasurableSet.preimage_permReindex_eq_of_exchangeableSigma {α : Type u_1} [MeasurableSpace α] {s : Set (ℕ → α)} (hs : MeasurableSet s) {π : Equiv.Perm ℕ} (hπ : (MulAction.fixedBy ℕ π)ᶜ.Finite) :
    permReindex π ⁻¹' s = s

    An exchangeable event is fixed by any finitely supported time permutation.

    source
    theorem TauCeti.Probability.measurable_permReindex_exchangeableSigma {α : Type u_1} [MeasurableSpace α] (π : Equiv.Perm ℕ) :
    Measurable (permReindex π)

    Reindexing by any permutation is measurable as an endomap of the exchangeable σ-algebra.

    source
    theorem TauCeti.Probability.measurable_exchangeableSigma_of_comp_permReindex_eq {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {g : (ℕ → α) → β} (hg : Measurable g) (hg_perm : ∀ (π : Equiv.Perm ℕ), (MulAction.fixedBy ℕ π)ᶜ.Finite → g ∘ permReindex π = g) :
    Measurable g

    An ambient-measurable observable fixed by every finitely supported reindexing is measurable with respect to the exchangeable σ-algebra.

    source
    theorem TauCeti.Probability.comp_permReindex_eq_of_measurable_exchangeableSigma {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] {g : (ℕ → α) → β} (hg : Measurable g) {π : Equiv.Perm ℕ} (hπ : (MulAction.fixedBy ℕ π)ᶜ.Finite) :
    g ∘ permReindex π = g

    For a target with measurable singletons, a function measurable with respect to the exchangeable σ-algebra is fixed by every finitely supported reindexing.

    source
    theorem TauCeti.Probability.pathTail_le_exchangeableSigma {α : Type u_1} [MeasurableSpace α] :
    pathTail α ≤ exchangeableSigma α

    The path-space tail σ-algebra is contained in the exchangeable σ-algebra: tail events are fixed by every finitely supported permutation of the time coordinate.