Tail σ-algebras on path space and for general processes

This file provides two canonical viewpoints on tail σ-algebras with explicit bridge lemmas connecting them.

Main definitions

• tailFamily X n: The n-th reverse (future) σ-algebra generated by the tails of X
• tailProcess X: Tail σ-algebra of a process X : ℕ → Ω → α

Main results

• tailFamily_antitone, tailProcess_le_tailFamily: basic monotonicity
• tailProcess_eq_iInf_revFiltration: bridge to a reverse-filtration formulation (parameterised by an arbitrary revFiltration)
• tailProcess_le_ambient: the tail σ-algebra is a sub-σ-algebra of the ambient one

Implementation notes

This file is designed to be mathlib-ready:

• Only imports mathlib (no project dependencies)
• Comprehensive docstrings
• Conservative use of attributes (@[simp] only on definitional aliases)

Index Arithmetic (isolate Nat arithmetic once)

@[simp]

theorem Exchangeability.Tail.nat_add_assoc (n m k : ℕ) : n + (m + k) = n + m + k

Process-Relative Tail

@[reducible]

def Exchangeability.Tail.tailFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (n : ℕ) : MeasurableSpace Ω

The n-th reverse (future) σ-algebra generated by the tails of X.

Equations

• Exchangeability.Tail.tailFamily X n = ⨆ (k : ℕ), MeasurableSpace.comap (fun (ω : Ω) => X (n + k) ω) inferInstance

@[reducible]

def Exchangeability.Tail.tailProcess {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : MeasurableSpace Ω

Tail σ-algebra of a process X : ℕ → Ω → α.

Equations

• Exchangeability.Tail.tailProcess X = iInf (Exchangeability.Tail.tailFamily X)

theorem Exchangeability.Tail.tailFamily_antitone {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : Antitone (tailFamily X)

theorem Exchangeability.Tail.tailProcess_le_tailFamily {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (n : ℕ) : tailProcess X ≤ tailFamily X n

Helper Lemmas for comap and Infima

theorem Exchangeability.Tail.MeasurableSpace.preimage_injective_of_surjective {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Surjective f) : Function.Injective fun (s : Set β) => f ⁻¹' s

Preimage is injective on sets when f is surjective.

theorem Exchangeability.Tail.iInf_comap_eq_comap_iInf_of_surjective {ι : Type u_3} [Nonempty ι] {α : Type u_4} {β : Type u_5} {f : α → β} (hf : Function.Surjective f) (m : ι → MeasurableSpace β) : ⨅ (i : ι), MeasurableSpace.comap f (m i) = MeasurableSpace.comap f (iInf m)

With f surjective and a nonempty index type, comap commutes with ⨅.

theorem Exchangeability.Tail.tailProcess_eq_iInf_revFiltration {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (revFiltration : (ℕ → Ω → α) → ℕ → MeasurableSpace Ω) (hrev : ∀ (m : ℕ), revFiltration X m = ⨆ (k : ℕ), MeasurableSpace.comap (fun (ω : Ω) => X (m + k) ω) inferInstance) : tailProcess X = ⨅ (m : ℕ), revFiltration X m

Bridge 3 (to ViaMartingale's revFiltration). If revFiltration X m is defined as the σ-algebra generated by all X (m+k), then the tail equals ⨅ m, revFiltration X m.

Proof strategy: Rewrite each slice using hrev, then unfold tailProcess.

General Properties

theorem Exchangeability.Tail.tailProcess_le_ambient {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (hX : ∀ (k : ℕ), Measurable (X k)) : tailProcess X ≤ inferInstance

Tail σ-algebra is sub-σ-algebra of ambient space when all X_k are measurable.

NOTE: For probability/finite measures, trimming to the tail σ-algebra preserves sigma-finiteness. This is automatic via type class inference in mathlib.