Theorems · Theorem · probability

MeasureTheory.Integrable.integral_norm_condKernel

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

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyNormedAddCommGroupMeasureTheory.IsFiniteMeasure