Theorems · Theorem · probability

ProbabilityTheory.Kernel.lintegral_piecewise

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ η : ProbabilityTheory.Kernel α β}
  {s : Set α} {hs : MeasurableSet s} [inst : DecidablePred fun x => x ∈ s] (a : α) (g : β → ENNReal),
  ∫⁻ (b : β), g b ∂(ProbabilityTheory.Kernel.piecewise hs κ η) a =
    if a ∈ s then ∫⁻ (b : β), g b ∂κ a else ∫⁻ (b : β), g b ∂η a

Defined in

Mathlib.Probability.Kernel.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidablePred