Finite Convergence

theorem FD1D.FiniteKernel.exists_pow_pos {α : Type u_1} [Fintype α] [DecidableEq α] (K : FiniteKernel α) (hirr : K.Irreducible) (hloop : K.HasPositiveLoops) : ∃ (N : ℕ), 0 < N ∧ ∀ (x y : α), 0 < K.pow N x y

Irreducibility and positive one-step loops make one common kernel power strictly positive in every entry.

def FD1D.FiniteKernel.lawL1 {α : Type u_1} [Fintype α] (μ ν : FiniteLaw α) : ℝ

The ℓ¹ distance between two finite probability laws.

Equations

• FD1D.FiniteKernel.lawL1 μ ν = ∑ x : α, |μ.mass x - ν.mass x|

theorem FD1D.FiniteKernel.tendsto_iterate_mass {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (K : FiniteKernel α) (hirr : K.Irreducible) (hloop : K.HasPositiveLoops) (π : FiniteLaw α) (hπ : K.IsStationary π) (μ : FiniteLaw α) : Filter.Tendsto (fun (n : ℕ) => (K.iterate n μ).mass) Filter.atTop (nhds π.mass)

Ordinary iterates of a finite irreducible kernel with positive loops converge, pointwise in mass, to any stationary law.

theorem FD1D.FiniteKernel.existsUnique_stationary_and_tendsto {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (K : FiniteKernel α) (hirr : K.Irreducible) (hloop : K.HasPositiveLoops) : ∃! π : FiniteLaw α, K.IsStationary π ∧ ∀ (μ : FiniteLaw α), Filter.Tendsto (fun (n : ℕ) => (K.iterate n μ).mass) Filter.atTop (nhds π.mass)

A finite irreducible kernel with positive loops has one stationary law, and every initial law converges ordinarily to it.

theorem FD1D.FiniteKernel.tendsto_expect_iterate {α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] (K : FiniteKernel α) (hirr : K.Irreducible) (hloop : K.HasPositiveLoops) (π : FiniteLaw α) (hπ : K.IsStationary π) (μ : FiniteLaw α) (f : α → ℝ) : Filter.Tendsto (fun (n : ℕ) => (K.iterate n μ).expect f) Filter.atTop (nhds (π.expect f))

Expectations of every real observable converge along the ordinary iterates to their value under the unique stationary law.