Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-25 15:41 3f5c9d30

View on Github →

feat(probability/probability_mass_function): construct a pmf from a probability measure (#18270) Given a measurable space α with a measurable_singleton_class instance, this PR defines a function measure.to_pmf that converts a probability measure μ to a pmf, by defining the mass of a point x to be the measure of the singleton set {x} under μ.

Estimated changes

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.measure.tsum_indicator_apply_singleton

Modified src/probability/probability_mass_function/basic.lean

added def measure_theory.measure.to_pmf

added theorem measure_theory.measure.to_pmf_apply

added theorem measure_theory.measure.to_pmf_to_measure

added theorem pmf.to_measure_eq_iff_eq_to_pmf

added theorem pmf.to_measure_inj

added theorem pmf.to_measure_injective

added theorem pmf.to_measure_to_pmf

modified theorem pmf.to_outer_measure_apply_inter_support

modified theorem pmf.to_outer_measure_caratheodory

added theorem pmf.to_outer_measure_inj

added theorem pmf.to_outer_measure_injective

added theorem pmf.to_pmf_eq_iff_to_measure_eq

Modified src/probability/probability_mass_function/monad.lean

added theorem pmf.to_measure_pure

modified theorem pmf.to_measure_pure_apply

added theorem pmf.to_pmf_dirac