InformationTheory.Shannon.BackwardFiltration

Imports 5

Backward filtration and tail σ-algebra #

Given a measurable transformation T : Ω → Ω on a measurable space (Ω, m₀), the backward filtration is the antitone sequence

ℋ_n := T⁻ⁿ(m₀) = MeasurableSpace.comap (T^[n]) m₀

Indexed over ℕᵒᵈ, this becomes a MeasureTheory.Filtration ℕᵒᵈ m₀. The tail σ-algebra is ℋ_∞ := ⋂_n ℋ_n.

These objects underpin the backward martingale approach to Birkhoff's ergodic theorem.

Main definitions #

backwardFiltration — the antitone sequence n ↦ comap (T^[n]) m₀ packaged as a Filtration ℕᵒᵈ m₀.
tailSigma — the tail σ-algebra ⨅ n, comap (T^[n]) m₀.

Main statements #

backwardFiltration_apply — applied form (definitional).
tailSigma_le_comap_iterate — tailSigma ≤ comap (T^[n]) m₀ for every n.
comap_T_tailSigma_le — comap T (tailSigma) ≤ tailSigma (one half of T-invariance; the equality direction requires extra structure such as measure preservation).

def

InformationTheory.Shannon.backwardFiltration

source

{Ω : Type u_1} [m₀ : MeasurableSpace Ω] (T : Ω → Ω) (hT : Measurable T) :

MeasureTheory.Filtration ℕ ᵒᵈ m₀

Backward filtration ℋ_n := σ(T^[n]) = T⁻ⁿ(m₀), indexed by ℕᵒᵈ.

In ℕᵒᵈ, n ≤ m corresponds to m ≤ n in ℕ, so the underlying ℕ-indexed family n ↦ comap (T^[n]) m₀ is antitone — exactly the backward-filtration shape needed for reverse-time martingale arguments.

Equations

InformationTheory.Shannon.backwardFiltration T hT = { seq := fun (n : ℕ ᵒᵈ) => MeasurableSpace.comap T^[OrderDual.ofDual n] m₀, mono' := ⋯, le' := ⋯ }

Instances For

Used by

theorem

InformationTheory.Shannon.backwardFiltration_apply

source

@[simp]

{Ω : Type u_1} [m₀ : MeasurableSpace Ω] (T : Ω → Ω) (hT : Measurable T) (n : ℕ ᵒᵈ) :

↑(backwardFiltration T hT) n = MeasurableSpace.comap T^[OrderDual.ofDual n] m₀

Applied form of backwardFiltration.

Used by

def

InformationTheory.Shannon.tailSigma

source

@[reducible]

{Ω : Type u_1} [m₀ : MeasurableSpace Ω] (T : Ω → Ω) (hT : Measurable T) :

MeasurableSpace Ω

Tail σ-algebra ℋ_∞ := ⋂_n ℋ_n = ⨅_n comap (T^[n]) m₀.

Equations

InformationTheory.Shannon.tailSigma T hT = ⨅ (n : ℕ), ↑(InformationTheory.Shannon.backwardFiltration T hT) (OrderDual.toDual n)

Instances For

Used by

theorem

InformationTheory.Shannon.tailSigma_le_comap_iterate

source

{Ω : Type u_1} [m₀ : MeasurableSpace Ω] (T : Ω → Ω) (hT : Measurable T) (n : ℕ) :

tailSigma T hT ≤ MeasurableSpace.comap T^[n] m₀

tailSigma is bounded above by every level of the backward filtration.

Used by

theorem

InformationTheory.Shannon.tailSigma_le

source

{Ω : Type u_1} [m₀ : MeasurableSpace Ω] (T : Ω → Ω) (hT : Measurable T) :

tailSigma T hT ≤ m₀

tailSigma is contained in m₀: it is a sub-σ-algebra of the ambient space.

Used by

theorem

InformationTheory.Shannon.comap_T_tailSigma_le

source

{Ω : Type u_1} [m₀ : MeasurableSpace Ω] (T : Ω → Ω) (hT : Measurable T) :

MeasurableSpace.comap T (tailSigma T hT) ≤ tailSigma T hT

One half of T-invariance: pulling the tail σ-algebra back through T lands again inside the tail. The reverse inclusion requires additional structure (e.g. measure preservation).

Used by