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 a ∂Pmf.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 a ∂Pmf.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 0 ∂Pmf.toMeasure (Pmf.bernoulli p h) = ENNReal.toReal p