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