Finite-dimensional distributions of Markov chains

DefinitionFinite-dimensional distribution of a Markov chain#✓fully proved

For a measure \(\mu\) on a measurable space \(S\), a kernel \(\kappa\) from \(S\) to \(S\), a natural number \(n\) and sets \(A_0, \dots, A_n \subseteq S\), the finite-dimensional distribution \(\mathrm{FDD}_n(\mu, \kappa; A_0, \dots, A_n) \in [0, \infty]\) is defined by recursion on \(n\): \(\mathrm{FDD}_0(\mu, \kappa; A_0) = \mu(A_0)\) and \(\mathrm{FDD}_{n+1}(\mu, \kappa; A_0, \dots, A_{n+1}) = \int_{A_0} \mathrm{FDD}_n(\kappa(x), \kappa; A_1, \dots, A_{n+1}) \, d\mu(x)\). Unfolded, it is the iterated integral

\[ \int_{A_0} \mu(dx_0) \int_{A_1} \kappa(x_0, dx_1) \cdots \int_{A_n} \kappa(x_{n-1}, dx_n). \]

When \(\mu\) is a probability measure and \(\kappa\) a Markov kernel, this is the probability that a chain with initial distribution \(\mu\) and transition kernel \(\kappa\) visits \(A_0, A_1, \dots, A_n\) at consecutive times.

noncomputable def markovFDD {S : Type*} [MeasurableSpace S]
    (mu : Measure S) (kappa : Kernel S S) : (n : Nat) -> (Fin (n + 1) -> Set S) -> ENNReal
  | 0, A => mu (A 0)
  | n + 1, A => ∫⁻ x in A 0, markovFDD (kappa x) kappa n (fun i => A i.succ) ∂mu

Used by 3

Used byFinite-dimensional distributions given the past · Finite-dimensional distributions of a Markov chain · Measurability of the finite-dimensional distributions in the starting state

LemmaMeasurability of the finite-dimensional distributions in the starting state#✓fully proved

Let \(\kappa\) be a Markov kernel on a measurable space \(S\), let \(n\) be a natural number and let \(A_0, \dots, A_n\) be measurable subsets of \(S\). Write \(\mathrm{FDD}_n(\mu, \kappa; A_0, \dots, A_n)\) for the finite-dimensional distribution of a Markov chain with initial measure \(\mu\) and transition kernel \(\kappa\). Then the map \(x \mapsto \mathrm{FDD}_n(\kappa(x), \kappa; A_0, \dots, A_n)\) from \(S\) to \([0, \infty]\) is measurable.

This is the regularity needed to integrate the finite-dimensional distributions against a starting distribution.

lemma markovFDD_measurable {S : Type*} [MeasurableSpace S]
    (kappa : Kernel S S) [IsMarkovKernel kappa]
    (n : Nat) (A : Fin (n + 1) -> Set S) (hA : forall i, MeasurableSet (A i)) :
    Measurable (fun x => markovFDD (kappa x) kappa n A)

Uses 1 · Used by 2

Statement usesFinite-dimensional distribution of a Markov chain

Used byFinite-dimensional distributions given the past · Finite-dimensional distributions of a Markov chain

LemmaThe σ-algebras generated by a sequence increase#✓fully proved

Let \(X_0, X_1, \dots\) be maps from a measurable space \(\Omega\) to a measurable space \(S\), and for each \(k\) let \(\sigma(X_0, \dots, X_k)\) be the σ-algebra on \(\Omega\) generated by \(\omega \mapsto (X_0(\omega), \dots, X_k(\omega))\), with the product σ-algebra on \(S^{k+1}\). Then \(\sigma(X_0, \dots, X_k) \subseteq \sigma(X_0, \dots, X_{k+1})\) for every \(k\).

lemma comap_sigma_mono
    {Omega S : Type*} [MeasurableSpace Omega] [MeasurableSpace S]
    (X : Nat -> Omega -> S) (k : Nat) :
    MeasurableSpace.comap (fun omega => fun i : Fin (k + 1) => X i omega) MeasurableSpace.pi ≤
    MeasurableSpace.comap (fun omega => fun i : Fin (k + 2) => X i omega) MeasurableSpace.pi

Used by 1

Used byAdding the next step to a past event

LemmaAdding the next step to a past event#✓fully proved

Let \(X_0, X_1, \dots\) be maps from a measurable space \(\Omega\) to a measurable space \(S\), and write \(\sigma(X_0, \dots, X_k)\) for the σ-algebra on \(\Omega\) generated by \(\omega \mapsto (X_0(\omega), \dots, X_k(\omega))\), with the product σ-algebra on \(S^{k+1}\). If \(C\) is measurable with respect to \(\sigma(X_0, \dots, X_k)\) and \(B \subseteq S\) is measurable, then \(C \cap X_{k+1}^{-1}(B)\) is measurable with respect to \(\sigma(X_0, \dots, X_{k+1})\).

lemma comap_inter_preimage
    {Omega S : Type*} [MeasurableSpace Omega] [MeasurableSpace S]
    (X : Nat -> Omega -> S) (k : Nat)
    (C : Set Omega) (B : Set S) (hB : MeasurableSet B)
    (hC : @MeasurableSet Omega (MeasurableSpace.comap
      (fun omega => fun i : Fin (k + 1) => X i omega) MeasurableSpace.pi) C) :
    @MeasurableSet Omega (MeasurableSpace.comap
      (fun omega => fun i : Fin (k + 2) => X i omega) MeasurableSpace.pi)
      (C ∩ X (k + 1) ⁻¹' B)

Uses 1 · Used by 1

Proof usesThe σ-algebras generated by a sequence increase

Used byFinite-dimensional distributions given the past

LemmaThe Markov property for measurable functions#✓fully proved

Let \(P\) be a probability measure on a measurable space \(\Omega\), let \(X_0, X_1, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\), and let \(\kappa\) be a Markov kernel on \(S\). Write \(\sigma(X_0, \dots, X_k)\) for the σ-algebra on \(\Omega\) generated by \(\omega \mapsto (X_0(\omega), \dots, X_k(\omega))\), with the product σ-algebra on \(S^{k+1}\). Suppose that for every \(k\), every measurable \(B \subseteq S\) and every \(C\) measurable with respect to \(\sigma(X_0, \dots, X_k)\), \(\int_C \mathbf{1}_{X_{k+1}^{-1}(B)} \, dP = \int_C \kappa(X_k(\omega), B) \, dP(\omega)\). Then for every \(k\), every \(C\) measurable with respect to \(\sigma(X_0, \dots, X_k)\) and every measurable \(f : S \to [0, \infty]\), \(\int_C f(X_{k+1}(\omega)) \, dP(\omega) = \int_C \int_S f(y) \, \kappa(X_k(\omega), dy) \, dP(\omega)\).

MathlibExt.Probability.MarkovChainFDD.lintegral_measurable_extension · 16 lines

lemma lintegral_measurable_extension
    {Omega S : Type*} [MeasurableSpace Omega] [MeasurableSpace S]
    (P : Measure Omega) [IsProbabilityMeasure P]
    (X : Nat -> Omega -> S) (hmeas : forall i, Measurable (X i))
    (kappa : Kernel S S) [IsMarkovKernel kappa]
    (hmarkov : forall (k : Nat) (B : Set S), MeasurableSet B ->
      forall (C : Set Omega),
        @MeasurableSet Omega (MeasurableSpace.comap
          (fun omega => fun i : Fin (k + 1) => X i omega) MeasurableSpace.pi) C ->
        ∫⁻ omega in C, (X (k + 1) ⁻¹' B).indicator (fun _ => (1 : ENNReal)) omega ∂P =
        ∫⁻ omega in C, kappa (X k omega) B ∂P)
    (k : Nat) (C : Set Omega)
    (hC_comap : @MeasurableSet Omega (MeasurableSpace.comap
      (fun omega => fun i : Fin (k + 1) => X i omega) MeasurableSpace.pi) C)
    (f : S -> ENNReal) (hf : Measurable f) :
    ∫⁻ omega in C, f (X (k + 1) omega) ∂P = ∫⁻ omega in C, (∫⁻ y, f y ∂kappa (X k omega)) ∂P

Used by 1

Used byFinite-dimensional distributions given the past

LemmaRestricting an integral to a preimage#✓fully proved

Let \(P\) be a measure on a measurable space \(\Omega\), let \(X : \Omega \to S\) be a measurable map to a measurable space \(S\), let \(A \subseteq S\) be measurable, let \(C \subseteq \Omega\) be any set and let \(f : S \to [0, \infty]\) be any function. Then \(\int_{C \cap X^{-1}(A)} f(X(\omega)) \, dP(\omega) = \int_C \mathbf{1}_A(X(\omega)) \, f(X(\omega)) \, dP(\omega)\).

lemma set_lintegral_inter_preimage
    {Omega S : Type*} [MeasurableSpace Omega] [MeasurableSpace S]
    (P : Measure Omega) (X : Omega -> S) (hX : Measurable X)
    (A : Set S) (hA : MeasurableSet A) (C : Set Omega)
    (f : S -> ENNReal) :
    ∫⁻ omega in C ∩ X ⁻¹' A, f (X omega) ∂P = ∫⁻ omega in C, A.indicator f (X omega) ∂P

Used by 1

Used byFinite-dimensional distributions given the past

TheoremFinite-dimensional distributions given the past#✓fully proved

Let \(P\) be a probability measure on a measurable space \(\Omega\), let \(X_0, X_1, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\), and let \(\kappa\) be a Markov kernel on \(S\). Write \(\sigma(X_0, \dots, X_k)\) for the σ-algebra on \(\Omega\) generated by \(\omega \mapsto (X_0(\omega), \dots, X_k(\omega))\), with the product σ-algebra on \(S^{k+1}\), and \(\mathrm{FDD}_n(\mu, \kappa; A_0, \dots, A_n)\) for the finite-dimensional distribution of a Markov chain with initial measure \(\mu\) and transition kernel \(\kappa\). Suppose that for every \(k\), every measurable \(B \subseteq S\) and every \(C\) measurable with respect to \(\sigma(X_0, \dots, X_k)\), \(\int_C \mathbf{1}_{X_{k+1}^{-1}(B)} \, dP = \int_C \kappa(X_k(\omega), B) \, dP(\omega)\). Then for all natural numbers \(n\) and \(j\), all measurable sets \(A_0, \dots, A_n \subseteq S\) and every measurable set \(C \subseteq \Omega\) that is also measurable with respect to \(\sigma(X_0, \dots, X_j)\),

\[ P\Bigl(C \cap \bigcap_{i=0}^{n} X_{j+1+i}^{-1}(A_i)\Bigr) = \int_C \mathrm{FDD}_n(\kappa(X_j(\omega)), \kappa; A_0, \dots, A_n) \, dP(\omega). \]

MathlibExt.Probability.MarkovChainFDD.markov_chain_fdd_aux · 18 lines

theorem markov_chain_fdd_aux
    {Omega S : Type*} [MeasurableSpace Omega] [MeasurableSpace S]
    (P : Measure Omega) [IsProbabilityMeasure P]
    (X : Nat -> Omega -> S) (hmeas : forall i, Measurable (X i))
    (kappa : Kernel S S) [IsMarkovKernel kappa]
    (hmarkov : forall (k : Nat) (B : Set S), MeasurableSet B ->
      forall (C : Set Omega),
        @MeasurableSet Omega (MeasurableSpace.comap
          (fun omega => fun i : Fin (k + 1) => X i omega) MeasurableSpace.pi) C ->
        ∫⁻ omega in C, (X (k + 1) ⁻¹' B).indicator (fun _ => (1 : ENNReal)) omega ∂P =
        ∫⁻ omega in C, kappa (X k omega) B ∂P)
    (n : Nat) (j : Nat)
    (A : Fin (n + 1) -> Set S) (hA : forall i, MeasurableSet (A i))
    (C : Set Omega) (hC_meas : MeasurableSet C)
    (hC_comap : @MeasurableSet Omega (MeasurableSpace.comap
      (fun omega => fun i : Fin (j + 1) => X i omega) MeasurableSpace.pi) C) :
    P (C ∩ ⋂ i : Fin (n + 1), X (j + 1 + ↑i) ⁻¹' A i) =
    ∫⁻ omega in C, markovFDD (kappa (X j omega)) kappa n A ∂P

Uses 5 · Used by 1

Statement usesFinite-dimensional distribution of a Markov chain

Proof usesAdding the next step to a past event · The Markov property for measurable functions · Measurability of the finite-dimensional distributions in the starting state · Restricting an integral to a preimage

Used byFinite-dimensional distributions of a Markov chain

TheoremFinite-dimensional distributions of a Markov chain#✓fully proved

Let \(P\) be a probability measure on a measurable space \(\Omega\), let \(X_0, X_1, \dots\) be measurable maps from \(\Omega\) to a measurable space \(S\), and let \(\kappa\) be a Markov kernel on \(S\). Write \(\sigma(X_0, \dots, X_k)\) for the σ-algebra on \(\Omega\) generated by \(\omega \mapsto (X_0(\omega), \dots, X_k(\omega))\), with the product σ-algebra on \(S^{k+1}\). Suppose \(X\) is a Markov chain with transition kernel \(\kappa\): for every \(k\), every measurable \(B \subseteq S\) and every \(C\) measurable with respect to \(\sigma(X_0, \dots, X_k)\), \(\int_C \mathbf{1}_{X_{k+1}^{-1}(B)} \, dP = \int_C \kappa(X_k(\omega), B) \, dP(\omega)\). Let \(\mu = P \circ X_0^{-1}\) be the initial distribution. Then for every natural number \(n\) and all measurable sets \(A_0, \dots, A_n \subseteq S\),

\[ P(X_i \in A_i \text{ for } 0 \le i \le n) = \int_{A_0} \mu(dx_0) \int_{A_1} \kappa(x_0, dx_1) \cdots \int_{A_n} \kappa(x_{n-1}, dx_n), \]

where the right-hand side is the finite-dimensional distribution \(\mathrm{FDD}_n(\mu, \kappa; A_0, \dots, A_n)\) of a Markov chain with initial measure \(\mu\) and transition kernel \(\kappa\).

theorem markov_chain_finite_dimensional_distributions
    {Omega S : Type*} [MeasurableSpace Omega] [MeasurableSpace S]
    (P : Measure Omega) [IsProbabilityMeasure P]
    (X : Nat -> Omega -> S) (hmeas : forall i, Measurable (X i))
    (kappa : Kernel S S) [IsMarkovKernel kappa]
    (n : Nat) (A : Fin (n + 1) -> Set S) (hA : forall i, MeasurableSet (A i))
    (hmarkov : forall (k : Nat) (B : Set S), MeasurableSet B ->
      forall (C : Set Omega),
        @MeasurableSet Omega (MeasurableSpace.comap
          (fun omega => fun i : Fin (k + 1) => X i omega) MeasurableSpace.pi) C ->
        ∫⁻ omega in C, (X (k + 1) ⁻¹' B).indicator (fun _ => (1 : ENNReal)) omega ∂P =
        ∫⁻ omega in C, kappa (X k omega) B ∂P) :
    P (⋂ i : Fin (n + 1), X i ⁻¹' A i) = markovFDD (P.map (X 0)) kappa n A

Uses 3

Statement usesFinite-dimensional distribution of a Markov chain

Proof usesMeasurability of the finite-dimensional distributions in the starting state · Finite-dimensional distributions given the past

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.