Theorems · Theorem · probability

MeasureTheory.Integrable.integral_condKernel

∀ {α : Type u_1} {Ω : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω]
  [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E]
  {ρ : MeasureTheory.Measure (α × Ω)} [inst_5 : MeasureTheory.IsFiniteMeasure ρ] {f : α × Ω → E},
  MeasureTheory.Integrable f ρ → MeasureTheory.Integrable (fun x => ∫ (y : Ω), f (x, y) ∂ρ.condKernel x) ρ.fst

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyNormedAddCommGroupNormedSpaceMeasureTheory.IsFiniteMeasure