Tail σ-algebras of a process, and cons/tail of sequence-valued random variables

This file provides the process-relative tail σ-algebra API requested in the Exchangeability roadmap, Layer 2. For a process X : (k : ℕ) → Ω → β k, tailFamily X n is the σ-algebra generated by the coordinates X k with n ≤ k, and tailProcess X is the Mathlib tail σ-algebra limsup ... atTop of the coordinate σ-algebras. The future σ-algebras form an antitone family, the interface that later reverse-martingale statements consume via tailFamily_antitone and tailProcess_eq_iInf_tailFamily.

It also provides the pointwise Stream'.cons/Stream'.tail operations processCons/processTail on sequence-valued random variables t : Ω → ℕ → α, with their measurability and comap σ-algebra-contraction lemmas — kept here because their contraction lemmas are exactly the tail σ-algebra facts the Kallenberg conditional-independence step of the de Finetti factorisation needs.

@[implicit_reducible]

def TauCeti.Probability.tailFamily {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) (n : ℕ) : MeasurableSpace Ω

The σ-algebra generated by the future coordinates X k with n ≤ k.

Equations

• TauCeti.Probability.tailFamily X n = ⨆ (k : { k : ℕ // n ≤ k }), MeasurableSpace.comap (X ↑k) inferInstance

@[implicit_reducible]

def TauCeti.Probability.tailProcess {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) : MeasurableSpace Ω

The tail σ-algebra of a process, expressed as Mathlib's limsup tail σ-algebra.

Equations

• TauCeti.Probability.tailProcess X = Filter.limsup (fun (k : ℕ) => MeasurableSpace.comap (X k) inferInstance) Filter.atTop

@[simp]

theorem TauCeti.Probability.tailFamily_eq_iSup_comap {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) (n : ℕ) : tailFamily X n = ⨆ (k : { k : ℕ // n ≤ k }), MeasurableSpace.comap (X ↑k) inferInstance

Normal form for the future σ-algebra generated by coordinates from n onward.

theorem TauCeti.Probability.tailProcess_eq_limsup {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) : tailProcess X = Filter.limsup (fun (k : ℕ) => MeasurableSpace.comap (X k) inferInstance) Filter.atTop

The process-relative tail σ-algebra is Mathlib's limsup tail σ-algebra.

@[simp]

theorem TauCeti.Probability.tailProcess_eq_iInf_tailFamily {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) : tailProcess X = ⨅ (n : ℕ), tailFamily X n

Normal form for the process-relative tail σ-algebra.

theorem TauCeti.Probability.measurable_tailFamily_of_le {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] {X : (k : ℕ) → Ω → β k} {n k : ℕ} (hnk : n ≤ k) : Measurable (X k)

A future coordinate is measurable with respect to the corresponding future σ-algebra.

theorem TauCeti.Probability.tailFamily_le_iff {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] {X : (k : ℕ) → Ω → β k} {n : ℕ} {m : MeasurableSpace Ω} : tailFamily X n ≤ m ↔ ∀ (k : ℕ), n ≤ k → Measurable (X k)

Universal property of the future σ-algebra generated by coordinates from n onward.

theorem TauCeti.Probability.tailFamily_antitone {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) : Antitone (tailFamily X)

The future σ-algebras of a process form a decreasing family.

theorem TauCeti.Probability.tailProcess_le_tailFamily {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) (n : ℕ) : tailProcess X ≤ tailFamily X n

The tail σ-algebra is contained in every future σ-algebra.

theorem TauCeti.Probability.tailFamily_eq_comap_shift {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] (X : (k : ℕ) → Ω → β k) (r : ℕ) : tailFamily X r = MeasurableSpace.comap (fun (ω : Ω) (n : ℕ) => X (r + n) ω) inferInstance

The future σ-algebra tailFamily X r is the σ-algebra generated by the r-shifted tail ω ↦ (X (r + ·) ω), viewed as a single (product-valued) random variable.

theorem TauCeti.Probability.tailFamily_le_ambient {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] [MeasurableSpace Ω] {X : (k : ℕ) → Ω → β k} (n : ℕ) (hX : ∀ (k : ℕ), n ≤ k → Measurable (X k)) : tailFamily X n ≤ inferInstance

If all coordinates are ambient-measurable, then each future σ-algebra is a sub-σ-algebra of the ambient one.

theorem TauCeti.Probability.tailProcess_le_ambient {Ω : Type u_1} {β : ℕ → Type u_2} [(k : ℕ) → MeasurableSpace (β k)] [MeasurableSpace Ω] {X : (k : ℕ) → Ω → β k} (n : ℕ) (hX : ∀ (k : ℕ), n ≤ k → Measurable (X k)) : tailProcess X ≤ inferInstance

If the coordinates from some cutoff n onward are ambient-measurable, then the tail σ-algebra is a sub-σ-algebra of the ambient one. The tail does not see the finitely many initial coordinates, so only eventual measurability is required.

@[reducible, inline]

abbrev TauCeti.Probability.pathTail (α : Type u_4) [MeasurableSpace α] : MeasurableSpace (ℕ → α)

The path-space tail σ-algebra, i.e. the tail of the coordinate process on ℕ → α.

Equations

• TauCeti.Probability.pathTail α = TauCeti.Probability.tailProcess fun (k : ℕ) (x : ℕ → α) => x k

@[simp]

theorem TauCeti.Probability.pathTail_eq_tailProcess {α : Type u_3} [MeasurableSpace α] : pathTail α = tailProcess fun (k : ℕ) (x : ℕ → α) => x k

Normal form for the path-space tail σ-algebra.

theorem TauCeti.Probability.pathTail_le_tailFamily {α : Type u_3} [MeasurableSpace α] (n : ℕ) : pathTail α ≤ tailFamily (fun (k : ℕ) (x : ℕ → α) => x k) n

The path-space tail σ-algebra is contained in every future path σ-algebra from time n onward.

Cons and tail of sequence-valued random variables

processCons / processTail prepend / drop the leading coordinate of a sequence-valued random variable t : Ω → ℕ → α. The comap contraction lemmas (comap_processTail_le, comap_le_comap_processCons) record that the tail generates a coarser σ-algebra and that consing refines it; these feed the Kallenberg conditional-independence step of the de Finetti block-product factorisation. The definitions are not @[expose]; their characteristic API is the @[simp] _apply / interaction lemmas below.

Adapted from cameronfreer/exchangeability (DeFinetti/ViaMartingale/ShiftOperations.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22).

def TauCeti.Probability.processCons {Ω : Type u_1} {α : Type u_3} (x : Ω → α) (t : Ω → ℕ → α) : Ω → ℕ → α

Cons a head random variable onto a sequence-valued one (a pointwise Stream'.cons): processCons x t = [x, t 0, t 1, …].

Equations

• TauCeti.Probability.processCons x t ω = Stream'.cons (x ω) (t ω)

@[simp]

theorem TauCeti.Probability.processCons_zero {Ω : Type u_1} {α : Type u_3} (x : Ω → α) (t : Ω → ℕ → α) (ω : Ω) : processCons x t ω 0 = x ω

Leading coordinate of a cons: processCons x t ω 0 = x ω.

@[simp]

theorem TauCeti.Probability.processCons_succ {Ω : Type u_1} {α : Type u_3} (x : Ω → α) (t : Ω → ℕ → α) (ω : Ω) (n : ℕ) : processCons x t ω (n + 1) = t ω n

Later coordinates of a cons: processCons x t ω (n + 1) = t ω n.

def TauCeti.Probability.processTail {Ω : Type u_1} {α : Type u_3} (t : Ω → ℕ → α) : Ω → ℕ → α

Drop the leading coordinate of a sequence-valued random variable (a pointwise Stream'.tail): processTail t ω n = t ω (n+1).

Equations

• TauCeti.Probability.processTail t ω = Stream'.tail (t ω)

@[simp]

theorem TauCeti.Probability.processTail_apply {Ω : Type u_1} {α : Type u_3} (t : Ω → ℕ → α) (ω : Ω) (n : ℕ) : processTail t ω n = t ω (n + 1)

Coordinate equation for processTail: its nth coordinate is t (n + 1).

@[simp]

theorem TauCeti.Probability.processTail_processCons {Ω : Type u_1} {α : Type u_3} (x : Ω → α) (t : Ω → ℕ → α) : processTail (processCons x t) = t

The tail of a cons recovers the original sequence.

@[simp]

theorem TauCeti.Probability.processCons_processTail {Ω : Type u_1} {α : Type u_3} (t : Ω → ℕ → α) : processCons (fun (ω : Ω) => t ω 0) (processTail t) = t

Reconstruct a sequence from its head and tail (the reverse of processTail_processCons).

theorem TauCeti.Probability.measurable_processCons {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_3} [MeasurableSpace α] {x : Ω → α} {t : Ω → ℕ → α} (hx : Measurable x) (ht : ∀ (n : ℕ), Measurable fun (ω : Ω) => t ω n) : Measurable (processCons x t)

Consing a measurable head onto a process is measurable when its coordinates t (· ·) are.

theorem TauCeti.Probability.measurable_processTail {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_3} [MeasurableSpace α] {t : Ω → ℕ → α} (ht : ∀ (n : ℕ), Measurable fun (ω : Ω) => t ω (n + 1)) : Measurable (processTail t)

The tail of a process is measurable when its tail coordinates t (· + 1) are.

theorem TauCeti.Probability.comap_processTail_le {Ω : Type u_1} {α : Type u_3} [MeasurableSpace α] {t : Ω → ℕ → α} : MeasurableSpace.comap (processTail t) inferInstance ≤ MeasurableSpace.comap t inferInstance

The tail of a sequence-valued random variable generates a coarser σ-algebra than the variable itself.

theorem TauCeti.Probability.comap_le_comap_processCons {Ω : Type u_1} {α : Type u_3} [MeasurableSpace α] (x : Ω → α) (t : Ω → ℕ → α) : MeasurableSpace.comap t inferInstance ≤ MeasurableSpace.comap (processCons x t) inferInstance

Consing a head onto a sequence-valued random variable refines its σ-algebra: σ(t) ≤ σ(processCons x t).

@[simp]

theorem TauCeti.Probability.comap_processCons_eq_sup {Ω : Type u_1} {α : Type u_3} [MeasurableSpace α] (x : Ω → α) (t : Ω → ℕ → α) : MeasurableSpace.comap (processCons x t) inferInstance = MeasurableSpace.comap x inferInstance ⊔ MeasurableSpace.comap t inferInstance

Consing a head onto a sequence-valued random variable joins their σ-algebras: σ(processCons x t) = σ(x) ⊔ σ(t).