Construction of Markov chains

DefinitionLifting a kernel to histories#✓fully proved

For a kernel \(\kappa\) from a measurable space \(S\) to itself and \(n \in \mathbb{N}\), the lifted kernel from \(S^{\{0, \dots, n\}}\) to \(S\) sends a history \((x_0, \dots, x_n)\) to \(\kappa(x_n, \cdot)\): it reads off the last coordinate and applies \(\kappa\).

This is the form of kernel used by the Ionescu–Tulcea trajectory construction.

noncomputable def markovLiftKernel (κ : Kernel S S) (n : ℕ) :
    Kernel ((i : ↥(Finset.Iic n)) → S) S :=
  κ.comap (fun x => x ⟨n, Finset.mem_Iic.mpr le_rfl⟩) (measurable_pi_apply _)

Used by 17

Used byFinite Wright–Fisher chain is absorbed almost surely · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain · Integral of a shifted path functional · Canonical Markov law satisfies the finite Markov chain specification · Markov chain construction theorem · Canonical Markov chain measure · Markov property of the canonical Markov chain measure · Initial distribution of the canonical Markov chain measure · Path measure from a point as a trajectory measure · Lifted transition kernel on histories · Measurability of the Markov expectation · One-step shift of a Markov partial trajectory · The shifted trajectory of a Markov chain restarts from its last state · Markov property · Markov property, set-integral form · Strong Markov property for a.s.-finite stopping times

DefinitionCanonical Markov chain measure#✓fully proved

Let \(\kappa\) be a Markov kernel from a measurable space \(S\) to itself and let \(\mu\) be a measure on \(S\). The canonical Markov chain measure \(P_\mu\) is the measure on the path space \(S^{\mathbb{N}}\) given by the Ionescu–Tulcea theorem for the initial measure \(\mu\) and, at each time \(n\), the kernel sending a history \((x_0, \dots, x_n)\) to \(\kappa(x_n, \cdot)\). When \(\mu\) is a probability measure, \(P_\mu\) is the law of the Markov chain with initial distribution \(\mu\) and transition kernel \(\kappa\).

noncomputable def markovChainMeasure : Measure (ℕ → S) :=
  Kernel.trajMeasure (X := fun _ : ℕ => S) μ (markovLiftKernel κ)

Uses 1 · Used by 14

Statement usesLifting a kernel to histories

Used byFinite Wright–Fisher chain is absorbed almost surely · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain · Canonical Markov law started from a point starts there almost surely · Canonical Markov law satisfies the finite Markov chain specification · Markov chain construction theorem · Markov property of the canonical Markov chain measure · Initial distribution of the canonical Markov chain measure · Markov chain path measure · Path measure from a point as a trajectory measure · Measurability of the Markov expectation · Markov property · Markov property, set-integral form · Strong Markov property for a.s.-finite stopping times

TheoremInitial distribution of the canonical Markov chain measure#✓fully proved

Let \(\kappa\) be a Markov kernel from a measurable space \(S\) to itself and let \(\mu\) be a measure on \(S\). Under the canonical Markov chain measure \(P_\mu\) on \(S^{\mathbb{N}}\) with initial measure \(\mu\) and transition kernel \(\kappa\), the law of the initial coordinate is \(\mu\): the pushforward of \(P_\mu\) along \(\omega \mapsto \omega_0\) equals \(\mu\).

theorem markovChainMeasure_initial_distribution :
    Measure.map (fun (ω : ℕ → S) => ω 0) (markovChainMeasure κ μ) = μ

Uses 2 · Used by 2

Statement usesCanonical Markov chain measure

Proof usesLifting a kernel to histories

Used byCanonical Markov law started from a point starts there almost surely · Markov chain construction theorem

TheoremMarkov property of the canonical Markov chain measure#✓fully proved

Let \(S\) be a nonempty standard Borel space, let \(\kappa\) be a Markov kernel from \(S\) to \(S\), let \(\mu\) be a probability measure on \(S\), and let \(P_\mu\) be the canonical Markov chain measure on \(S^{\mathbb{N}}\) with initial distribution \(\mu\) and transition kernel \(\kappa\). Write \(X_n(\omega) = \omega_n\). For every \(n \in \mathbb{N}\), the regular conditional distribution of \(X_{n+1}\) given \((X_0, \dots, X_n)\) under \(P_\mu\) agrees with the lifted kernel \((x_0, \dots, x_n) \mapsto \kappa(x_n, \cdot)\) for almost every \((x_0, \dots, x_n)\) with respect to the law of \((X_0, \dots, X_n)\) under \(P_\mu\).

theorem markovChainMeasure_condDistrib (n : ℕ)
    [StandardBorelSpace S] [Nonempty S] :
    condDistrib (fun (x : ℕ → S) => x (n + 1)) (Preorder.frestrictLe n)
      (markovChainMeasure κ μ)
      =ᵐ[Measure.map (Preorder.frestrictLe n) (markovChainMeasure κ μ)]
        markovLiftKernel κ n

Uses 2 · Used by 2

Statement usesCanonical Markov chain measure · Lifting a kernel to histories

Used byCanonical Markov law satisfies the finite Markov chain specification · Markov chain construction theorem

TheoremMarkov chain construction theorem#✓fully proved

Let \(S\) be a nonempty standard Borel space, let \(\kappa\) be a Markov kernel from \(S\) to \(S\) and let \(\mu\) be a probability measure on \(S\). Then there is a probability measure \(P\) on the path space \(S^{\mathbb{N}}\) such that, writing \(X_n(\omega) = \omega_n\) for the coordinates, the law of \(X_0\) under \(P\) is \(\mu\), and for every \(n \in \mathbb{N}\) the regular conditional distribution of \(X_{n+1}\) given \((X_0, \dots, X_n)\) under \(P\) agrees with the kernel \((x_0, \dots, x_n) \mapsto \kappa(x_n, \cdot)\) for almost every \((x_0, \dots, x_n)\) with respect to the law of \((X_0, \dots, X_n)\) under \(P\).

That is, the coordinate process \((X_0, X_1, \dots)\) under \(P\) is a Markov chain with initial distribution \(\mu\) and transition kernel \(\kappa\).

theorem markov_chain_construction
    (κ : Kernel S S) [IsMarkovKernel κ]
    (μ : Measure S) [IsProbabilityMeasure μ]
    [StandardBorelSpace S] [Nonempty S] :
    ∃ (P : Measure (ℕ → S)) (_ : IsProbabilityMeasure P),
      P.map (fun (ω : ℕ → S) => ω 0) = μ ∧
      ∀ n : ℕ,
        condDistrib (fun (x : ℕ → S) => x (n + 1)) (Preorder.frestrictLe n) P
          =ᵐ[Measure.map (Preorder.frestrictLe n) P] markovLiftKernel κ n

Uses 4

Statement usesLifting a kernel to histories

Proof usesCanonical Markov chain measure · Markov property of the canonical Markov chain measure · Initial distribution of the canonical Markov chain measure

TheoremCanonical Markov law started from a point starts there almost surely#✓fully proved

The canonical Markov law with initial distribution dirac i starts at i almost surely. Its initial marginal is supplied by the existing construction.

theorem ae_eval_zero_markovChainMeasure {M : ℕ} (P : StochasticMatrix M)
    (i : Fin (M + 1)) :
    ∀ᵐ ω ∂markovChainMeasure (finiteChainKernel P) (Measure.dirac i), ω 0 = i

Uses 4 · Used by 3

Statement usesTransition kernel of a stochastic matrix · Canonical Markov chain measure · Stochastic matrix

Proof usesInitial distribution of the canonical Markov chain measure

Used byFinite Wright–Fisher chain is absorbed almost surely · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain

TheoremCanonical Markov law satisfies the finite Markov chain specification#✓fully proved

The coordinate process under the existing canonical matrix-derived Markov law satisfies the original finite-state Markov-chain specification on Filtration.piLE.

theorem isFiniteMarkovChain_markovChainMeasure {M : ℕ} (P : StochasticMatrix M)
    (i : Fin (M + 1)) :
    IsFiniteMarkovChain (fun n (ω : ℕ → Fin (M + 1)) ↦ ω n) P Filtration.piLE
      (markovChainMeasure (finiteChainKernel P) (Measure.dirac i))

Uses 7 · Used by 3

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

Proof usesTransition kernel of a stochastic matrix evaluated on a set · Markov property of the canonical Markov chain measure · Lifting a kernel to histories

Used byFinite Wright–Fisher chain is absorbed almost surely · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain

AbbreviationLifted transition kernel on histories#✓fully proved

For a kernel \(\kappa\) on \(S\) and \(n \in \mathbb{N}\), this is the kernel from histories \((x_0, \dots, x_n)\) of states in \(S\), indexed by \(\{0, \dots, n\}\), to \(S\) that sends \((x_0, \dots, x_n)\) to \(\kappa(x_n, \cdot)\). It is the Markov lift kernel of \(\kappa\) at \(n\).

noncomputable abbrev markovLiftKernel (κ : Kernel S S) (n : ℕ) :
    Kernel ((_i : ↥(Finset.Iic n)) → S) S :=
  MathlibExt.Probability.MarkovChainConstruction.markovLiftKernel κ n

Uses 1 · Used by 8

Statement usesLifting a kernel to histories

Used byIntegral of a shifted path functional · Path measure from a point as a trajectory measure · Measurability of the Markov expectation · Shifted finite-dimensional distributions · One-step shift of a Markov partial trajectory · One-step shift of the partial trajectory kernel · The shifted trajectory of a Markov chain restarts from its last state · Markov property, set-integral form

TheoremOne-step shift of a Markov partial trajectory#✓fully proved

Let \(\kappa\) be a Markov kernel on a measurable space \(S\), let \(a, b \in \mathbb{N}\) and let \(z = (z_0, \dots, z_{a+b})\) be a history in \(S^{\{0, \dots, a+b\}}\). Let \(\mu_z\) be the one-step partial trajectory of the lifted kernel of \(\kappa\) from time \(a + b\) to time \(a + b + 1\) started at \(z\), that is, the law of \((z_0, \dots, z_{a+b}, X)\) where \(X\) has law \(\kappa(z_{a+b})\). Then the image of \(\mu_z\) under the map \((y_0, \dots, y_{a+b+1}) \mapsto (y_a, \dots, y_{a+b+1})\) that drops the first \(a\) coordinates equals the one-step partial trajectory of the lifted kernel from time \(b\) to time \(b + 1\) started at \((z_a, \dots, z_{a+b})\), that is, the law of \((z_a, \dots, z_{a+b}, X')\) where \(X'\) has law \(\kappa(z_{a+b})\).

theorem partialTraj_succ_map_drop {a b : ℕ} (z : Π _i : ↥(Finset.Iic (a + b)), S) :
    ((partialTraj (X := fun _ : ℕ => S) (markovLiftKernel κ) (a + b) (a + b + 1)) z).map (dropHist a (b + 1))
    = partialTraj (X := fun _ : ℕ => S) (markovLiftKernel κ) b (b + 1) (dropHist a b z)

Uses 2 · Used by 1

Statement usesLifted transition kernel on histories

Proof usesLifting a kernel to histories

Used byOne-step shift of the partial trajectory kernel

DefinitionLast-coordinate history#✓fully proved

For \(a \in \mathbb{N}\) and a history \(x = (x_0, \dots, x_a)\) of states in \(S\), indexed by \(\{0, \dots, a\}\), the last-coordinate history of \(x\) is the history indexed by \(\{0\}\) whose only entry is \(x_a\).

def lastHist (a : ℕ) (x₀ : Π _i : ↥(Finset.Iic a), S) : Π _i : ↥(Finset.Iic 0), S :=
  fun _i => x₀ ⟨a, Finset.mem_Iic.mpr le_rfl⟩

Used by 4

Used byIntegral of a shifted path functional · Path measure from a point as a trajectory measure · Shifted finite-dimensional distributions · The shifted trajectory of a Markov chain restarts from its last state

TheoremOne-step shift of the partial trajectory kernel#✓fully proved

Let \(\kappa\) be a Markov kernel on \(S\) and \(a, b \in \mathbb{N}\). For a history \(z = (z_0, \dots, z_{a+b})\) of states in \(S\), extend \(z\) by one step, drawing \(z_{a+b+1}\) from \(\kappa(z_{a+b}, \cdot)\), and then keep the entries at times \(a, \dots, a + b + 1\), reindexed as \(0, \dots, b + 1\). The law of the result equals the law obtained by first keeping the entries of \(z\) at times \(a, \dots, a + b\), reindexed as \(0, \dots, b\), and then extending that history by one step in the same way. This holds as an identity of kernels in \(z\).

theorem partialTraj_succ_map_drop_kernel {a b : ℕ} :
    (partialTraj (X := fun _ : ℕ => S) (markovLiftKernel κ) (a + b) (a + b + 1)).map (dropHist a (b + 1))
      = partialTraj (X := fun _ : ℕ => S) (markovLiftKernel κ) b (b + 1) ∘ₖ
          Kernel.deterministic (dropHist (S := S) a b) (measurable_dropHist a b)

Uses 2 · Used by 1

Statement usesLifted transition kernel on histories

Proof usesOne-step shift of a Markov partial trajectory

Used byShifted finite-dimensional distributions

TheoremShifted finite-dimensional distributions#✓fully proved

Let \(\kappa\) be a Markov kernel on \(S\) and \(a, b \in \mathbb{N}\). For a history \(x = (x_0, \dots, x_a)\) of states in \(S\), let \(Q_x\) be the law of the history \((X_0, \dots, X_{a+b})\) that equals \(x\) at times \(0, \dots, a\) and then draws each next state from \(\kappa\) applied to the current state (the Ionescu–Tulcea partial trajectory from time \(a\) to time \(a + b\)). Then the image of \(Q_x\) under \((X_0, \dots, X_{a+b}) \mapsto (X_a, \dots, X_{a+b})\), with the times reindexed as \(0, \dots, b\), equals the law of \((X_0, \dots, X_b)\) under the partial trajectory from time \(0\) to time \(b\) started from the one-entry history \((x_a)\). This holds as an identity of kernels in \(x\).

theorem partialTraj_map_drop {a b : ℕ} :
    (partialTraj (X := fun _ : ℕ => S) (markovLiftKernel κ) a (a + b)).map (dropHist a b)
      = partialTraj (X := fun _ : ℕ => S) (markovLiftKernel κ) 0 b ∘ₖ
          Kernel.deterministic (lastHist (S := S) a) (measurable_lastHist a)

Uses 3 · Used by 1

Statement usesLast-coordinate history · Lifted transition kernel on histories

Proof usesOne-step shift of the partial trajectory kernel

Used byThe shifted trajectory of a Markov chain restarts from its last state

DefinitionTime shift on path space#✓fully proved

Let \(S\) be a set and \(n \in \mathbb{N}\). The time-\(n\) shift on the path space \(S^{\mathbb{N}}\) sends a path \(\omega\) to the path \(k \mapsto \omega_{n+k}\).

def shiftPath (n : ℕ) : (ℕ → S) → (ℕ → S) :=
  fun ω k => ω (n + k)

Used by 8

Used byFinite restrictions of the shifted path · Integral of a shifted path functional · The shifted trajectory of a Markov chain restarts from its last state · Markov property · Markov property, set-integral form · The shift by a random time agrees with the fixed shift on its level set · Strong Markov property for everywhere-finite stopping times · Strong Markov property for a.s.-finite stopping times

LemmaFinite restrictions of the shifted path#✓fully proved

For all \(n, b \in \mathbb{N}\) and every path \(\omega : \mathbb{N} \to S\), let \(\theta_n \omega\) be the shifted path, \((\theta_n \omega)_k = \omega_{n+k}\). The restriction of \(\theta_n \omega\) to the times \(0, \dots, b\) equals the restriction of \(\omega\) to the times \(0, \dots, n + b\) with its entries at times \(n, \dots, n + b\) kept and reindexed as \(0, \dots, b\); that is, it is the tuple \((\omega_n, \omega_{n+1}, \dots, \omega_{n+b})\).

lemma frestrictLe_comp_shiftPath (n b : ℕ) :
    (Preorder.frestrictLe (π := fun _ : ℕ => S) b) ∘ (shiftPath (S := S) n)
      = (dropHist n b) ∘ (Preorder.frestrictLe (π := fun _ : ℕ => S) (n + b))

Uses 1 · Used by 1

Statement usesTime shift on path space

Used byThe shifted trajectory of a Markov chain restarts from its last state

TheoremThe shifted trajectory of a Markov chain restarts from its last state#✓fully proved

Let \(\kappa\) be a Markov kernel on a measurable space \(S\), let \(n \in \mathbb{N}\) and let \(x = (x_0, \dots, x_n) \in S^{\{0, \dots, n\}}\). Let \(P_x\) be the trajectory measure on \(S^{\mathbb{N}}\) of the lifted kernel of \(\kappa\) started at time \(n\) from the history \(x\), and let \(P_{x_n}\) be the trajectory measure of the lifted kernel started at time \(0\) from the one-point history \(x_n\). Then the image of \(P_x\) under the time-\(n\) shift \(\omega \mapsto (k \mapsto \omega_{n+k})\) equals \(P_{x_n}\).

theorem traj_map_shiftPath_eq {n : ℕ} (x₀ : Π _i : ↥(Finset.Iic n), S) :
    (Kernel.traj (X := fun _ : ℕ => S) (markovLiftKernel κ) n x₀).map (shiftPath n)
      = Kernel.traj (X := fun _ : ℕ => S) (markovLiftKernel κ) 0 (lastHist n x₀)

Uses 6 · Used by 1

Statement usesLifting a kernel to histories · Last-coordinate history · Lifted transition kernel on histories · Time shift on path space

Proof usesFinite restrictions of the shifted path · Shifted finite-dimensional distributions

Used byIntegral of a shifted path functional

DefinitionPath filtration#✓fully proved

Let \(S\) be a measurable space. The path filtration on the path space \(S^{\mathbb{N}}\) is the filtration indexed by \(\mathbb{N}\), relative to the product σ-algebra, whose σ-algebra at time \(n\) is the one generated by the coordinate maps \(\omega \mapsto \omega_i\) for \(i \le n\).

noncomputable def pathFiltration (S : Type*) [MeasurableSpace S] :
    Filtration ℕ
      (m := MeasurableSpace.pi (m := fun _ : ℕ => (inferInstance : MeasurableSpace S))) where
  seq n := ⨆ (i : ℕ) (_ : i ≤ n),
    MeasurableSpace.comap (fun (ω : ℕ → S) => ω i) ‹MeasurableSpace S›
  mono' i j hij := iSup_mono fun k => iSup_mono' fun hk => ⟨hk.trans hij, le_rfl⟩
  le' n := iSup_le fun k => iSup_le fun _ => (measurable_pi_apply k).comap_le

Used by 5

Used byThe path filtration is contained in the product σ-algebra · Markov property · Markov property, set-integral form · Strong Markov property for everywhere-finite stopping times · Strong Markov property for a.s.-finite stopping times

LemmaThe path filtration is contained in the product σ-algebra#✓fully proved

Let \(S\) be a measurable space. For every \(n \in \mathbb{N}\), the \(n\)-th σ-algebra of the path filtration on \(S^{\mathbb{N}}\), generated by the coordinate maps \(\omega \mapsto \omega_i\) for \(i \le n\), is contained in the product σ-algebra on \(S^{\mathbb{N}}\).

lemma pathFiltration_le_pi (S : Type*) [MeasurableSpace S] (n : ℕ) :
    pathFiltration S n ≤ MeasurableSpace.pi

Uses 1 · Used by 1

Statement usesPath filtration

Used byMarkov property, set-integral form

AbbreviationMarkov chain path measure#✓fully proved

For a measure \(\mu\) on \(S\) and a Markov kernel \(\kappa\) on \(S\), the path measure \(P_\mu\) is the measure on \(S^{\mathbb{N}}\), with the product \(\sigma\)-algebra, obtained by integrating against \(\mu(dx)\) the Ionescu–Tulcea trajectory measure that starts at \(x\) at time \(0\) and draws each next state from \(\kappa\) applied to the current state. It is the Markov chain measure of \(\kappa\) and \(\mu\); when \(\mu\) is a probability measure it is the law on path space of the Markov chain with initial distribution \(\mu\) and transition kernel \(\kappa\).

noncomputable abbrev MarkovChainPathMeasure
    (S : Type*) [MeasurableSpace S]
    (μ : Measure S) (κ : Kernel S S) [IsMarkovKernel κ] :
    @Measure (ℕ → S) MeasurableSpace.pi :=
  MathlibExt.Probability.MarkovChainConstruction.markovChainMeasure κ μ

Uses 1 · Used by 8

Statement usesCanonical Markov chain measure

Used byIntegral of a shifted path functional · Path measure from a point as a trajectory measure · Expectation under the chain started from a point · Measurability of the Markov expectation · Markov property · Markov property, set-integral form · Strong Markov property for everywhere-finite stopping times · Strong Markov property for a.s.-finite stopping times

DefinitionExpectation under the chain started from a point#✓fully proved

For a Markov kernel \(\kappa\) on \(S\), a function \(Y : S^{\mathbb{N}} \to \mathbb{R}\) of paths and a state \(x \in S\), the expectation \(E_x Y\) is the integral of \(Y\) against the Markov chain path measure with transition kernel \(\kappa\) and initial distribution the Dirac measure at \(x\).

noncomputable def markovExpectation
    (S : Type*) [MeasurableSpace S]
    (κ : Kernel S S) [IsMarkovKernel κ] (Y : (ℕ → S) → ℝ) (x : S) : ℝ :=
  ∫ ω, Y ω ∂(MarkovChainPathMeasure S (Measure.dirac x) κ)

Uses 1 · Used by 5

Statement usesMarkov chain path measure

Used byMeasurability of the Markov expectation · Markov property · Markov property, set-integral form · Strong Markov property for everywhere-finite stopping times · Strong Markov property for a.s.-finite stopping times

TheoremMeasurability of the Markov expectation#✓fully proved

Let \(S\) be a nonempty standard Borel space, \(\kappa\) a Markov kernel on \(S\), and \(Y : S^{\mathbb{N}} \to \mathbb{R}\) a bounded function, measurable for the product \(\sigma\)-algebra. Then the map \(x \mapsto E_x Y\), sending a state \(x\) to the expectation of \(Y\) under the Markov chain with transition kernel \(\kappa\) started from \(x\), is measurable.

theorem measurable_markovExpectation
    (S : Type*) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S]
    (κ : Kernel S S) [IsMarkovKernel κ]
    (Y : (ℕ → S) → ℝ) (hY_meas : @Measurable _ _ MeasurableSpace.pi _ Y)
    (_hY_bdd : ∃ C : ℝ, ∀ ω, |Y ω| ≤ C) :
    Measurable (markovExpectation S κ Y)

Uses 5 · Used by 2

Statement usesExpectation under the chain started from a point

Proof usesCanonical Markov chain measure · Lifting a kernel to histories · Markov chain path measure · Lifted transition kernel on histories

Used byMarkov property · Markov property, set-integral form

TheoremPath measure from a point as a trajectory measure#✓fully proved

Let \(\kappa\) be a Markov kernel on \(S\), \(n \in \mathbb{N}\), and \(x = (x_0, \dots, x_n)\) a history of states in \(S\). The law on path space of the Markov chain with transition kernel \(\kappa\) and initial distribution the Dirac measure at \(x_n\) equals the Ionescu–Tulcea trajectory measure on \(S^{\mathbb{N}}\) started at time \(0\) from the one-entry history \((x_n)\) (the last-coordinate history of \(x\)), in which each next state is drawn from \(\kappa\) applied to the current state.

theorem MarkovChainPathMeasure_dirac_eq_traj {n : ℕ} (x₀ : Π _i : ↥(Finset.Iic n), S) :
    MarkovChainPathMeasure S (Measure.dirac (x₀ ⟨n, Finset.mem_Iic.mpr le_rfl⟩)) κ
      = Kernel.traj (X := fun _ : ℕ => S) (markovLiftKernel κ) 0 (lastHist n x₀)

Uses 5 · Used by 1

Statement usesLifting a kernel to histories · Markov chain path measure · Last-coordinate history · Lifted transition kernel on histories

Proof usesCanonical Markov chain measure

Used byIntegral of a shifted path functional

TheoremIntegral of a shifted path functional#✓fully proved

Let \(S\) be a nonempty standard Borel space, \(\kappa\) a Markov kernel on \(S\), and \(Y : S^{\mathbb{N}} \to \mathbb{R}\) a bounded function, measurable for the product \(\sigma\)-algebra. Fix \(n \in \mathbb{N}\) and a history \(x = (x_0, \dots, x_n)\) of states in \(S\), and let \(P_{n,x}\) be the Ionescu–Tulcea trajectory measure on \(S^{\mathbb{N}}\) that equals \(x\) at times \(0, \dots, n\) and afterwards draws each next state from \(\kappa\) applied to the current state. Then

\[\int Y(\theta_n \omega) \, dP_{n,x}(\omega) = \int Y \, dP_{\delta_{x_n}},\]

where \((\theta_n \omega)_k = \omega_{n+k}\) is the time-\(n\) shift and \(P_{\delta_{x_n}}\) is the law on path space of the Markov chain with transition kernel \(\kappa\) and initial distribution the Dirac measure at \(x_n\).

The statement also takes a finite measure \(\mu\) on \(S\), which does not appear in it.

theorem integral_shiftPath_traj_eq_markovExpectation
    (S : Type*) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S]
    (μ : Measure S) [IsFiniteMeasure μ]
    (κ : Kernel S S) [IsMarkovKernel κ]
    (Y : (ℕ → S) → ℝ) (hY_meas : @Measurable _ _ MeasurableSpace.pi _ Y)
    (_hY_bdd : ∃ C : ℝ, ∀ ω, |Y ω| ≤ C)
    (n : ℕ) (x₀ : (_i : ↥(Finset.Iic n)) → S) :
    ∫ ω, Y (shiftPath n ω) ∂(Kernel.traj (X := fun _ : ℕ => S) (markovLiftKernel κ) n x₀) =
      ∫ ω, Y ω ∂(MarkovChainPathMeasure S (Measure.dirac (x₀ ⟨n, Finset.mem_Iic.mpr le_rfl⟩)) κ)

Uses 7 · Used by 1

Statement usesLifting a kernel to histories · Markov chain path measure · Lifted transition kernel on histories · Time shift on path space

Proof usesPath measure from a point as a trajectory measure · Last-coordinate history · The shifted trajectory of a Markov chain restarts from its last state

Used byMarkov property, set-integral form

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.