theorem IsMarkovChain.markov_property {Ω : Type u_1} {S : Type u_2} {m : MeasurableSpace Ω} [MeasurableSpace S] {X : ℕ → Ω → S} {ℱ : MeasureTheory.Filtration ℕ m} {κ : ProbabilityTheory.Kernel S S} [ProbabilityTheory.IsMarkovKernel κ] {μ : MeasureTheory.Measure Ω} (hMC : IsMarkovChain X ℱ κ μ) (n : ℕ) {B : Set S} (hB : MeasurableSet B) : μ[(B.indicator fun (x : S) => 1) ∘ X (n + 1) | ↑ℱ n] =ᵐ[μ] fun (ω : Ω) => ((κ (X n ω)) B).toReal

The defining Markov property of an IsMarkovChain, re-exported as a top-level lemma: for any measurable set B ⊆ S and any n,

E[1_B ∘ X (n+1) | ℱ n] = κ (X n ·) B μ-a.e.,

i.e. P(X_{n+1} ∈ B | ℱ_n) = κ(X_n, B).

def shiftPath {S : Type u_3} (n : ℕ) : (ℕ → S) → ℕ → S

The discrete-time shift on path space: shiftPath n ω is the path k ↦ ω (n + k), i.e. the trajectory ω viewed from time n onward.

theorem measurable_shiftPath {S : Type u_3} [MeasurableSpace S] (n : ℕ) : Measurable (shiftPath n)

The time-n shift map on path space is measurable.

noncomputable def pathFiltration (S : Type u_3) [MeasurableSpace S] : MeasureTheory.Filtration ℕ MeasurableSpace.pi

The canonical filtration on the path space ℕ → S: at time n it is the σ-algebra generated by the coordinate maps ω ↦ ω i for i ≤ n.

noncomputable def MarkovChainPathMeasure (S : Type u_3) [MeasurableSpace S] (μ : MeasureTheory.Measure S) (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.Measure (ℕ → S)

The law on path space ℕ → S of the Markov chain with initial distribution μ and transition kernel κ. Built via the trajectory measure of the lifted kernel markovLiftKernel κ.

instance MarkovChainPathMeasure.isProbabilityMeasure (S : Type u_3) [MeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsProbabilityMeasure μ] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.IsProbabilityMeasure (MarkovChainPathMeasure S μ κ)

When the initial distribution μ is a probability measure, the resulting path measure is itself a probability measure on ℕ → S.

instance MarkovChainPathMeasure.isFiniteMeasure (S : Type u_3) [MeasurableSpace S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.IsFiniteMeasure (MarkovChainPathMeasure S μ κ)

When the initial distribution μ is finite, the resulting path measure is itself a finite measure on ℕ → S.

noncomputable def markovExpectation (S : Type u_3) [MeasurableSpace S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (Y : (ℕ → S) → ℝ) (x : S) : ℝ

The expectation E_x Y of a path functional Y under the Markov chain started from the point x ∈ S. It is the integral of Y against the path measure with initial distribution δ_x.

theorem measurable_markovExpectation (S : Type u_3) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (Y : (ℕ → S) → ℝ) (hY_meas : Measurable Y) (hY_bdd : ∃ (C : ℝ), ∀ (ω : ℕ → S), |Y ω| ≤ C) : Measurable (markovExpectation S κ Y)

The map x ↦ E_x Y = markovExpectation S κ Y x is measurable in the starting state x, provided Y is bounded measurable on path space and S is a standard Borel space.

theorem integral_shiftPath_traj_eq_markovExpectation (S : Type u_3) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (Y : (ℕ → S) → ℝ) (hY_meas : Measurable Y) (hY_bdd : ∃ (C : ℝ), ∀ (ω : ℕ → S), |Y ω| ≤ C) (n : ℕ) (x₀ : ↥(Finset.Iic n) → S) : ∫ (ω : ℕ → S), Y (shiftPath n ω) ∂(ProbabilityTheory.Kernel.traj (markovLiftKernel κ) n) x₀ = ∫ (ω : ℕ → S), Y ω ∂MarkovChainPathMeasure S (MeasureTheory.Measure.dirac (x₀ ⟨n, ⋯⟩)) κ

Identifies an integral on the trajectory kernel with markovExpectation: the integral of Y against the shifted trajectory starting from a finite history x₀ equals E_{x₀ n} Y, the expected value of Y for the chain started from the last coordinate of x₀.

theorem pathFiltration_le_pi (S : Type u_3) [MeasurableSpace S] (n : ℕ) : ↑(pathFiltration S) n ≤ MeasurableSpace.pi

Each level of the pathFiltration is contained in the product σ-algebra on ℕ → S.

theorem markov_setIntegral_shift (S : Type u_3) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (Y : (ℕ → S) → ℝ) (hY_meas : Measurable Y) (hY_bdd : ∃ (C : ℝ), ∀ (ω : ℕ → S), |Y ω| ≤ C) (n : ℕ) (A : Set (ℕ → S)) (hA : MeasurableSet A) : have P_μ := MarkovChainPathMeasure S μ κ; ∫ (ω : ℕ → S) in A, (Y ∘ shiftPath n) ω ∂P_μ = ∫ (ω : ℕ → S) in A, markovExpectation S κ Y (ω n) ∂P_μ

Set-integral form of the Markov property for the Markov chain path measure. For any bounded measurable path functional Y and any set A measurable with respect to pathFiltration S n,

∫_A Y(shiftPath n ω) dP_μ = ∫_A markovExpectation S κ Y (ω n) dP_μ.

This is the analogue of setIntegral_shift_eq_pathExpectation for discrete-time Markov chains.

theorem markov_property_full (S : Type u_3) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S] (μ : MeasureTheory.Measure S) [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel κ] (Y : (ℕ → S) → ℝ) (hY_meas : Measurable Y) (hY_bdd : ∃ (C : ℝ), ∀ (ω : ℕ → S), |Y ω| ≤ C) (n : ℕ) : have P_μ := MarkovChainPathMeasure S μ κ; P_μ[Y ∘ shiftPath n | ↑(pathFiltration S) n] =ᵐ[P_μ] fun (ω : ℕ → S) => markovExpectation S κ Y (ω n)

Markov property for a discrete-time Markov chain (conditional-expectation form). For any bounded measurable path functional Y on ℕ → S,

E_μ[Y ∘ shiftPath n | pathFiltration n] = (ω ↦ E_{ω n} Y) P_μ-a.e.,

i.e. conditioning on the trajectory up to time n only depends on the value ω n, and the conditional expectation of Y(shiftPath n ·) equals the expectation E_{ω n} Y of Y under the chain restarted from ω n.