Theorems · Theorem · probability

ProbabilityTheory.Kernel.absolutelyContinuous_comp_of_absolutelyContinuous

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ]
  [StandardBorelSpace Ω] [Nonempty Ω] [MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧] {ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.SFinite ν],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous ν) → ∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous (μ.bind ⇑κ)

Defined in

Mathlib.Probability.Kernel.Posterior

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureProbabilityTheory.IsFiniteKernelStandardBorelSpaceNonemptyMeasurableSpace.CountableOrCountablyGeneratedMeasureTheory.SFinite