Theorems · Theorem · probability

ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [StandardBorelSpace β]
  (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsDeterministic κ],
  ∃ f, ∃ (hf : Measurable f), κ = ProbabilityTheory.Kernel.deterministic f hf

in a standard Borel space, a deterministic Markov kernel is a Dirac kernel of one measurable function.

Defined in

Mathlib.Probability.Kernel.Deterministic

Cited by

0 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceProbabilityTheory.IsMarkovKernelProbabilityTheory.IsDeterministic