Theorems · Definition · probability

ProbabilityTheory.Kernel.partialTraj

{X : ℕ → Type u_1} →
  {mX : (n : ℕ) → MeasurableSpace (X n)} →
    ((n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      (a b : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((i : ↥(Finset.Iic b)) → X ↑i)

Given a family of kernels κ n from X 0 × ... × X n to X (n + 1) for all n, construct a kernel from X 0 × ... × X a to X 0 × ... × X b by iterating κ. The idea is that the input is some trajectory up to time a, and the output is the distribution of the trajectory up to time b. In particular if b ≤ a, this is just a deterministic kernel (see partialTraj_le). The name partialTraj stands for "partial trajectory". This kernel can be extended into a kernel with codomain Π n, X n via the Ionescu-Tulcea theorem.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Cited by

44 results in Mathlib

Foundations

Depth 222 from the axioms · uses propext, Classical.choice, Quot.sound