Bernoulli distribution: bind and variance #
Binding a kernel through Ber(x, y, p) is the p-mixture of its two values, and the variance of
a real observable under Ber(x, y, p) is p * (1 - p) * (f x - f y) ^ 2.
Main results #
ProbabilityTheory.bernoulliMeasure_bind:Ber(x, y, p).bind f = p • f x + (1 - p) • f y.ProbabilityTheory.variance_bernoulliMeasure:Var[f; Ber(x, y, p)] = p * (1 - p) * (f x - f y) ^ 2.
[UPSTREAM] candidates for Mathlib.Probability.Distributions.Bernoulli.
theorem
ProbabilityTheory.bernoulliMeasure_bind
{X : Type u_1}
{Y : Type u_2}
[MeasurableSpace X]
[MeasurableSpace Y]
[MeasurableSingletonClass X]
(x y : X)
(p : ↑unitInterval)
{f : X → MeasureTheory.Measure Y}
(hf : Measurable f)
:
(bernoulliMeasure x y p).bind f = unitInterval.toNNReal p • f x + unitInterval.toNNReal (unitInterval.symm p) • f y
theorem
ProbabilityTheory.variance_bernoulliMeasure
{X : Type u_1}
[MeasurableSpace X]
[MeasurableSingletonClass X]
(x y : X)
(p : ↑unitInterval)
{f : X → ℝ}
(hf : AEMeasurable f (bernoulliMeasure x y p))
:
variance f (bernoulliMeasure x y p) = ↑p * (1 - ↑p) * (f x - f y) ^ 2