Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-10 19:12 62c1912e

View on Github →

chore(measure_theory/set_integral): use weaker assumptions here and there (#5647)

use ae_measurable f (μ.restrict s) in more lemmas;
introduce measurable_at_filter and use it.

Estimated changes

Modified src/measure_theory/interval_integral.lean

modified theorem interval_integral.fderiv_integral

modified theorem interval_integral.fderiv_integral_of_tendsto_ae

modified theorem interval_integral.integral_has_fderiv_at

modified theorem interval_integral.integral_has_fderiv_at_of_tendsto_ae

modified theorem interval_integral.measure_integral_sub_linear_is_o_of_tendsto_ae

Modified src/measure_theory/measurable_space.lean

added theorem filter.eventually.exists_measurable_mem_of_lift'

modified theorem subsingleton.is_measurable

modified theorem subsingleton.measurable

Modified src/measure_theory/measure_space.lean

added theorem ae_measurable.ae_inf_principal_eq_mk

added theorem ae_measurable.ae_mem_imp_eq_mk

added theorem ae_measurable.mono_set

added theorem ae_measurable_zero

added theorem measure_theory.ae_imp_of_ae_restrict

added theorem measure_theory.ae_zero

added theorem measure_theory.le_ae_restrict

added theorem measure_theory.measure.measure_inter_eq_zero_of_restrict

added theorem subsingleton.ae_measurable

Modified src/measure_theory/set_integral.lean

added theorem ae_measurable.measurable_at_filter_of_mem

added theorem continuous_on.integrable_at_nhds_within

added theorem continuous_on.integral_sub_linear_is_o_ae

added theorem continuous_within_at.integral_sub_linear_is_o_ae

added theorem measurable_at_bot

added def measurable_at_filter

modified theorem measure_theory.measure.finite_at_filter.integrable_at_filter

modified theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto

modified theorem measure_theory.measure.finite_at_filter.integrable_at_filter_of_tendsto_ae

added theorem measure_theory.set_integral_congr

added theorem measure_theory.set_integral_congr_ae