Theorems · Theorem · probability

MeasureTheory.Integrable.condKernel_ae

∀ {α : 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 ρ → ∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun ω => f (a, ω)) (ρ.condKernel a)

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyNormedAddCommGroupMeasureTheory.IsFiniteMeasure