Theorems · Theorem · probability

ProbabilityTheory.Kernel.setIntegral_deterministic

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {E : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : β → E} {a : α} [CompleteSpace E] {g : α → β}
  [MeasurableSingletonClass β] (hg : Measurable g) (s : Set β) [inst_4 : Decidable (g a ∈ s)],
  ∫ (x : β) in s, f x ∂(ProbabilityTheory.Kernel.deterministic g hg) a = if g a ∈ s then f (g a) else 0

Defined in

Mathlib.Probability.Kernel.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSingletonClassDecidable