Theorems · Theorem · probability

ProbabilityTheory.Kernel.partialTraj_succ_self

∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (a : ℕ),
  ProbabilityTheory.Kernel.partialTraj κ a (a + 1) =
    (ProbabilityTheory.Kernel.id.prod ((κ a).map ⇑(MeasurableEquiv.piSingleton a))).map (IicProdIoc a (a + 1))

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Cited by

6 results in Mathlib

Foundations

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