The path law of a homogeneous Markov chain

Given an initial law ν on a state space α and a transition kernel κ : Kernel α α, this file builds the law markovChainLaw ν κ of the associated homogeneous Markov chain as a measure on path space ℕ → α, and computes its finite-dimensional laws.

The construction is Mathlib's Ionescu–Tulcea measure ProbabilityTheory.Kernel.trajMeasure for the time-indexed homogeneous kernel family that reads the current state off the trajectory so far and steps by the fixed transition kernel κ. All this file adds is that homogeneous specialization together with the two facts that identify the resulting measure: its time-zero marginal is ν, and it has the Markov property markovChainLaw_map_prefix_succ_eq_compProd, which recursively determines the law of a prefix of length n + 1 from the law of a prefix of length n. On a state space with measurable singletons that recursion unwinds to the familiar product formula markovChainLaw_map_prefix_apply_singleton,

ℙ(X₀ = w 0, …, X n = w n) = ν {w 0} * ∏ i, κ (w i) {w (i + 1)},

which is the defining property of a Markov chain, and the form in which the finite path masses are consumed downstream.

Main definitions

• TauCeti.Probability.markovChainLaw — the path law of the homogeneous Markov chain with initial law ν and transition kernel κ.

Main results

• TauCeti.Probability.markovChainLaw_map_eval_zero — the chain starts from ν.
• TauCeti.Probability.markovChainLaw_map_prefix_succ_eq_compProd — the Markov property: the joint law of a prefix and of the next state is the prefix law extended by one κ-step from its last coordinate.
• TauCeti.Probability.markovChainLaw_map_pair_succ, TauCeti.Probability.markovChainLaw_map_eval_succ — the two-coordinate form of the Markov property and the forward recursion for the one-dimensional marginals.
• TauCeti.Probability.markovChainLaw_map_prefix_apply_singleton — on a state space with measurable singletons, the mass of a finite path is the initial weight times the product of the transition weights.

References

• Olav Kallenberg, Foundations of Modern Probability, 2nd edition, Springer, 2002, Chapter 7, for the path law of a Markov chain with a given initial law and transition kernel.

noncomputable def TauCeti.Probability.markovChainLaw {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.Measure (ℕ → α)

The path law of a homogeneous Markov chain with initial law ν and transition kernel κ: the Ionescu–Tulcea measure of the time-indexed homogeneous family markovStep κ induced by the fixed transition kernel κ.

Equations

• TauCeti.Probability.markovChainLaw ν κ = ProbabilityTheory.Kernel.trajMeasure ν (TauCeti.Probability.markovStep✝ κ)

instance TauCeti.Probability.instIsProbabilityMeasureForallNatMarkovChainLaw {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (markovChainLaw ν κ)

@[simp]

theorem TauCeti.Probability.markovChainLaw_map_eval_zero {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.Measure.map (fun (x : ℕ → α) => x 0) (markovChainLaw ν κ) = ν

The chain starts from its initial law.

theorem TauCeti.Probability.markovChainLaw_map_prefix_succ_eq_compProd {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → α) => (fun (i : Fin (n + 1)) => x ↑i, x (n + 1))) (markovChainLaw ν κ) = (MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin (n + 1)) => x ↑i) (markovChainLaw ν κ)).compProd (κ.comap (fun (w : Fin (n + 1) → α) => w (Fin.last n)) ⋯)

The Markov property of the chain. The joint law of the length-n + 1 prefix (X 0, …, X n) and of the next state X (n + 1) is the prefix law extended by one κ-step out of the last coordinate of the prefix. Together with markovChainLaw_map_eval_zero this determines all the finite-dimensional laws of the chain.

theorem TauCeti.Probability.markovChainLaw_map_pair_succ {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → α) => (x n, x (n + 1))) (markovChainLaw ν κ) = (MeasureTheory.Measure.map (fun (x : ℕ → α) => x n) (markovChainLaw ν κ)).compProd κ

The one-step transition law of the chain. The joint law of the states at times n and n + 1 is the time-n law extended by κ; this is the Markov property read off two coordinates rather than a whole prefix.

@[simp]

theorem TauCeti.Probability.markovChainLaw_map_eval_succ {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) : MeasureTheory.Measure.map (fun (x : ℕ → α) => x (n + 1)) (markovChainLaw ν κ) = (MeasureTheory.Measure.map (fun (x : ℕ → α) => x n) (markovChainLaw ν κ)).bind ⇑κ

The time-n laws of the chain satisfy the forward recursion: the law at time n + 1 is the law at time n pushed through the transition kernel. With markovChainLaw_map_eval_zero this identifies every one-dimensional marginal of the chain.

theorem TauCeti.Probability.markovChainLaw_map_prefix_apply_singleton {α : Type u_1} [MeasurableSpace α] (ν : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] [MeasureTheory.IsProbabilityMeasure ν] [MeasurableSingletonClass α] (n : ℕ) (w : Fin (n + 1) → α) : (MeasureTheory.Measure.map (fun (x : ℕ → α) (i : Fin (n + 1)) => x ↑i) (markovChainLaw ν κ)) {w} = ν {w 0} * ∏ i : Fin n, (κ (w i.castSucc)) {w i.succ}

The finite path masses of the chain. On a state space with measurable singletons the mass a homogeneous Markov chain gives to a finite path is the initial weight of its first state times the product of the transition weights along it. This is the defining product form of the finite-dimensional laws of a Markov chain.