Theorems · Definition · probability

ProbabilityTheory.Kernel.trajFun

{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 : ℕ) → ((i : ↥(Finset.Iic a)) → X ↑i) → MeasureTheory.Measure ((n : ℕ) → X n)

This function is the kernel given by the Ionescu-Tulcea theorem. It is shown below that it is measurable and turned into a true kernel in Kernel.traj.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

6 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceProbabilityTheory.IsMarkovKernel