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 p.toMeasure) :
∫ (a : α), f ap.toMeasure = ∑' (a : α), (p a).toReal 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 ap.toMeasure = a : α, (p a).toReal f a
theorem PMF.bernoulli_expectation {p : ENNReal} (h : p 1) :
∫ (b : Bool), bif b then 1 else 0(PMF.bernoulli p h).toMeasure = p.toReal