Commit 2022-02-23 12:32 b0fbd912

View on Github →

feat(measure_theory/measure): generalize scalar actions (#12187) As a result of this change, many smul lemmas now also apply to nat and nnreal, which allows some lemmas to be removed.

Estimated changes

Modified src/measure_theory/covering/differentiation.lean

Modified src/measure_theory/decomposition/lebesgue.lean

Modified src/measure_theory/integral/set_to_l1.lean

Modified src/measure_theory/measure/haar.lean

Modified src/measure_theory/measure/hausdorff.lean

Modified src/measure_theory/measure/lebesgue.lean

Modified src/measure_theory/measure/measure_space.lean

modified theorem ae_measurable.smul_measure

modified theorem measure_theory.ae_smul_measure

deleted theorem measure_theory.measure.coe_nnreal_smul

modified theorem measure_theory.measure.coe_smul

modified theorem measure_theory.measure.smul_apply

modified theorem measure_theory.measure.smul_to_outer_measure

Modified src/measure_theory/measure/outer_measure.lean

added def measure_theory.outer_measure.coe_fn_add_monoid_hom

modified theorem measure_theory.outer_measure.coe_smul

modified theorem measure_theory.outer_measure.smul_apply

modified theorem measure_theory.outer_measure.smul_supr

modified theorem measure_theory.outer_measure.trim_smul

Modified src/measure_theory/measure/regular.lean

Modified src/measure_theory/measure/vector_measure.lean

Modified src/probability/independence.lean