LeanPool.RlTheoryInLean.Data.Matrix.Stochastic

@[reducible, inline]

abbrev StochasticMatrix.l1Space (S : Type u) : Type u

The finite-dimensional L¹ space of real-valued functions on S.

Equations

• StochasticMatrix.l1Space S = WithLp 1 (S → ℝ)

class StochasticMatrix.StochasticVec {S : Type u} [Fintype S] (x : S → ℝ) : Prop

A nonnegative vector whose entries sum to one.

• nonneg (s : S) : 0 ≤ x s
• rowsum : ∑ s : S, x s = 1

theorem StochasticMatrix.StochasticVec.le_one {S : Type u} [Fintype S] (x : S → ℝ) [StochasticVec x] (s : S) : x s ≤ 1

@[reducible, inline]

abbrev StochasticMatrix.Simplex (S : Type u) [Fintype S] : Set (l1Space S)

The probability simplex, represented inside finite-dimensional L¹.

Equations

• StochasticMatrix.Simplex S = {x : StochasticMatrix.l1Space S | StochasticMatrix.StochasticVec x.ofLp}

instance StochasticMatrix.instStochasticVecOfLpForallRealValL1SpaceMemSetSimplex {S : Type u} [Fintype S] (x : ↑(Simplex S)) : StochasticVec (↑x).ofLp

instance StochasticMatrix.instIsClosedL1SpaceSimplex {S : Type u} [Fintype S] : IsClosed (Simplex S)

instance StochasticMatrix.instCompleteSpaceElemL1SpaceSimplex {S : Type u} [Fintype S] : CompleteSpace ↑(Simplex S)

theorem StochasticMatrix.l1_norm_eq_sum {S : Type u} [Fintype S] (f : l1Space S) : ‖f‖ = ∑ s : S, |f.ofLp s|

theorem StochasticMatrix.l1_norm_eq_one {S : Type u} [Fintype S] (x : l1Space S) [StochasticVec x.ofLp] : ‖x‖₊ = 1

theorem StochasticMatrix.simplex_subset_closedBall {S : Type u} [Fintype S] : Simplex S ⊆ Metric.closedBall 0 1

theorem StochasticMatrix.simples_is_compact {S : Type u} [Fintype S] : IsCompact (Simplex S)

class StochasticMatrix.RowStochastic {S : Type u} [Fintype S] (P : Matrix S S ℝ) : Prop

A matrix whose rows are stochastic vectors.

• stochastic (s : S) : StochasticVec (P s)

theorem StochasticMatrix.sum_svec_mul_smat_eq_one {S : Type u} [Fintype S] (μ : S → ℝ) [StochasticVec μ] (P : Matrix S S ℝ) [RowStochastic P] : ∑ i : S, ∑ j : S, μ i * P i j = 1

instance StochasticMatrix.svec_mul_smat_is_svec {S : Type u} [Fintype S] (μ : S → ℝ) [StochasticVec μ] (P : Matrix S S ℝ) [RowStochastic P] : StochasticVec (Matrix.vecMul μ P)

instance StochasticMatrix.smat_mul_smat_is_smat {S : Type u} [Fintype S] (P Q : Matrix S S ℝ) [RowStochastic P] [RowStochastic Q] : RowStochastic (P * Q)

instance StochasticMatrix.smat_pow_is_smat {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] (n : ℕ) : RowStochastic (P ^ n)

theorem StochasticMatrix.chapman_kolmogorov_eq_ge {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] (m n : ℕ) (i j k : S) : (P ^ (m + n)) i j ≥ (P ^ m) i k * (P ^ n) k j

class StochasticMatrix.Irreducible {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] : Prop

Irreducibility of a finite stochastic matrix.

• irreducible (i j : S) : ∃ (n : ℕ), 0 < (P ^ n) i j

noncomputable def StochasticMatrix.returnTimes {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) (i : S) : Set ℕ

The set of positive return times for state i

Equations

• StochasticMatrix.returnTimes P i = {n : ℕ | 1 ≤ n ∧ 0 < (P ^ n) i i}

theorem StochasticMatrix.return_times_add_mem {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] (i : S) {a b : ℕ} (ha : a ∈ returnTimes P i) (hb : b ∈ returnTimes P i) : a + b ∈ returnTimes P i

Return times are closed under addition (used via AddSubmonoid.closure)

class StochasticMatrix.Aperiodic {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] : Prop

A stochastic matrix is aperiodic if for each state, the GCD of return times is 1

• aperiodic (i : S) : Nat.setGcd (returnTimes P i) = 1

theorem StochasticMatrix.eventually_positive {S : Type u} [Fintype S] [DecidableEq S] [Nonempty S] (P : Matrix S S ℝ) [RowStochastic P] [Irreducible P] [Aperiodic P] : ∃ (N : ℕ), ∀ (n : ℕ) (i j : S), N ≤ n → 0 < (P ^ n) i j

class StochasticMatrix.DoeblinMinorization {S : Type u} [Fintype S] (P : Matrix S S ℝ) [RowStochastic P] : Prop

A Doeblin minorization for a finite stochastic matrix.

• minorize : ∃ (ε : ℝ) (ν : S → ℝ), 0 < ε ∧ ε < 1 ∧ StochasticVec ν ∧ ∀ (i j : S), P i j ≥ ε * ν j

theorem StochasticMatrix.smat_minorizable_with_large_pow {S : Type u} [Fintype S] [DecidableEq S] [Nonempty S] (P : Matrix S S ℝ) [RowStochastic P] [Irreducible P] [Aperiodic P] : ∃ (N : ℕ), 1 ≤ N ∧ DoeblinMinorization (P ^ N)

theorem StochasticMatrix.smat_nonexpansive_in_l1 {S : Type u} [Fintype S] (Q : Matrix S S ℝ) [RowStochastic Q] (x y : S → ℝ) : ‖WithLp.toLp 1 (Matrix.vecMul x Q - Matrix.vecMul y Q)‖₊ ≤ ‖WithLp.toLp 1 (x - y)‖₊

theorem StochasticMatrix.smat_pow_nonexpansive_in_l1 {S : Type u} [Fintype S] [DecidableEq S] (Q : Matrix S S ℝ) [RowStochastic Q] (n : ℕ) (x y : S → ℝ) : ‖WithLp.toLp 1 (Matrix.vecMul x (Q ^ n) - Matrix.vecMul y (Q ^ n))‖₊ ≤ ‖WithLp.toLp 1 (x - y)‖₊

def StochasticMatrix.smatAsOperator {S : Type u} [Fintype S] (P : Matrix S S ℝ) [RowStochastic P] : ↑(Simplex S) → ↑(Simplex S)

The affine action of a stochastic matrix on the probability simplex.

Equations

• StochasticMatrix.smatAsOperator P μ = ⟨WithLp.toLp 1 (Matrix.vecMul (↑μ).ofLp P), ⋯⟩

theorem StochasticMatrix.smat_as_operator_iter {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] (n : ℕ) : (smatAsOperator P)^[n] = fun (μ : ↑(Simplex S)) => ⟨WithLp.toLp 1 (Matrix.vecMul (↑μ).ofLp (P ^ n)), ⋯⟩

theorem StochasticMatrix.smat_contraction_in_simplex {S : Type u} [Fintype S] (P : Matrix S S ℝ) [RowStochastic P] [DoeblinMinorization P] : ∃ (K : NNReal), 0 < K ∧ ContractingWith K (smatAsOperator P)

class StochasticMatrix.Stationary {S : Type u} [Fintype S] (μ : S → ℝ) (P : Matrix S S ℝ) : Prop

A stationary distribution for a matrix.

• stationary : Matrix.vecMul μ P = μ

theorem StochasticMatrix.multi_step_stationary {S : Type u} [Fintype S] [DecidableEq S] (μ : S → ℝ) (P : Matrix S S ℝ) (n : ℕ) [Stationary μ P] : Stationary μ (P ^ n)

theorem StochasticMatrix.pos_of_stationary {S : Type u} [Fintype S] [DecidableEq S] (μ : S → ℝ) [StochasticVec μ] (P : Matrix S S ℝ) [RowStochastic P] [Irreducible P] [Stationary μ P] (s : S) : 0 < μ s

noncomputable def StochasticMatrix.cesaroAverage {S : Type u} [Fintype S] [DecidableEq S] (x₀ : S → ℝ) (P : Matrix S S ℝ) (n : ℕ) : S → ℝ

The Cesaro average of the first n + 1 iterates of a stochastic vector.

Equations

• StochasticMatrix.cesaroAverage x₀ P n = (↑n + 1)⁻¹ • ∑ k ∈ Finset.range (n + 1), Matrix.vecMul x₀ (P ^ k)

theorem StochasticMatrix.cesaro_average_is_svec {S : Type u} [Fintype S] [DecidableEq S] (x₀ : S → ℝ) [StochasticVec x₀] (P : Matrix S S ℝ) [RowStochastic P] (n : ℕ) : StochasticVec (cesaroAverage x₀ P n)

theorem StochasticMatrix.cesaro_average_almost_invariant {S : Type u} [Fintype S] [DecidableEq S] (x₀ : S → ℝ) [StochasticVec x₀] (P : Matrix S S ℝ) [RowStochastic P] (n : ℕ) : ‖WithLp.toLp 1 (Matrix.vecMul (cesaroAverage x₀ P n) P - cesaroAverage x₀ P n)‖ ≤ 2 / (↑n + 1)

@[reducible, inline]

noncomputable abbrev StochasticMatrix.uniformDistribution {S : Type u} [Fintype S] : S → ℝ

The uniform probability distribution on a nonempty finite type.

Equations

• StochasticMatrix.uniformDistribution = Function.const S (1 / ↑(Fintype.card S))

instance StochasticMatrix.instStochasticVecUniformDistribution {S : Type u} [Fintype S] [Nonempty S] : StochasticVec uniformDistribution

instance StochasticMatrix.instNonemptyElemL1SpaceSimplex {S : Type u} [Fintype S] [Nonempty S] : Nonempty ↑(Simplex S)

theorem StochasticMatrix.stationary_distribution_exists {S : Type u} [Fintype S] [Nonempty S] (P : Matrix S S ℝ) [RowStochastic P] : ∃ (μ : S → ℝ), StochasticVec μ ∧ Stationary μ P

theorem StochasticMatrix.stationary_distribution_uniquely_exists {S : Type u} [Fintype S] [DecidableEq S] [Nonempty S] (P : Matrix S S ℝ) [RowStochastic P] [Aperiodic P] [Irreducible P] : ∃! μ : S → ℝ, StochasticVec μ ∧ Stationary μ P

class StochasticMatrix.GeometricMixing {S : Type u} [Fintype S] [DecidableEq S] (P : Matrix S S ℝ) [RowStochastic P] : Prop

Geometric convergence to stationarity in total variation/L¹ distance.

• mixing : ∃ (C : ℝ) (ρ : ℝ) (μ : S → ℝ), 0 < C ∧ 0 < ρ ∧ ρ < 1 ∧ StochasticVec μ ∧ Stationary μ P ∧ ∀ (x : S → ℝ) [StochasticVec x] (n : ℕ), ↑‖WithLp.toLp 1 (Matrix.vecMul x (P ^ n) - μ)‖₊ ≤ C * ρ ^ n

instance StochasticMatrix.instGeometricMixingOfAperiodicOfIrreducible {S : Type u} [Fintype S] [DecidableEq S] [Nonempty S] (P : Matrix S S ℝ) [RowStochastic P] [Aperiodic P] [Irreducible P] : GeometricMixing P