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