Documentation

Mathlib.Probability.ProbabilityMassFunction.Integrals

Integrals with a measure derived from probability mass functions. #

This files connects Pmf with integral. The main result is that the integral (i.e. the expected value) with regard to a measure derived from a Pmf is a sum weighted by the Pmf.

It also provides the expected value for specific probability mass functions.

theorem Pmf.integral_eq_tsum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (p : Pmf α) (f : αE) (hf : MeasureTheory.Integrable f) :
∫ (a : α), f aPmf.toMeasure p = ∑' (a : α), ENNReal.toReal (p a) f a
theorem Pmf.integral_eq_sum {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] [Fintype α] (p : Pmf α) (f : αE) :
∫ (a : α), f aPmf.toMeasure p = Finset.sum Finset.univ fun a => ENNReal.toReal (p a) f a
theorem Pmf.bernoulli_expectation {p : ENNReal} (h : p 1) :
∫ (b : Bool), bif b then 1 else 0Pmf.toMeasure (Pmf.bernoulli p h) = ENNReal.toReal p