noncomputable def markovFDD {S : Type u_1} [MeasurableSpace S] (mu : MeasureTheory.Measure S) (kappa : ProbabilityTheory.Kernel S S) (n : ℕ) : (Fin (n + 1) → Set S) → ENNReal

The finite-dimensional distribution of a Markov chain with initial distribution mu and transition kernel kappa. Concretely, markovFDD mu kappa n A computes the iterated integral

∫_{A 0} ∫_{A 1} ⋯ ∫_{A n} 1 dκ(xₙ₋₁) ⋯ dκ(x₀) dμ,

i.e. the probability that the chain visits the sets A 0, A 1, …, A n at consecutive times.

theorem markovFDD_measurable {S : Type u_1} [MeasurableSpace S] (kappa : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel kappa] (n : ℕ) (A : Fin (n + 1) → Set S) (hA : ∀ (i : Fin (n + 1)), MeasurableSet (A i)) : Measurable fun (x : S) => markovFDD (kappa x) kappa n A

For each n and tuple of measurable sets A, the function x ↦ markovFDD (kappa x) kappa n A is measurable in the starting state x. This is the key regularity statement needed to integrate the FDDs against a starting distribution.

theorem comap_sigma_mono {Omega : Type u_1} {S : Type u_2} [MeasurableSpace Omega] [MeasurableSpace S] (X : ℕ → Omega → S) (k : ℕ) : MeasurableSpace.comap (fun (omega : Omega) (i : Fin (k + 1)) => X (↑i) omega) MeasurableSpace.pi ≤ MeasurableSpace.comap (fun (omega : Omega) (i : Fin (k + 2)) => X (↑i) omega) MeasurableSpace.pi

The σ-algebra generated by (X 0, …, X k) is contained in the one generated by (X 0, …, X (k+1)). In other words, the σ-algebras σ(X 0, …, X k) are monotone in k.

theorem comap_inter_preimage {Omega : Type u_1} {S : Type u_2} [MeasurableSpace Omega] [MeasurableSpace S] (X : ℕ → Omega → S) (k : ℕ) (C : Set Omega) (B : Set S) (hB : MeasurableSet B) (hC : MeasurableSet C) : MeasurableSet (C ∩ X (k + 1) ⁻¹' B)

If C is measurable with respect to σ(X 0, …, X k) and B is a measurable subset of the state space, then C ∩ X (k+1)⁻¹ B is measurable with respect to σ(X 0, …, X (k+1)).

theorem lintegral_measurable_extension {Omega : Type u_1} {S : Type u_2} [MeasurableSpace Omega] [MeasurableSpace S] (P : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Omega → S) (hmeas : ∀ (i : ℕ), Measurable (X i)) (kappa : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel kappa] (hmarkov : ∀ (k : ℕ) (B : Set S), MeasurableSet B → ∀ (C : Set Omega), MeasurableSet C → ∫⁻ (omega : Omega) in C, (X (k + 1) ⁻¹' B).indicator (fun (x : Omega) => 1) omega ∂P = ∫⁻ (omega : Omega) in C, (kappa (X k omega)) B ∂P) (k : ℕ) (C : Set Omega) (hC_comap : MeasurableSet C) (f : S → ENNReal) (hf : Measurable f) : ∫⁻ (omega : Omega) in C, f (X (k + 1) omega) ∂P = ∫⁻ (omega : Omega) in C, ∫⁻ (y : S), f y ∂kappa (X k omega) ∂P

Promotes the Markov property from indicator functions to general measurable functions: under the Markov hypothesis on indicators of measurable sets, for every measurable f : S → ℝ≥0∞ and every set C measurable with respect to σ(X 0, …, X k), ∫_C f (X (k+1) ω) dP = ∫_C (∫ f dκ (X k ω)) dP.

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

Restriction–indicator identity used in the inductive step: integrating f ∘ X over C ∩ X⁻¹ A is the same as integrating the indicator A.indicator f ∘ X over C.

theorem markov_chain_fdd_aux {Omega : Type u_1} {S : Type u_2} [MeasurableSpace Omega] [MeasurableSpace S] (P : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Omega → S) (hmeas : ∀ (i : ℕ), Measurable (X i)) (kappa : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel kappa] (hmarkov : ∀ (k : ℕ) (B : Set S), MeasurableSet B → ∀ (C : Set Omega), MeasurableSet C → ∫⁻ (omega : Omega) in C, (X (k + 1) ⁻¹' B).indicator (fun (x : Omega) => 1) omega ∂P = ∫⁻ (omega : Omega) in C, (kappa (X k omega)) B ∂P) (n j : ℕ) (A : Fin (n + 1) → Set S) (hA : ∀ (i : Fin (n + 1)), MeasurableSet (A i)) (C : Set Omega) (hC_meas : MeasurableSet C) (hC_comap : MeasurableSet C) : P (C ∩ ⋂ (i : Fin (n + 1)), X (j + 1 + ↑i) ⁻¹' A i) = ∫⁻ (omega : Omega) in C, markovFDD (kappa (X j omega)) kappa n A ∂P

Auxiliary form of the finite-dimensional distribution formula, allowing an arbitrary "prefix" event C measurable with respect to σ(X 0, …, X j). It states P(C ∩ ⋂_{i ≤ n} {X (j+1+i) ∈ A i}) = ∫_C markovFDD (κ (X j ω)) κ n A dP, i.e. conditioning on the past up to time j, the joint distribution of the next n+1 steps is given by markovFDD started from X j ω.

theorem markov_chain_fdd {Omega : Type u_1} {S : Type u_2} [MeasurableSpace Omega] [MeasurableSpace S] (P : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Omega → S) (hmeas : ∀ (i : ℕ), Measurable (X i)) (kappa : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel kappa] (n : ℕ) (A : Fin (n + 1) → Set S) (hA : ∀ (i : Fin (n + 1)), MeasurableSet (A i)) (hmarkov : ∀ (k : ℕ) (B : Set S), MeasurableSet B → ∀ (C : Set Omega), MeasurableSet C → ∫⁻ (omega : Omega) in C, (X (k + 1) ⁻¹' B).indicator (fun (x : Omega) => 1) omega ∂P = ∫⁻ (omega : Omega) in C, (kappa (X k omega)) B ∂P) : P (⋂ (i : Fin (n + 1)), X ↑i ⁻¹' A i) = markovFDD (MeasureTheory.Measure.map (X 0) P) kappa n A

Finite-dimensional distributions of a Markov chain. If X is a sequence of random variables with transition kernel κ (in the sense expressed by hmarkov), then for any measurable sets A 0, …, A n,

P(⋂ i : Fin (n+1), {X i ∈ A i}) = markovFDD (P ∘ X 0⁻¹) κ n A.

This is the standard formula expressing the law of (X 0, …, X n) as an iterated integral against the initial distribution and the transition kernel.

theorem markov_chain_finite_dimensional_distributions {Omega : Type u_1} {S : Type u_2} [MeasurableSpace Omega] [MeasurableSpace S] (P : MeasureTheory.Measure Omega) [MeasureTheory.IsProbabilityMeasure P] (X : ℕ → Omega → S) (hmeas : ∀ (i : ℕ), Measurable (X i)) (kappa : ProbabilityTheory.Kernel S S) [ProbabilityTheory.IsMarkovKernel kappa] (n : ℕ) (A : Fin (n + 1) → Set S) (hA : ∀ (i : Fin (n + 1)), MeasurableSet (A i)) (hmarkov : ∀ (k : ℕ) (B : Set S), MeasurableSet B → ∀ (C : Set Omega), MeasurableSet C → ∫⁻ (omega : Omega) in C, (X (k + 1) ⁻¹' B).indicator (fun (x : Omega) => 1) omega ∂P = ∫⁻ (omega : Omega) in C, (kappa (X k omega)) B ∂P) : P (⋂ (i : Fin (n + 1)), X ↑i ⁻¹' A i) = markovFDD (MeasureTheory.Measure.map (X 0) P) kappa n A

Markov chain finite-dimensional distributions (textbook statement). If X is any Markov chain with initial distribution μ = P ∘ (X 0)⁻¹ and transition kernel κ, then the finite-dimensional probabilities are given by

P(X i ∈ A i, 0 ≤ i ≤ n) = ∫_{A 0} μ(dx₀) ∫_{A 1} κ(x₀, dx₁) ⋯ ∫_{A n} κ(x_{n-1}, dx_n).

This is the user-facing wrapper around markov_chain_fdd.