Theorems · Theorem · probability

ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel

∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] (κ : ProbabilityTheory.Kernel α (β × Ω))
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] (a : α), (fun b => κ.condKernel (a, b)) =ᵐ[κ.fst a] ⇑(κ a).condKernel

For fst κ a-almost all b, the conditional kernel Kernel.condKernel κ applied to (a, b) is equal to the conditional kernel of the measure κ a applied to b.

Defined in

Mathlib.Probability.Kernel.Disintegration.Unique

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsFiniteKernel