Stationary processes

A process X : ℕ → Ω → α is stationary when the law of a block of consecutive values does not depend on where the block starts. A process that advances by a measure-preserving map of the sample space is stationary.

Main definitions

• ProbabilityTheory.block X a n: the n consecutive values of X from time a.
• ProbabilityTheory.IsStationary X μ: every block has the law of the block of the same length at time 0.

Main statements

• MeasureTheory.MeasurePreserving.identDistrib_comp: a measurable function has the same law after a measure-preserving map.
• ProbabilityTheory.IsStationary.of_measurePreserving: if X (t + 1) = X t ∘ T for a measure-preserving T, then X is stationary.

References

• [CT06]

def ProbabilityTheory.block {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (a n : ℕ) (ω : Ω) : Fin n → α

block X a n is the block of n consecutive values of X starting at time a.

Equations

• ProbabilityTheory.block X a n ω i = X (↑i + a) ω

theorem ProbabilityTheory.block_zero_succ {Ω : Type u_1} {α : Type u_2} {X : ℕ → Ω → α} (t : ℕ) : block X 0 (t + 1) = ⇑(Fin.snocEquiv fun (x : Fin (t + 1)) => α) ∘ fun (ω : Ω) => (X t ω, block X 0 t ω)

A block from time 0 grows by the next value appended at its end.

theorem ProbabilityTheory.measurable_block {Ω : Type u_1} {α : Type u_2} {X : ℕ → Ω → α} [MeasurableSpace Ω] [MeasurableSpace α] (hX : ∀ (t : ℕ), Measurable (X t)) (a n : ℕ) : Measurable (block X a n)

def ProbabilityTheory.IsStationary {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (μ : MeasureTheory.Measure Ω) : Prop

A process is stationary when the law of a block does not depend on where it starts.

Equations

• ProbabilityTheory.IsStationary X μ = ∀ (a n : ℕ), ProbabilityTheory.IdentDistrib (ProbabilityTheory.block X a n) (ProbabilityTheory.block X 0 n) μ μ

theorem ProbabilityTheory.IsStationary.comp {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {X : ℕ → Ω → α} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} (hs : IsStationary X μ) {f : α → β} (hf : Measurable f) : IsStationary (fun (t : ℕ) (ω : Ω) => f (X t ω)) μ

A measurable function of a stationary process is stationary.

theorem MeasureTheory.MeasurePreserving.identDistrib_comp {Ω : Type u_1} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace β] {μ : Measure Ω} {T : Ω → Ω} (hT : MeasurePreserving T μ μ) {f : Ω → β} (hf : Measurable f) : ProbabilityTheory.IdentDistrib (f ∘ T) f μ μ

A measurable function has the same law after a measure-preserving map.

theorem ProbabilityTheory.IsStationary.of_measurePreserving {Ω : Type u_1} {α : Type u_2} {X : ℕ → Ω → α} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (hX : ∀ (t : ℕ), Measurable (X t)) (h : ∀ (t : ℕ), X (t + 1) = X t ∘ T) : IsStationary X μ

A process that advances by a measure-preserving map of the sample space is stationary.