Theorems · Theorem · probability

MeasureTheory.Measure.setIntegral_condKernel_univ_left

∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {E : Type u_3}
  {f : β × Ω → E} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℝ E] {t : Set Ω},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f (Set.univ ×ˢ t) ρ →
      ∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasureTheory.IsFiniteMeasureNormedAddCommGroupNormedSpace