Markov and strong Markov properties

TheoremMarkov property, set-integral form#✓fully proved

Let \(S\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(S\), \(\kappa\) a Markov kernel on \(S\), and \(P_\mu\) the path measure on \(S^{\mathbb{N}}\) of the Markov chain with initial measure \(\mu\) and transition kernel \(\kappa\). Let \(Y : S^{\mathbb{N}} \to \mathbb{R}\) be bounded and measurable for the product \(\sigma\)-algebra, let \(n \in \mathbb{N}\), let \(\theta_n\) be the shift \((\theta_n \omega)_k = \omega_{n+k}\), and let \(\mathcal{F}_n\) be the \(\sigma\)-algebra generated by the coordinates \(\omega_0, \dots, \omega_n\). For \(x \in S\), let \(E_x[Y]\) be the integral of \(Y\) against the path measure of the chain started at \(x\). Then for every set \(A \in \mathcal{F}_n\),

\[\int_A Y(\theta_n \omega) \, dP_\mu(\omega) = \int_A E_{\omega_n}[Y] \, dP_\mu(\omega).\]

theorem markov_setIntegral_shift
    (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 : ℕ) (A : Set (ℕ → S))
    (hA : @MeasurableSet _ (pathFiltration S n) A) :
    let P_μ := MarkovChainPathMeasure S μ κ
    ∫ ω in A, (Y ∘ shiftPath n) ω ∂P_μ = ∫ ω in A, markovExpectation S κ Y (ω n) ∂P_μ

Uses 10 · Used by 1

Statement usesMarkov chain path measure · Expectation under the chain started from a point · Path filtration · Time shift on path space

Proof usesCanonical Markov chain measure · Lifting a kernel to histories · Integral of a shifted path functional · Lifted transition kernel on histories · Measurability of the Markov expectation · The path filtration is contained in the product σ-algebra

Used byMarkov property

TheoremMarkov property#✓fully proved

Let \(S\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(S\), \(\kappa\) a Markov kernel on \(S\), and \(P_\mu\) the path measure on \(S^{\mathbb{N}}\) of the Markov chain with initial measure \(\mu\) and transition kernel \(\kappa\). Let \(Y : S^{\mathbb{N}} \to \mathbb{R}\) be bounded and measurable for the product \(\sigma\)-algebra, let \(n \in \mathbb{N}\), let \(\theta_n\) be the shift \((\theta_n \omega)_k = \omega_{n+k}\), and let \(\mathcal{F}_n\) be the \(\sigma\)-algebra generated by the coordinates \(\omega_0, \dots, \omega_n\). For \(x \in S\), let \(E_x[Y]\) be the integral of \(Y\) against the path measure of the chain started at \(x\). Then for \(P_\mu\)-almost every \(\omega\),

\[E_{P_\mu}[Y \circ \theta_n \mid \mathcal{F}_n](\omega) = E_{\omega_n}[Y].\]

In other words, conditioning on the trajectory up to time \(n\) depends only on the state at time \(n\).

theorem markov_property_full
    (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 : ℕ) :
    let P_μ := MarkovChainPathMeasure S μ κ
    P_μ[Y ∘ shiftPath n | pathFiltration S n]
    =ᵐ[P_μ]
      fun ω => markovExpectation S κ Y (ω n)

Uses 8 · Used by 1

Statement usesMarkov chain path measure · Expectation under the chain started from a point · Path filtration · Time shift on path space

Proof usesCanonical Markov chain measure · Lifting a kernel to histories · Measurability of the Markov expectation · Markov property, set-integral form

Used byStrong Markov property for a.s.-finite stopping times

DefinitionPath shifted by a random time#✓fully proved

For a type \(S\) and a function \(T : (\mathbb{N} \to S) \to \mathbb{N}\) (typically a stopping time), the shift by \(T\) sends a path \(\omega : \mathbb{N} \to S\) to the path \(k \mapsto \omega(T(\omega) + k)\).

def stoppedPathShift {S : Type*} (T : (ℕ → S) → ℕ) : (ℕ → S) → (ℕ → S) :=
  fun ω k => ω (T ω + k)

Used by 2

Used byThe shift by a random time agrees with the fixed shift on its level set · Strong Markov property for everywhere-finite stopping times

TheoremThe shift by a random time agrees with the fixed shift on its level set#✓fully proved

Let \(S\) be a type, let \(T : (\mathbb{N} \to S) \to \mathbb{N}\) and \(n \in \mathbb{N}\), and let \(\omega : \mathbb{N} \to S\) be a path with \(T(\omega) = n\). Then the path \(\omega\) shifted by \(T\), namely \(k \mapsto \omega(T(\omega) + k)\), equals the path \(\omega\) shifted by \(n\), namely \(k \mapsto \omega(n + k)\).

theorem stoppedPathShift_eq_shiftPath_on_eq {S : Type*}
    (T : (ℕ → S) → ℕ) (n : ℕ) (ω : ℕ → S) (h : T ω = n) :
    stoppedPathShift T ω = shiftPath n ω

Uses 2

Statement usesTime shift on path space · Path shifted by a random time

LemmaA.e. equality from a.e. equality on the fibers of a natural-valued function#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), let \(T : \Omega \to \mathbb{N}\) be a function whose fibers \(\{T = n\}\), \(n \in \mathbb{N}\), are all measurable, and let \(f, g : \Omega \to \mathbb{R}\). If for every \(n \in \mathbb{N}\) we have \(f = g\) almost everywhere with respect to the restriction of \(\mu\) to \(\{T = n\}\), then \(f = g\) \(\mu\)-almost everywhere.

lemma ae_eq_of_ae_eq_restrict_fibers {Ω : Type*} {m0 : MeasurableSpace Ω}
    (T : Ω → ℕ) (μ : @Measure Ω m0)
    (f g : Ω → ℝ)
    (hT_meas : ∀ n, MeasurableSet {ω : Ω | T ω = n})
    (h : ∀ n, f =ᵐ[μ.restrict {ω | T ω = n}] g) :
    f =ᵐ[μ] g

LemmaA.e. equality from a.e. equality on the finite fibers#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\), let \(\tau : \Omega \to \mathbb{N} \cup \{\infty\}\) satisfy \(\tau \ne \infty\) \(\mu\)-almost everywhere and have every fiber \(\{\tau = n\}\), \(n \in \mathbb{N}\), measurable, and let \(f, g : \Omega \to \mathbb{R}\). If for every \(n \in \mathbb{N}\) we have \(f = g\) almost everywhere with respect to the restriction of \(\mu\) to \(\{\tau = n\}\), then \(f = g\) \(\mu\)-almost everywhere.

lemma ae_eq_of_ae_eq_restrict_finite_fibers {Ω : Type*} [MeasurableSpace Ω]
    (τ : Ω → WithTop ℕ) (μ : Measure Ω) (f g : Ω → ℝ)
    (hfinite : ∀ᵐ ω ∂μ, τ ω ≠ ⊤)
    (hmeas : ∀ n : ℕ, MeasurableSet {ω | τ ω = (n : WithTop ℕ)})
    (h : ∀ n : ℕ, f =ᵐ[μ.restrict {ω | τ ω = (n : WithTop ℕ)}] g) : f =ᵐ[μ] g

Used by 1

Used byStrong Markov property for a.s.-finite stopping times

TheoremStrong Markov property for a.s.-finite stopping times#✓fully proved

Let \(S\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(S\), \(\kappa\) a Markov kernel on \(S\), and \(P_\mu\) the law on the path space \(S^{\mathbb{N}}\) of the Markov chain with initial distribution \(\mu\) and transition kernel \(\kappa\). For \(x \in S\) write \(E_x\) for the expectation under the chain started from \(x\), and for a path \(\omega\) and \(n \in \mathbb{N}\) write \(\theta_n \omega\) for the shifted path \(k \mapsto \omega(n + k)\). Let \(T : S^{\mathbb{N}} \to \mathbb{N} \cup \{\infty\}\) be a stopping time for the path filtration, with \(\sigma\)-algebra \(\mathcal{F}_T\), such that \(T \ne \infty\) \(P_\mu\)-almost surely, and let \(Y_n : S^{\mathbb{N}} \to \mathbb{R}\), for \(n \in \mathbb{N}\), be measurable functions with \(|Y_n(\omega)| \le C\) for a single constant \(C\) and all \(n\) and \(\omega\). Then the conditional expectation under \(P_\mu\) given \(\mathcal{F}_T\) of \(\omega \mapsto Y_{T(\omega)}(\theta_{T(\omega)} \omega)\) equals \(\omega \mapsto E_{\omega(T(\omega))}[Y_{T(\omega)}]\) \(P_\mu\)-almost surely.

On the null event \(\{T = \infty\}\) both sides are evaluated at the same unspecified finite time, which does not affect the almost-sure equality.

theorem strong_markov_chain_ae_finite
    (S : Type*) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S]
    (μ : Measure S) [IsFiniteMeasure μ]
    (κ : Kernel S S) [IsMarkovKernel κ]
    (T : (ℕ → S) → WithTop ℕ)
    (hT : @IsStoppingTime (ℕ → S) ℕ MeasurableSpace.pi _ (pathFiltration S) T)
    (hT_finite : ∀ᵐ ω ∂MarkovChainPathMeasure S μ κ, T ω ≠ ⊤)
    (Y : ℕ → (ℕ → S) → ℝ)
    (hY_meas : ∀ n, @Measurable _ _ MeasurableSpace.pi _ (Y n))
    (hY_bdd : ∃ C : ℝ, ∀ n ω, |Y n ω| ≤ C) :
    let P_μ := MarkovChainPathMeasure S μ κ
    P_μ[stoppedValue (fun n ω => Y n (shiftPath n ω)) T | hT.measurableSpace]
      =ᵐ[P_μ] stoppedValue (fun n ω => markovExpectation S κ (Y n) (ω n)) T

Sources

• Theory of Probability, Lecture 31 (strong Markov property).

Uses 8 · Used by 1

Statement usesMarkov chain path measure · Expectation under the chain started from a point · Path filtration · Time shift on path space

Proof usesCanonical Markov chain measure · Lifting a kernel to histories · Markov property · A.e. equality from a.e. equality on the finite fibers

Used byStrong Markov property for everywhere-finite stopping times

TheoremStrong Markov property for everywhere-finite stopping times#✓fully proved

Let \(S\) be a nonempty standard Borel space, \(\mu\) a finite measure on \(S\), \(\kappa\) a Markov kernel on \(S\), and \(P_\mu\) the law on the path space \(S^{\mathbb{N}}\) of the Markov chain with initial distribution \(\mu\) and transition kernel \(\kappa\); for \(x \in S\) write \(E_x\) for the expectation under the chain started from \(x\). Let \(T : S^{\mathbb{N}} \to \mathbb{N}\) be a stopping time for the path filtration, with \(\sigma\)-algebra \(\mathcal{F}_T\), and let \(Y_n : S^{\mathbb{N}} \to \mathbb{R}\), for \(n \in \mathbb{N}\), be measurable functions with \(|Y_n(\omega)| \le C\) for a single constant \(C\) and all \(n\) and \(\omega\). Write \(\theta_T \omega\) for the path \(\omega\) shifted by \(T\), namely \(k \mapsto \omega(T(\omega) + k)\). Then the conditional expectation under \(P_\mu\) given \(\mathcal{F}_T\) of \(\omega \mapsto Y_{T(\omega)}(\theta_T \omega)\) equals \(\omega \mapsto E_{\omega(T(\omega))}[Y_{T(\omega)}]\) \(P_\mu\)-almost surely.

This is the special case of the strong Markov property for a.s.-finite stopping times in which the time is finite everywhere.

theorem strong_markov_chain
    (S : Type*) [MeasurableSpace S] [StandardBorelSpace S] [Nonempty S]
    (μ : Measure S) [IsFiniteMeasure μ]
    (κ : Kernel S S) [IsMarkovKernel κ]
    (T : (ℕ → S) → ℕ)
    (hT : @IsStoppingTime (ℕ → S) ℕ
      MeasurableSpace.pi _ (pathFiltration S) (fun ω => (T ω : WithTop ℕ)))
    (Y : ℕ → (ℕ → S) → ℝ)
    (hY_meas : ∀ n, @Measurable _ _ MeasurableSpace.pi _ (Y n))
    (hY_bdd : ∃ C : ℝ, ∀ n ω, |Y n ω| ≤ C) :
    let P_μ := MarkovChainPathMeasure S μ κ
    P_μ[fun ω => Y (T ω) (stoppedPathShift T ω) | hT.measurableSpace]
    =ᵐ[P_μ]
      fun ω => markovExpectation S κ (Y (T ω)) (ω (T ω))

Uses 6

Statement usesMarkov chain path measure · Expectation under the chain started from a point · Path filtration · Path shifted by a random time

Proof usesTime shift on path space · Strong Markov property for a.s.-finite stopping times

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.