Theorems · Definition · probability

ProbabilityTheory.Kernel.traj

• 1000+ list: Ionescu-Tulcea theorem

{X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] →
    (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) →
      [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] →
        (a : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((n : ℕ) → X n)

Ionescu-Tulcea Theorem : Given a family of kernels κ n taking variables in Iic n with value in X (n + 1), the kernel traj κ a takes a variable x depending on the variables i ≤ a and associates to it a kernel on trajectories depending on all variables, where the entries with index ≤ a are those of x, and then one follows iteratively the kernels κ a, then κ (a + 1), and so on. The fact that such a kernel exists on infinite trajectories is not obvious, and is the content of the Ionescu-Tulcea theorem.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

26 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceProbabilityTheory.IsMarkovKernel