noncomputable def markovLiftKernel {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) (n : ℕ) : ProbabilityTheory.Kernel (↥(Finset.Iic n) → S) S

Lift the Markov kernel κ : S → S to a kernel on tuples (x_0, …, x_n) by reading off the last coordinate x_n and applying κ. This is the form required by the Ionescu–Tulcea trajectory construction.

instance markovLiftKernel.instIsMarkovKernel {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : ProbabilityTheory.IsMarkovKernel (markovLiftKernel κ n)

The lifted kernel markovLiftKernel κ n is again a Markov kernel whenever κ is.

noncomputable def markovChainMeasure {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure S) : MeasureTheory.Measure (ℕ → S)

The canonical measure P_μ on path space ℕ → S of the Markov chain with initial distribution μ and transition kernel κ, built via the Ionescu–Tulcea trajectory measure.

instance markovChainMeasure.isProbabilityMeasure {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] : MeasureTheory.IsProbabilityMeasure (markovChainMeasure κ μ)

markovChainMeasure κ μ is a probability measure on path space.

theorem markovChainMeasure_initial_distribution {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure S) : MeasureTheory.Measure.map (fun (ω : ℕ → S) => ω 0) (markovChainMeasure κ μ) = μ

Under the canonical Markov-chain measure, the law of the initial state ω 0 is the initial distribution μ.

theorem markovChainMeasure_condDistrib {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) [StandardBorelSpace S] [Nonempty S] : ⇑(ProbabilityTheory.condDistrib (fun (x : ℕ → S) => x (n + 1)) (Preorder.frestrictLe n) (markovChainMeasure κ μ)) =ᵐ[MeasureTheory.Measure.map (Preorder.frestrictLe n) (markovChainMeasure κ μ)] ⇑(markovLiftKernel κ n)

Under the canonical Markov-chain measure, the regular conditional distribution of the next state X_{n+1} given the history (X_0, …, X_n) agrees almost everywhere with the lifted transition kernel markovLiftKernel κ n. This is the defining Markov property.

theorem markov_chain_construction {S : Type u_1} [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace S] [Nonempty S] : ∃ (P : MeasureTheory.Measure (ℕ → S)) (x : MeasureTheory.IsProbabilityMeasure P), MeasureTheory.Measure.map (fun (ω : ℕ → S) => ω 0) P = μ ∧ ∀ (n : ℕ), ⇑(ProbabilityTheory.condDistrib (fun (x : ℕ → S) => x (n + 1)) (Preorder.frestrictLe n) P) =ᵐ[MeasureTheory.Measure.map (Preorder.frestrictLe n) P] ⇑(markovLiftKernel κ n)

Markov chain construction theorem.

Given a Markov transition kernel κ : S → S and an initial distribution μ on a standard Borel space S, there exists a probability measure P on path space ℕ → S such that

• the law of ω 0 under P is μ, and
• for every n, the conditional law of ω (n+1) given the past (ω 0, …, ω n) is the transition kernel κ applied to the current state.

That is, the sequence (X_0, X_1, …) sampled from P is a Markov chain with initial distribution μ and transitions κ.