Theorems · Theorem · probability

ProbabilityTheory.integral_bernoulliMeasure

∀ {X : Type u_1} [inst : MeasurableSpace X] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSingletonClass X] (x y : X) (p : ↑unitInterval) (f : X → E),
  ∫ (z : X), f z ∂ProbabilityTheory.bernoulliMeasure x y p = ↑p • f x + (1 - ↑p) • f y

Defined in

Mathlib.Probability.Distributions.Bernoulli

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceCompleteSpaceMeasurableSingletonClass