Commit 2022-02-05 09:52 99693218

View on Github →

feat(measure_theory/probability_mass_function): Lemmas connecting pmf.support and pmf.to_measure (#11842) Add lemmas relating the support of a pmf to the measures of sets under the induced measure.

Estimated changes

Modified src/measure_theory/probability_mass_function/basic.lean

modified theorem pmf.to_measure_apply'

modified theorem pmf.to_measure_apply

added theorem pmf.to_measure_apply_eq_of_inter_support_eq

added theorem pmf.to_measure_apply_eq_one_iff

modified theorem pmf.to_measure_apply_eq_to_outer_measure_apply

modified theorem pmf.to_measure_apply_finset

modified theorem pmf.to_measure_apply_fintype

added theorem pmf.to_measure_apply_inter_support

modified theorem pmf.to_measure_apply_of_finite

added theorem pmf.to_measure_mono

modified theorem pmf.to_outer_measure_apply'

modified theorem pmf.to_outer_measure_apply

added theorem pmf.to_outer_measure_apply_eq_of_inter_support_eq

added theorem pmf.to_outer_measure_apply_eq_one_iff

modified theorem pmf.to_outer_measure_apply_eq_zero_iff

modified theorem pmf.to_outer_measure_apply_finset

modified theorem pmf.to_outer_measure_apply_fintype

added theorem pmf.to_outer_measure_apply_inter_support

modified theorem pmf.to_outer_measure_apply_le_to_measure_apply

added theorem pmf.to_outer_measure_mono