Theorems · Definition · probability

ProbabilityTheory.Kernel.trajContent

{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.AddContent ENNReal (MeasureTheory.measurableCylinders X)

Given a family of kernels κ : (n : ℕ) → Kernel (Π i : Iic n, X i) (X (n + 1)), and the trajectory up to time a we can construct an additive content over cylinders. It corresponds to composing the kernels, starting at time a + 1.

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

9 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceProbabilityTheory.IsMarkovKernel