Theorems · Theorem · probability

MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero

∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α] {x : α}, ρ.fst {x} ≠ 0 → ∀ (s : Set Ω), (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

If the singleton {x} has non-zero mass for ρ.fst, then for all s : Set Ω, ρCond x s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s) .

Defined in

Mathlib.Probability.Kernel.Disintegration.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.Measure.IsCondKernelMeasureTheory.IsFiniteMeasureMeasurableSingletonClass