Theorems · Definition · probability

ProbabilityTheory.bernoulliMeasure

{X : Type u_1} → [inst : MeasurableSpace X] → X → X → ↑unitInterval → MeasureTheory.Measure X

The Bernoulli distribution over an arbitrary measurable space X. Given x y : X and p : I (I is the unitInterval), it is the measure which gives mass p to {x} and 1 - p to {y}.

Defined in

Mathlib.Probability.Distributions.Bernoulli

Cited by

19 results in Mathlib

Foundations

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

Assumes

MeasurableSpace