Theorems · Theorem · probability

ProbabilityTheory.Kernel.integral_withDensity

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E}
  [inst_2 : ProbabilityTheory.IsSFiniteKernel κ] {a : α} {g : α → β → NNReal},
  Measurable (Function.uncurry g) → ∫ (b : β), f b ∂(κ.withDensity fun a b => ↑(g a b)) a = ∫ (b : β), g a b • f b ∂κ a

Defined in

Mathlib.Probability.Kernel.WithDensity

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceProbabilityTheory.IsSFiniteKernel