Theorems · Theorem · probability

MeasureTheory.Measure.condKernel_apply_of_ne_zero

∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] {ρ : MeasureTheory.Measure (α × Ω)} [inst_2 : MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α] {x : α}, ρ.fst {x} ≠ 0 → ∀ (s : Set Ω), (ρ.condKernel x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

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

Defined in

Mathlib.Probability.Kernel.Disintegration.StandardBorel

Cited by

1 results in Mathlib

Foundations

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

Assumes

StandardBorelSpaceNonemptyMeasureTheory.IsFiniteMeasureMeasurableSingletonClass