Shift Operations for Martingale Proof

Core definitions for sequence shifting and tail operations used throughout the ViaMartingale proof:

• path X - The random path ω ↦ (n ↦ X n ω)
• shiftRV X m - Shifted path ω ↦ (n ↦ X (m + n) ω)
• shiftProcess X m - Shifted process (θₘX)ₙ = X_{m+n}
• consRV, tailRV - Cons and tail for sequences

These are extracted from ViaMartingale.lean to enable modular imports.

Path and Shift Definitions

def Exchangeability.DeFinetti.ViaMartingale.path {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) : Ω → ℕ → α

The random path of a process: ω ↦ (n ↦ X n ω).

Equations

• Exchangeability.DeFinetti.ViaMartingale.path X ω n = X n ω

def Exchangeability.DeFinetti.ViaMartingale.shiftRV {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m : ℕ) : Ω → ℕ → α

Shifted random path: ω ↦ (n ↦ X (m + n) ω).

Equations

• Exchangeability.DeFinetti.ViaMartingale.shiftRV X m ω n = X (m + n) ω

def Exchangeability.DeFinetti.ViaMartingale.shiftProcess {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m : ℕ) : ℕ → Ω → α

Shifted process: (θₘX)ₙ = X_{m+n}.

Equations

• Exchangeability.DeFinetti.ViaMartingale.shiftProcess X m n ω = X (m + n) ω

Cons and Tail Operations

def Exchangeability.DeFinetti.ViaMartingale.consRV {Ω : Type u_1} {α : Type u_2} (x : Ω → α) (t : Ω → ℕ → α) : Ω → ℕ → α

Cons a value onto a sequence: consRV x t produces [x, t(0), t(1), ...].

Equations

• Exchangeability.DeFinetti.ViaMartingale.consRV x t x✝ 0 = x x✝
• Exchangeability.DeFinetti.ViaMartingale.consRV x t x✝ n.succ = t x✝ n

def Exchangeability.DeFinetti.ViaMartingale.tailRV {Ω : Type u_1} {α : Type u_2} (t : Ω → ℕ → α) : Ω → ℕ → α

Tail of a sequence: drops index 0, so tailRV t n = t (n+1).

Equations

• Exchangeability.DeFinetti.ViaMartingale.tailRV t ω n = t ω (n + 1)

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.consRV_zero {Ω : Type u_1} {α : Type u_2} (x : Ω → α) (t : Ω → ℕ → α) (ω : Ω) : consRV x t ω 0 = x ω

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.consRV_succ {Ω : Type u_1} {α : Type u_2} (x : Ω → α) (t : Ω → ℕ → α) (ω : Ω) (n : ℕ) : consRV x t ω (n + 1) = t ω n

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.tailRV_apply {Ω : Type u_1} {α : Type u_2} (t : Ω → ℕ → α) (ω : Ω) (n : ℕ) : tailRV t ω n = t ω (n + 1)

@[simp]

theorem Exchangeability.DeFinetti.ViaMartingale.tailRV_consRV {Ω : Type u_1} {α : Type u_2} (x : Ω → α) (t : Ω → ℕ → α) : tailRV (consRV x t) = t

theorem Exchangeability.DeFinetti.ViaMartingale.shiftRV_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m : ℕ) (ω : Ω) (n : ℕ) : shiftRV X m ω n = X (m + n) ω

theorem Exchangeability.DeFinetti.ViaMartingale.shiftRV_zero {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) : shiftRV X 0 = path X

theorem Exchangeability.DeFinetti.ViaMartingale.shiftProcess_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m n : ℕ) (ω : Ω) : shiftProcess X m n ω = X (m + n) ω

Measurability

Measurable combinators

theorem Exchangeability.DeFinetti.ViaMartingale.measurable_path {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {X : ℕ → Ω → α} (hX : ∀ (n : ℕ), Measurable (X n)) : Measurable (path X)

A process viewed as a full path is measurable.

theorem Exchangeability.DeFinetti.ViaMartingale.measurable_consRV {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (x : Ω → α) (t : Ω → ℕ → α) : Measurable x → Measurable t → Measurable (consRV x t)

Consing a head to a sequence is measurable if both pieces are measurable.

theorem Exchangeability.DeFinetti.ViaMartingale.measurable_tailRV {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {t : Ω → ℕ → α} (ht : Measurable t) : Measurable (tailRV t)

Tail is measurable when the original sequence is measurable.

theorem Exchangeability.DeFinetti.ViaMartingale.comap_tailRV_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {t : Ω → ℕ → α} : MeasurableSpace.comap (tailRV t) inferInstance ≤ MeasurableSpace.comap t inferInstance

The contraction property: σ(tailRV t) ≤ σ(t).

This is the key property for Kallenberg 1.3: tail gives a coarser σ-algebra.

theorem Exchangeability.DeFinetti.ViaMartingale.comap_le_comap_consRV {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (x : Ω → α) (t : Ω → ℕ → α) : MeasurableSpace.comap t inferInstance ≤ MeasurableSpace.comap (consRV x t) inferInstance

For W' = consRV x W, we have σ(W) ≤ σ(W').

This is the contraction for Kallenberg 1.3 when W' = cons(X_r, W).

theorem Exchangeability.DeFinetti.ViaMartingale.measurable_shiftRV {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {X : ℕ → Ω → α} (hX : ∀ (n : ℕ), Measurable (X n)) {m : ℕ} : Measurable (shiftRV X m)

Shift Contractability

theorem Exchangeability.DeFinetti.ViaMartingale.shift_contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (m : ℕ) : Contractable μ (shiftProcess X m)

If X is contractable, then so is each of its shifts θₘ X.