Commit 2022-01-18 21:06 6dd65257

View on Github →

feat(measure_theory/measure/measure_space): better definition of to_measurable (#11529) Currently, to_measurable μ t picks a measurable superset of t with the same measure. When the measure of t is infinite, it is most often useless. This PR adjusts the definition so that, in the case of sigma-finite spaces, to_measurable μ t has good properties even when t has infinite measure.

Estimated changes

Modified src/measure_theory/measure/measure_space.lean

added theorem measure_theory.is_locally_finite_measure_of_is_finite_measure_on_compacts

added theorem measure_theory.measure.exists_subset_measure_lt_top

added theorem measure_theory.measure.measure_to_measurable_inter_of_sigma_finite

added theorem measure_theory.nonempty_inter_of_measure_lt_add'

added theorem measure_theory.nonempty_inter_of_measure_lt_add

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.ae_eq_set_inter

added theorem measure_theory.ae_le_set_inter

modified def measure_theory.to_measurable