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 : ℕ → Ω → α
• tailShift α: Tail σ-algebra on path space (ℕ → α) defined via one-sided shifts

Main results

• tailProcess_coords_eq_tailShift: The critical bridge between path-space and process formulations
• tailProcess_eq_comap_path: Pullback formulation (most convenient in practice)
• tailProcess_eq_iInf_revFiltration: Connection to reverse filtration formulation

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

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

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)

@[simp]

theorem Exchangeability.Tail.tailProcess_def {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : tailProcess X = iInf (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

Path-Space Tail

def Exchangeability.Tail.tailShift (α : Type u_3) [MeasurableSpace α] : MeasurableSpace (ℕ → α)

Tail σ-algebra on path space (ℕ → α) defined via one-sided shifts.

Equations

• Exchangeability.Tail.tailShift α = ⨅ (n : ℕ), MeasurableSpace.comap (fun (ω : ℕ → α) (k : ℕ) => ω (n + k)) inferInstance

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.MeasurableSpace.map_comap_eq_of_surjective {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Surjective f) (m : MeasurableSpace β) : MeasurableSpace.map f (MeasurableSpace.comap f m) = m

If f is surjective, then map f (comap f m) = m.

theorem Exchangeability.Tail.comap_iInf_le {α : Type u_2} {β : Type u_4} {ι : Sort u_3} (f : α → β) (m : ι → MeasurableSpace β) : MeasurableSpace.comap f (iInf m) ≤ ⨅ (i : ι), MeasurableSpace.comap f (m i)

comap distributes over iInf unconditionally (≤ direction only).

The inequality comap f (⨅ i, m i) ≤ ⨅ i, comap f (m i) holds by monotonicity. The reverse inequality (and hence equality) requires f to be surjective. See iInf_comap_eq_comap_iInf_of_surjective for the surjective case.

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 ⨅.

Bridge Lemmas (LOAD-BEARING - Phase 1a)

theorem Exchangeability.Tail.comap_shift_eq_iSup_comap_coords {α : Type u_2} [MeasurableSpace α] (n : ℕ) : MeasurableSpace.comap (fun (ω : ℕ → α) (k : ℕ) => ω (n + k)) inferInstance = ⨆ (k : ℕ), MeasurableSpace.comap (fun (ω : ℕ → α) => ω (n + k)) inferInstance

On path space: the pullback of the product σ-algebra by the n-fold shift equals the join of the coordinate pullbacks at indices n+k.

Proof strategy: Use that the product σ-algebra on (ℕ → α) is generated by coordinate maps ω ↦ ω k. Apply comap_comp with eval (n+k) = (eval k) ∘ (shift^[n]), then bundle via iSup_congr.

theorem Exchangeability.Tail.tailFamily_eq_comap_sample_path_shift {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (n : ℕ) : tailFamily X n = MeasurableSpace.comap (fun (ω : Ω) (k : ℕ) => X k ω) (MeasurableSpace.comap (fun (ω : ℕ → α) (k : ℕ) => ω (n + k)) inferInstance)

Helper: Each tailFamily X n equals the pullback along the sample-path map of the n-shifted path-space σ-algebra. This is the key to connecting the two formulations.

theorem Exchangeability.Tail.tailProcess_coords_eq_tailShift {α : Type u_2} [MeasurableSpace α] : (tailProcess fun (k : ℕ) (ω : ℕ → α) => ω k) = tailShift α

Bridge 1 (path ↔ process). For the coordinate process on path space, tailProcess equals tailShift.

Proof strategy: Apply iInf_congr using comap_shift_eq_iSup_comap_coords.

theorem Exchangeability.Tail.comap_path_tailShift_le_tailProcess {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : MeasurableSpace.comap (fun (ω : Ω) (k : ℕ) => X k ω) (tailShift α) ≤ tailProcess X

Bridge 2a (unconditional inequality). The process tail is always at least as coarse as the pullback of the path tail.

Note: Equality holds when the sample-path map is surjective. See tailProcess_eq_comap_path_of_surjective.

theorem Exchangeability.Tail.tailProcess_eq_comap_path_of_surjective {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (hΦ : Function.Surjective fun (ω : Ω) (k : ℕ) => X k ω) : tailProcess X = MeasurableSpace.comap (fun (ω : Ω) (k : ℕ) => X k ω) (tailShift α)

Bridge 2b (surjective equality). When the sample-path map Φ : Ω → (ℕ → α) given by Φ ω k := X k ω is surjective, the process tail equals the pullback of the path tail along Φ.

Proof strategy: Use iInf_comap_eq_comap_iInf_of_surjective with Nonempty ℕ.

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.