Commit 2023-07-25 06:02 4bf4f50c

View on Github →

chore(MeasureSpace): move dirac and count to new files (#6116)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

deleted theorem MeasureTheory.restrict_dirac'

deleted theorem MeasureTheory.restrict_dirac

Created Mathlib/MeasureTheory/Measure/Count.lean

added def MeasureTheory.Measure.count

added theorem MeasureTheory.Measure.count_apply

added theorem MeasureTheory.Measure.count_apply_eq_top'

added theorem MeasureTheory.Measure.count_apply_eq_top

added theorem MeasureTheory.Measure.count_apply_finite'

added theorem MeasureTheory.Measure.count_apply_finite

added theorem MeasureTheory.Measure.count_apply_finset'

added theorem MeasureTheory.Measure.count_apply_finset

added theorem MeasureTheory.Measure.count_apply_infinite

added theorem MeasureTheory.Measure.count_apply_lt_top'

added theorem MeasureTheory.Measure.count_apply_lt_top

added theorem MeasureTheory.Measure.count_empty

added theorem MeasureTheory.Measure.count_eq_zero_iff'

added theorem MeasureTheory.Measure.count_eq_zero_iff

added theorem MeasureTheory.Measure.count_injective_image'

added theorem MeasureTheory.Measure.count_injective_image

added theorem MeasureTheory.Measure.count_ne_zero'

added theorem MeasureTheory.Measure.count_ne_zero

added theorem MeasureTheory.Measure.count_singleton'

added theorem MeasureTheory.Measure.count_singleton

added theorem MeasureTheory.Measure.empty_of_count_eq_zero'

added theorem MeasureTheory.Measure.empty_of_count_eq_zero

added theorem MeasureTheory.Measure.le_count_apply

Created Mathlib/MeasureTheory/Measure/Dirac.lean

added def MeasureTheory.Measure.dirac

added theorem MeasureTheory.Measure.dirac_apply'

added theorem MeasureTheory.Measure.dirac_apply

added theorem MeasureTheory.Measure.dirac_apply_of_mem

added theorem MeasureTheory.Measure.le_dirac_apply

added theorem MeasureTheory.Measure.map_dirac

added theorem MeasureTheory.Measure.map_eq_sum

added theorem MeasureTheory.Measure.restrict_singleton

added theorem MeasureTheory.Measure.sum_smul_dirac

added theorem MeasureTheory.Measure.tsum_indicator_apply_singleton

added theorem MeasureTheory.ae_dirac_eq

added theorem MeasureTheory.ae_dirac_iff

added theorem MeasureTheory.ae_eq_dirac'

added theorem MeasureTheory.ae_eq_dirac

added theorem MeasureTheory.mem_ae_dirac_iff

added theorem MeasureTheory.restrict_dirac'

added theorem MeasureTheory.restrict_dirac

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted def MeasureTheory.Measure.count

deleted theorem MeasureTheory.Measure.count_apply

deleted theorem MeasureTheory.Measure.count_apply_eq_top'

deleted theorem MeasureTheory.Measure.count_apply_eq_top

deleted theorem MeasureTheory.Measure.count_apply_finite'

deleted theorem MeasureTheory.Measure.count_apply_finite

deleted theorem MeasureTheory.Measure.count_apply_finset'

deleted theorem MeasureTheory.Measure.count_apply_finset

deleted theorem MeasureTheory.Measure.count_apply_infinite

deleted theorem MeasureTheory.Measure.count_apply_lt_top'

deleted theorem MeasureTheory.Measure.count_apply_lt_top

deleted theorem MeasureTheory.Measure.count_empty

deleted theorem MeasureTheory.Measure.count_eq_zero_iff'

deleted theorem MeasureTheory.Measure.count_eq_zero_iff

deleted theorem MeasureTheory.Measure.count_injective_image'

deleted theorem MeasureTheory.Measure.count_injective_image

deleted theorem MeasureTheory.Measure.count_ne_zero'

deleted theorem MeasureTheory.Measure.count_ne_zero

deleted theorem MeasureTheory.Measure.count_singleton'

deleted theorem MeasureTheory.Measure.count_singleton

deleted def MeasureTheory.Measure.dirac

deleted theorem MeasureTheory.Measure.dirac_apply'

deleted theorem MeasureTheory.Measure.dirac_apply

deleted theorem MeasureTheory.Measure.dirac_apply_of_mem

deleted theorem MeasureTheory.Measure.empty_of_count_eq_zero'

deleted theorem MeasureTheory.Measure.empty_of_count_eq_zero

deleted theorem MeasureTheory.Measure.le_count_apply

deleted theorem MeasureTheory.Measure.le_dirac_apply

deleted theorem MeasureTheory.Measure.map_dirac

deleted theorem MeasureTheory.Measure.map_eq_sum

deleted theorem MeasureTheory.Measure.restrict_singleton

deleted theorem MeasureTheory.Measure.sum_smul_dirac

deleted theorem MeasureTheory.Measure.tsum_indicator_apply_singleton

deleted theorem MeasureTheory.ae_dirac_eq

deleted theorem MeasureTheory.ae_dirac_iff

deleted theorem MeasureTheory.ae_eq_dirac'

deleted theorem MeasureTheory.ae_eq_dirac

deleted theorem MeasureTheory.mem_ae_dirac_iff

Modified Mathlib/Probability/CondCount.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean