Chapman–Kolmogorov equations

StructureMarkov chain with respect to a filtration#✓fully proved

Let \(\mu\) be a measure on \(\Omega\), let \((\mathcal{F}_n)_{n \in \mathbb{N}}\) be a filtration on \(\Omega\), and let \(\kappa\) be a Markov kernel from a measurable space \(S\) to itself. A sequence of random variables \(X_n : \Omega \to S\) is a Markov chain with respect to \((\mathcal{F}_n)\) with transition kernel \(\kappa\) under \(\mu\) if it is adapted to \((\mathcal{F}_n)\) and, for every \(n \in \mathbb{N}\) and every measurable \(B \subseteq S\),

\[\mathbb{E}_\mu[\mathbf{1}_B(X_{n+1}) \mid \mathcal{F}_n] = \kappa(X_n, B)\]

\(\mu\)-almost everywhere. This is the standard form \(P(X_{n+1} \in B \mid \mathcal{F}_n) = \kappa(X_n, B)\) of the Markov property.

structure IsMarkovChain {Ω S : Type*} {m : MeasurableSpace Ω} [MeasurableSpace S]
    (X : ℕ → Ω → S) (ℱ : Filtration ℕ m) (κ : Kernel S S)
    [IsMarkovKernel κ] (μ : Measure Ω) : Prop where
  adapted : Adapted ℱ X
  markov_prop : ∀ n : ℕ, ∀ B : Set S, MeasurableSet B →
    μ[(B.indicator (fun _ => (1 : ℝ))) ∘ (X (n + 1)) | ℱ n] =ᵐ[μ]
      fun ω => (κ (X n ω) B).toReal

Used by 6

Used byChapman–Kolmogorov equations for bounded measurable functions · Chapman–Kolmogorov equations, conditional form · One-step Chapman–Kolmogorov equation for functions · Integrated Chapman–Kolmogorov equation for functions · Chapman–Kolmogorov equations, forward (law) form · Finite Markov chains satisfy the general Markov property

TheoremChapman–Kolmogorov equations, conditional form#✓fully proved

Let \(X = (X_n)_{n \in \mathbb{N}}\) be a Markov chain with state space \(S\), with respect to a filtration \((\mathcal{F}_n)\), with Markov transition kernel \(\kappa\), under a probability measure \(\mu\). Then for all \(m, n \in \mathbb{N}\) and every measurable \(B \subseteq S\),

\[\mathbb{E}_\mu[\mathbf{1}_B(X_{m+n}) \mid \mathcal{F}_m] = \kappa^n(X_m, B)\]

\(\mu\)-almost everywhere, where \(\kappa^n\) is the \(n\)-fold composition of \(\kappa\) (the identity kernel for \(n = 0\)). For \(n = 1\) this is the defining one-step Markov property.

theorem condExp_indicator_eq (hMC : IsMarkovChain X ℱ κ μ)
    (m n : ℕ) {B : Set S} (hB : MeasurableSet B) :
    μ[((B.indicator (fun _ => (1 : ℝ))) ∘ (X (m + n))) | ℱ m] =ᵐ[μ]
      fun ω => ((κ ^ n) (X m ω) B).toReal

Uses 1 · Used by 1

Statement usesMarkov chain with respect to a filtration

Used byChapman–Kolmogorov equations for bounded measurable functions

TheoremChapman–Kolmogorov equations, forward (law) form#✓fully proved

Let \(X = (X_n)_{n \in \mathbb{N}}\) be a Markov chain with state space \(S\), with respect to a filtration, with Markov transition kernel \(\kappa\), under a probability measure \(\mu\), and let \(\kappa^n\) be the \(n\)-fold composition of \(\kappa\) (the identity kernel for \(n = 0\)). Then for all \(m, n \in \mathbb{N}\) the law of \(X_{m+n}\) is the law \(\nu_m\) of \(X_m\) pushed forward through \(\kappa^n\): for every measurable \(B \subseteq S\), \(\mu(X_{m+n} \in B) = \int_S \kappa^n(x, B) \, d\nu_m(x)\).

theorem map_eq_bind_pow (hMC : IsMarkovChain X ℱ κ μ) (m n : ℕ) :
    μ.map (X (m + n)) = (μ.map (X m)).bind (fun x => (κ ^ n) x)

Uses 1 · Used by 2

Statement usesMarkov chain with respect to a filtration

Used byIntegrated Chapman–Kolmogorov equation for functions · One-step forward equation

TheoremChapman–Kolmogorov equations for bounded measurable functions#✓fully proved

For a Markov chain X with transition kernel κ, the conditional expectation of f (X (m + n)) given the past up to time m is the κ ^ n-integral of f evaluated at X m. For n = 1 this is the one-step function form; the general case follows by integrating the canonical conditional-indicator formula over each past-measurable set.

theorem condExp_comp_eq_integral_pow (hMC : IsMarkovChain X ℱ κ μ)
    (m n : ℕ) {f : S → ℝ} (hf : StronglyMeasurable f)
    (hfb : ∃ C, ∀ y, ‖f y‖ ≤ C) :
    μ[ f ∘ X (m + n) | ℱ m ] =ᵐ[μ]
      fun ω => ∫ y, f y ∂ (κ ^ n) (X m ω)

Uses 2 · Used by 1

Statement usesMarkov chain with respect to a filtration

Proof usesChapman–Kolmogorov equations, conditional form

Used byOne-step Chapman–Kolmogorov equation for functions

TheoremOne-step Chapman–Kolmogorov equation for functions#✓fully proved

For a bounded measurable f, the conditional expectation of f (X (k+1)) given ℱ k is the κ-integral of f evaluated at X k.

theorem condExp_one_step_eq_integral (hMC : IsMarkovChain X ℱ κ μ) (k : ℕ)
    {f : S → ℝ} (hf : StronglyMeasurable f) (hfb : ∃ C, ∀ y, ‖f y‖ ≤ C) :
    μ[ f ∘ X (k + 1) | ℱ k ] =ᵐ[μ] fun ω => ∫ y, f y ∂ (κ (X k ω))

Uses 2

Statement usesMarkov chain with respect to a filtration

Proof usesChapman–Kolmogorov equations for bounded measurable functions

TheoremIntegrated Chapman–Kolmogorov equation for functions#✓fully proved

The unconditional expectation of f (X (m + n)) is the expectation of the κ ^ n-integral of f evaluated at X m.

theorem integral_comp_eq (hMC : IsMarkovChain X ℱ κ μ)
    (m n : ℕ) {f : S → ℝ} (hf : StronglyMeasurable f)
    (hfb : ∃ C, ∀ y, ‖f y‖ ≤ C) :
    ∫ ω, f (X (m + n) ω) ∂μ =
      ∫ ω, (∫ y, f y ∂ (κ ^ n) (X m ω)) ∂μ

Uses 2

Statement usesMarkov chain with respect to a filtration

Proof usesChapman–Kolmogorov equations, forward (law) form

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.