Commit 2023-09-15 18:54 a9e352ee

View on Github →

feat: Pmf.integral_eq_sum (#6454) 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 (bernoulli so far).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

added theorem MeasureTheory.hasFiniteIntegral_of_fintype

added theorem MeasureTheory.integrable_of_fintype

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

added def MeasureTheory.SimpleFunc.ofFintype

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem MeasureTheory.stronglyMeasurable_of_fintype

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

modified theorem MeasureTheory.integral_countable'

modified theorem MeasureTheory.integral_countable

modified theorem MeasureTheory.integral_finset

modified theorem MeasureTheory.integral_fintype

modified theorem MeasureTheory.integral_singleton'

modified theorem MeasureTheory.integral_singleton

modified theorem MeasureTheory.integral_unique

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

added theorem Pmf.restrict_toMeasure_support

added theorem Pmf.support_countable

Created Mathlib/Probability/ProbabilityMassFunction/Integrals.lean

added theorem Pmf.bernoulli_expectation

added theorem Pmf.integral_eq_sum

added theorem Pmf.integral_eq_tsum