LeanPool.RlTheoryInLean.Probability.MarkovChain.Finite.Defs

def ProbabilityTheory.MarkovChain.Finite.kernelMat {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) : Matrix S S ℝ

Matrix representation of a finite-state Markov transition kernel.

Equations

• ProbabilityTheory.MarkovChain.Finite.kernelMat M = Matrix.of fun (a b : S) => ((M.kernel a) {b}).toReal

def ProbabilityTheory.MarkovChain.Finite.initVec {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) : S → ℝ

Vector representation of the initial distribution of a finite Markov chain.

Equations

• ProbabilityTheory.MarkovChain.Finite.initVec M s = ↑(M.init {s})

theorem ProbabilityTheory.MarkovChain.Finite.prob_sum_to_one {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : ∑ s : S, (μ {s}).toReal = 1

instance ProbabilityTheory.MarkovChain.Finite.instStochasticVecInitVec {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] (M : HomMarkovChainSpec S) : StochasticMatrix.StochasticVec (initVec M)

instance ProbabilityTheory.MarkovChain.Finite.instRowStochasticKernelMat {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] (M : HomMarkovChainSpec S) : StochasticMatrix.RowStochastic (kernelMat M)

theorem ProbabilityTheory.MarkovChain.Finite.kernel_apply_eq_mat_apply {S : Type u} [MeasurableSpace S] (M : HomMarkovChainSpec S) (s s' : S) : ((M.kernel s) {s'}).toReal = kernelMat M s s'

theorem ProbabilityTheory.MarkovChain.Finite.integral_fintype_kernel_iter {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] {α : Type u_1} [NormedAddCommGroup α] [NormedSpace ℝ α] [CompleteSpace α] [DecidableEq S] (M : HomMarkovChainSpec S) (n : ℕ) (f : S → α) (s : S) : ∫ (s' : S), f s' ∂(M.kernel.iter n) s = ∑ s' : S, (kernelMat M ^ n) s s' • f s'