Finite Markov chains

StructureFinite-state Markov chain with a given transition matrix#✓fully proved

IsFiniteMarkovChain X P ℱ μ asserts that the sequence X : ℕ → Ω → Fin (M+1) is a Markov chain with transition matrix P, adapted to the filtration ℱ, under the measure μ. Concretely: each X n is ℱ n-measurable, and the conditional probability that X (n+1) = j given ℱ n equals P.prob (X n) j, matching the Markov property P(X_{n+1} = j | X_n = i, ...) = P_{ij}. Ported verbatim from v1/Atlas/TheoryOfProbability/code/FiniteMarkovChain.lean; v1 writes the filtration as DiscreteFiltration Ω m, which is Filtration ℕ m.

structure IsFiniteMarkovChain {M : ℕ} (X : ℕ → Ω → Fin (M + 1))
    (P : StochasticMatrix M) (ℱ : Filtration ℕ m) (μ : Measure Ω) : Prop where
  adapted : ∀ n, @Measurable _ _ (ℱ n) _ (X n)
  markov_prop : ∀ n : ℕ, ∀ j : Fin (M + 1),
    μ[(fun ω => if X (n + 1) ω = j then (1 : ℝ) else 0) | ℱ n] =ᵐ[μ]
      fun ω => P.prob (X n ω) j

Uses 1 · Used by 8

Statement usesStochastic matrix

Used byAlmost-sure absorption of the Wright–Fisher chain · Fixation probability of a Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Limiting fixation probability of a Wright–Fisher chain · Canonical Markov law satisfies the finite Markov chain specification · Bridge: finite-state Markov chains satisfy the general one-step Markov property · One-step forward equation · Finite Markov chains satisfy the general Markov property

DefinitionTransition kernel of a stochastic matrix#✓fully proved

The transition kernel of a stochastic matrix: finiteChainKernel P x is the probability measure on Fin (M + 1) putting mass P.prob x j on each state j. This is the kernel form of the transition matrix.

noncomputable def finiteChainKernel {M : ℕ} (P : StochasticMatrix M) :
    Kernel (Fin (M + 1)) (Fin (M + 1)) :=
  Kernel.ofFunOfCountable (fun x => ∑ j, ENNReal.ofReal (P.prob x j) • Measure.dirac j)

Uses 1 · Used by 12

Statement usesStochastic matrix

Used byAlmost-sure absorption of the Wright–Fisher chain · Finite Wright–Fisher chain is absorbed almost surely · Loss probability of a Wright–Fisher chain · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain · Limiting fixation probability of a Wright–Fisher chain · Canonical Markov law started from a point starts there almost surely · Canonical Markov law satisfies the finite Markov chain specification · Bridge: finite-state Markov chains satisfy the general one-step Markov property · Transition kernel of a stochastic matrix evaluated on a set · One-step forward equation · Finite Markov chains satisfy the general Markov property

TheoremTransition kernel of a stochastic matrix evaluated on a set#✓fully proved

The kernel of a stochastic matrix evaluated at a finite set is the sum of the transition probabilities into that set.

theorem finiteChainKernel_apply {M : ℕ} (P : StochasticMatrix M) (x : Fin (M + 1))
    (B : Finset (Fin (M + 1))) :
    finiteChainKernel P x ↑B = ∑ j ∈ B, ENNReal.ofReal (P.prob x j)

Uses 2 · Used by 5

Statement usesTransition kernel of a stochastic matrix · Stochastic matrix

Used byAlmost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Limiting fixation probability of a Wright–Fisher chain · Canonical Markov law satisfies the finite Markov chain specification · Bridge: finite-state Markov chains satisfy the general one-step Markov property

TheoremBridge: finite-state Markov chains satisfy the general one-step Markov property#✓fully proved

Bridge: finite-state Markov chains satisfy the general one-step Markov property. For a finite Markov chain, the conditional expectation of the indicator of X (n+1) ∈ B given ℱ n is the kernel of P evaluated at X n, almost surely. This is the one-step form of v1's general IsMarkovChain.markov_prop specialized to the matrix kernel. No measurability hypothesis on B is needed: the indicator is defined for every set, and the proof only sums over the finite state space.

theorem IsFiniteMarkovChain.condExp_indicator {M : ℕ} {X : ℕ → Ω → Fin (M + 1)}
    {P : StochasticMatrix M} {ℱ : Filtration ℕ m} [IsProbabilityMeasure μ]
    (hX : IsFiniteMarkovChain X P ℱ μ) {n : ℕ} {B : Set (Fin (M + 1))} :
    μ[(B.indicator (fun _ => (1 : ℝ))) ∘ (X (n + 1)) | ℱ n] =ᵐ[μ]
      fun ω => (finiteChainKernel P (X n ω) B).toReal

Uses 4 · Used by 1

Statement usesFinite-state Markov chain with a given transition matrix · Transition kernel of a stochastic matrix · Stochastic matrix

Proof usesTransition kernel of a stochastic matrix evaluated on a set

Used byFinite Markov chains satisfy the general Markov property

TheoremFinite Markov chains satisfy the general Markov property#✓fully proved

Convert the finite singleton-probability specification to the canonical general Markov-chain predicate under the probability-space hypotheses of condExp_indicator.

theorem IsFiniteMarkovChain.toIsMarkovChain {M : ℕ} {X : ℕ → Ω → Fin (M + 1)}
    {P : StochasticMatrix M} {ℱ : Filtration ℕ m} [IsProbabilityMeasure μ]
    (hX : IsFiniteMarkovChain X P ℱ μ) :
    MathlibExt.Probability.MarkovChainChapmanKolmogorov.IsMarkovChain
      X ℱ (finiteChainKernel P) μ

Uses 5 · Used by 1

Statement usesFinite-state Markov chain with a given transition matrix · Transition kernel of a stochastic matrix · Markov chain with respect to a filtration · Stochastic matrix

Proof usesBridge: finite-state Markov chains satisfy the general one-step Markov property

Used byOne-step forward equation

TheoremOne-step forward equation#✓fully proved

The law of X (n+1) is the law of X n transported by the transition kernel of P.

theorem IsFiniteMarkovChain.map_succ_eq_bind {M : ℕ} {X : ℕ → Ω → Fin (M + 1)}
    {P : StochasticMatrix M} {ℱ : Filtration ℕ m} [IsProbabilityMeasure μ]
    (hX : IsFiniteMarkovChain X P ℱ μ) (n : ℕ) :
    μ.map (X (n + 1)) = (μ.map (X n)).bind (finiteChainKernel P)

Uses 5 · Used by 3

Statement usesFinite-state Markov chain with a given transition matrix · Transition kernel of a stochastic matrix · Stochastic matrix

Proof usesFinite Markov chains satisfy the general Markov property · Chapman–Kolmogorov equations, forward (law) form

Used byAlmost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Limiting fixation probability of a Wright–Fisher chain

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.