Existence of stationary weights by Cesàro averages and compactness

noncomputable def Dynamics.Kernel.advance {α : Type u_1} [Fintype α] (K : Kernel α) (p : Distribution α) : Distribution α

Evolve a distribution by one transition.

Equations

• K.advance p = { weight := fun (b : α) => ∑ a : α, p.weight a * (K a).weight b, nonneg := ⋯, sum_one := ⋯ }

noncomputable def Dynamics.Kernel.law {α : Type u_1} [Fintype α] (K : Kernel α) (p : Distribution α) : ℕ → Distribution α

Distribution of the state at time n.

Equations

• K.law p 0 = p
• K.law p n.succ = K.advance (K.law p n)

noncomputable def Dynamics.Kernel.cesaro {α : Type u_1} [Fintype α] (K : Kernel α) (p : Distribution α) (n : ℕ) : Distribution α

Cesàro averages over the first n + 1 distributions.

Equations

• K.cesaro p n = { weight := fun (a : α) => (∑ t ∈ Finset.range (n + 1), (K.law p t).weight a) / (↑n + 1), nonneg := ⋯, sum_one := ⋯ }

theorem Dynamics.Kernel.weight_le_one {α : Type u_1} [Fintype α] (p : Distribution α) (a : α) : p.weight a ≤ 1

theorem Dynamics.Kernel.cesaro_defect {α : Type u_1} [Fintype α] (K : Kernel α) (p : Distribution α) (n : ℕ) (b : α) : (K.advance (K.cesaro p n)).weight b - (K.cesaro p n).weight b = ((K.law p (n + 1)).weight b - p.weight b) / (↑n + 1)

The defect of stationarity telescopes to two endpoint distributions.

theorem Dynamics.Kernel.exists_stationary {α : Type u_1} [Fintype α] [Nonempty α] (K : Kernel α) : ∃ (p : Distribution α), K.Stationary p

Every stochastic matrix on a finite nonempty type has a stationary distribution.