Homogeneous Markov chains as trajectory measures

This file packages the Ionescu--Tulcea trajectory construction for a homogeneous Markov kernel and identifies every coordinate marginal with the usual recursive iterate of the initial law.

def FD1D.TrajectoryBridge.iterateLaw {α : Type u_1} [MeasurableSpace α] (κ : ProbabilityTheory.Kernel α α) (μ₀ : MeasureTheory.Measure α) : ℕ → MeasureTheory.Measure α

The state law obtained after recursively applying a homogeneous kernel.

Equations

• FD1D.TrajectoryBridge.iterateLaw κ μ₀ 0 = μ₀
• FD1D.TrajectoryBridge.iterateLaw κ μ₀ n.succ = (FD1D.TrajectoryBridge.iterateLaw κ μ₀ n).bind ⇑κ

@[simp]

theorem FD1D.TrajectoryBridge.iterateLaw_zero {α : Type u_1} [MeasurableSpace α] (κ : ProbabilityTheory.Kernel α α) (μ₀ : MeasureTheory.Measure α) : iterateLaw κ μ₀ 0 = μ₀

@[simp]

theorem FD1D.TrajectoryBridge.iterateLaw_succ {α : Type u_1} [MeasurableSpace α] (κ : ProbabilityTheory.Kernel α α) (μ₀ : MeasureTheory.Measure α) (n : ℕ) : iterateLaw κ μ₀ (n + 1) = (iterateLaw κ μ₀ n).bind ⇑κ

def FD1D.TrajectoryBridge.historyKernel {α : Type u_1} [MeasurableSpace α] (κ : ProbabilityTheory.Kernel α α) (n : ℕ) : ProbabilityTheory.Kernel (↥(Finset.Iic n) → α) α

A homogeneous kernel viewed as a history-dependent kernel.

Equations

• FD1D.TrajectoryBridge.historyKernel κ n = κ.comap (fun (h : ↥(Finset.Iic n) → α) => h ⟨n, ⋯⟩) ⋯

instance FD1D.TrajectoryBridge.historyKernel.instIsMarkovKernel {α : Type u_1} [MeasurableSpace α] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : ProbabilityTheory.IsMarkovKernel (historyKernel κ n)

noncomputable def FD1D.TrajectoryBridge.trajectoryLaw {α : Type u_1} [MeasurableSpace α] (μ₀ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.Measure (ℕ → α)

The single path-space law generated from μ₀ by repeatedly applying κ.

Equations

• FD1D.TrajectoryBridge.trajectoryLaw μ₀ κ = ProbabilityTheory.Kernel.trajMeasure μ₀ (FD1D.TrajectoryBridge.historyKernel κ)

theorem FD1D.TrajectoryBridge.trajectoryLaw_marginal_zero {α : Type u_1} [MeasurableSpace α] (μ₀ : MeasureTheory.Measure α) (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] : MeasureTheory.Measure.map (fun (path : ℕ → α) => path 0) (trajectoryLaw μ₀ κ) = μ₀

theorem FD1D.TrajectoryBridge.trajectoryLaw_marginal_succ {α : Type u_1} [MeasurableSpace α] (μ₀ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ₀] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → α) => path (n + 1)) (trajectoryLaw μ₀ κ) = (MeasureTheory.Measure.map (fun (path : ℕ → α) => path n) (trajectoryLaw μ₀ κ)).bind ⇑κ

theorem FD1D.TrajectoryBridge.trajectoryLaw_marginal {α : Type u_1} [MeasurableSpace α] (μ₀ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ₀] (κ : ProbabilityTheory.Kernel α α) [ProbabilityTheory.IsMarkovKernel κ] (n : ℕ) : MeasureTheory.Measure.map (fun (path : ℕ → α) => path n) (trajectoryLaw μ₀ κ) = iterateLaw κ μ₀ n