Theorems · Theorem · probability

MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod

∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {s : Set β},
  MeasurableSet s → ∀ {t : Set Ω}, MeasurableSet t → ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasureTheory.IsFiniteMeasure