Theorems · Theorem · probability

ProbabilityTheory.setIntegral_condKernel_univ_right

∀ {α : 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 κ] {E : Type u_4} {f : β × Ω → E} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℝ E] (a : α) {s : Set β},
  MeasurableSet s →
    MeasureTheory.IntegrableOn f (s ×ˢ Set.univ) (κ a) →
      ∫ (b : β) in s, ∫ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedProbabilityTheory.IsFiniteKernelNormedAddCommGroupNormedSpace