Theorems · Theorem · probability

PMF.integral_eq_sum

∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [CompleteSpace E] [inst_5 : Fintype α] (p : PMF α) (f : α → E),
  ∫ (a : α), f a ∂p.toMeasure = ∑ a, (p a).toReal • f a

Defined in

Mathlib.Probability.ProbabilityMassFunction.Integrals

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSingletonClassNormedAddCommGroupNormedSpaceCompleteSpaceFintype