Recurrent processes

A process X : ℕ → Ω → α is recurrent when, almost surely, every state it ever visits it visits infinitely often:

∀ᵐ ω ∂μ, ∀ k, ∃ᶠ n in atTop, X n ω = X k ω

The main theorem is that recurrence is automatic for a stationary process on a countable state space (recurrent_of_measurePreserving_shift): it is Poincaré recurrence for the one-sided shift, applied to the countably many coordinate events {x | x 0 = a} at once. The exchangeability-specific corollaries of that theorem live in TauCeti.Probability.Exchangeability.Recurrence.Basic.

Main results

• TauCeti.Probability.recurrent_def — the defining equation of Recurrent, which is not @[expose], so this is the unfolding interface downstream.
• TauCeti.Probability.recurrent_iff_ae_forall_state — the state-indexed reading of recurrence.
• TauCeti.Probability.recurrent_of_measurePreserving_shift — a process with a shift-invariant path law on a countable state space is recurrent.
• TauCeti.Probability.recurrent_pathLaw_iff — the process-level and path-law readings agree.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.

Mathlib's MeasureTheory.Conservative is recurrence of a map — the Poincaré recurrence theorem — and is consumed here rather than reproved; recurrence of a process in the above sense is not in Mathlib. No material is adapted from cameronfreer/exchangeability, which treats exchangeable rather than Markov exchangeable sequences.

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

A process is recurrent when, almost surely, every state it visits it visits infinitely often. This is Diaconis and Freedman's standing hypothesis on a Markov exchangeable process.

The body is not exposed; recurrent_def is the unfolding interface.

Equations

• TauCeti.Probability.Recurrent μ X = ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, X n ω = X k ω

theorem TauCeti.Probability.recurrent_def {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} : Recurrent μ X ↔ ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, X n ω = X k ω

The defining equation of recurrence. Recurrent is not @[expose], so this is how downstream modules unfold it.

theorem TauCeti.Probability.recurrent_iff_ae_forall_state {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} : Recurrent μ X ↔ ∀ᵐ (ω : Ω) ∂μ, ∀ (a : α), (∃ (k : ℕ), X k ω = a) → ∃ᶠ (n : ℕ) in Filter.atTop, X n ω = a

The state-indexed reading of recurrence. Almost surely, every state the process attains it attains infinitely often.

theorem TauCeti.Probability.Recurrent.ae_infinite_setOf_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), {n : ℕ | X n ω = X k ω}.Infinite

The set of times at which a recurrent process revisits any given one of its states is infinite.

theorem TauCeti.Probability.Recurrent.ae_exists_ge {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Recurrent μ X) : ∀ᵐ (ω : Ω) ∂μ, ∀ (k N : ℕ), ∃ (n : ℕ), N ≤ n ∧ X n ω = X k ω

Every state of a recurrent process recurs after every time.

theorem TauCeti.Probability.Recurrent.congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} (h : Recurrent μ X) (hXY : ∀ (n : ℕ), X n =ᵐ[μ] Y n) : Recurrent μ Y

Recurrence only depends on the process up to almost-everywhere equality of its coordinates.

theorem TauCeti.Probability.Recurrent.map_values {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {β : Type u_3} (h : Recurrent μ X) (f : α → β) : Recurrent μ fun (n : ℕ) (ω : Ω) => f (X n ω)

Recurrence is inherited by every coordinatewise pushforward: a repeated state stays repeated.

theorem TauCeti.Probability.ae_forall_frequently_apply_eq_of_measurePreserving_shift {α : Type u_2} [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (h : MeasureTheory.MeasurePreserving (shift α) ρ ρ) : ∀ᵐ (x : ℕ → α) ∂ρ, ∀ (k : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, x n = x k

Poincaré recurrence on path space. A shift-invariant law on the paths of a countable state space gives full mass to the paths that revisit each of their states infinitely often.

The one-sided shift is measure preserving, hence conservative, so almost every path whose orbit meets the coordinate event {x | x 0 = a} meets it infinitely often; countability of the state space lets a single null set serve all a at once.

theorem TauCeti.Probability.recurrent_of_measurePreserving_shift {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (h : MeasureTheory.MeasurePreserving (shift α) (pathLaw μ X) (pathLaw μ X)) : Recurrent μ X

A stationary process on a countable state space is recurrent.

theorem TauCeti.Probability.measurableSet_setOf_forall_frequently_apply_eq {α : Type u_2} [MeasurableSpace α] [MeasurableEq α] : MeasurableSet {x : ℕ → α | ∀ (k : ℕ), ∃ᶠ (n : ℕ) in Filter.atTop, x n = x k}

The recurrent paths form a measurable set: they are cut out by countably many coordinate coincidences, each measurable by Mathlib's measurableSet_eq_fun.

theorem TauCeti.Probability.recurrent_pathLaw_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableEq α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : (Recurrent (pathLaw μ X) fun (n : ℕ) (x : ℕ → α) => x n) ↔ Recurrent μ X

The process-level and path-law formulations of recurrence agree.