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 a ∂p.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 a ∂p.toMeasure = Finset.univ.sum fun (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