Theorems · Theorem · probability

MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff

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

Defined in

Mathlib.Probability.Kernel.Disintegration.Integral

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceStandardBorelSpaceNonemptyNormedAddCommGroupMeasureTheory.IsFiniteMeasure