Process shift operation

The process-level path shift for a process X : ℕ → Ω → α, the random path seen from time m onward:

• processShift X m — the shifted random path ω ↦ (n ↦ X (m + n) ω), defined as the m-fold path-space shift (shift α)^[m] of the process's path.

The processCons / processTail operations on sequence-valued random variables, together with their σ-algebra-contraction lemmas, live in TauCeti.Probability.Process.Tail.Basic.

Its exported API is the @[simp] coordinate equation processShift_apply and the bridges to the path shift: processShift_eq_shift_iterate (composition) and map_processShift (measure level).

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

def TauCeti.Probability.processShift {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m : ℕ) : Ω → ℕ → α

The shifted random path of a process, as the m-fold path-space shift (shift α)^[m] of the process's path (reusing the path shift): ω ↦ (n ↦ X (m + n) ω).

Equations

• TauCeti.Probability.processShift X m ω = (TauCeti.Probability.shift α)^[m] fun (n : ℕ) => X n ω

@[simp]

theorem TauCeti.Probability.processShift_apply {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m n : ℕ) (ω : Ω) : processShift X m ω n = X (m + n) ω

Coordinate equation for processShift: its nth coordinate is X (m + n).

theorem TauCeti.Probability.measurable_processShift {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {X : ℕ → Ω → α} {m : ℕ} (hX : ∀ (n : ℕ), Measurable (X (m + n))) : Measurable (processShift X m)

The shifted process is measurable when its tail coordinates X (m + ·) are.

theorem TauCeti.Probability.processShift_eq_shift_iterate {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (m : ℕ) : processShift X m = (shift α)^[m] ∘ fun (ω : Ω) (n : ℕ) => X n ω

processShift X m is the m-fold path shift (shift α)^[m] composed with the process path.

theorem TauCeti.Probability.map_processShift {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (m : ℕ) : MeasureTheory.Measure.map (processShift X m) μ = MeasureTheory.Measure.map (shift α)^[m] (pathLaw μ X)

Measure-level bridge: the law of the shifted process is the pushforward of the path law by the m-fold path shift (shift α)^[m].