Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-18 23:32 3ee6248c

View on Github →

feat(measure_theory): links between an integral and its improper version (#7164) This PR introduces ways of studying and computing ∫ x, f x ∂μ by studying the limit of the sequence ∫ x in φ n, f x ∂μ for an appropriate sequence φ of subsets of the domain of f.

Estimated changes

Modified src/measure_theory/integrable_on.lean

added theorem ae_measurable.indicator

added theorem ae_measurable.restrict

added theorem ae_measurable_indicator_iff

deleted theorem measure_theory.ae_measurable_indicator_iff

Created src/measure_theory/integral_eq_improper.lean

added theorem measure_theory.ae_cover.ae_tendsto_indicator

added theorem measure_theory.ae_cover.bInter_Ici_ae_cover

added theorem measure_theory.ae_cover.bUnion_Iic_ae_cover

added theorem measure_theory.ae_cover.comp_tendsto

added theorem measure_theory.ae_cover.integrable_of_integral_norm_tendsto

added theorem measure_theory.ae_cover.integrable_of_integral_tendsto_of_nonneg_ae

added theorem measure_theory.ae_cover.integrable_of_lintegral_nnnorm_tendsto'

added theorem measure_theory.ae_cover.integrable_of_lintegral_nnnorm_tendsto

added theorem measure_theory.ae_cover.integral_eq_of_tendsto

added theorem measure_theory.ae_cover.integral_eq_of_tendsto_of_nonneg_ae

added theorem measure_theory.ae_cover.integral_tendsto_of_countably_generated

added theorem measure_theory.ae_cover.inter_restrict

added theorem measure_theory.ae_cover.lintegral_eq_of_tendsto

added theorem measure_theory.ae_cover.lintegral_tendsto_of_countably_generated

added theorem measure_theory.ae_cover.lintegral_tendsto_of_nat

added theorem measure_theory.ae_cover.restrict

added theorem measure_theory.ae_cover.supr_lintegral_eq_of_countably_generated

added structure measure_theory.ae_cover

added theorem measure_theory.ae_cover_Icc

added theorem measure_theory.ae_cover_Ici

added theorem measure_theory.ae_cover_Ico

added theorem measure_theory.ae_cover_Iic

added theorem measure_theory.ae_cover_Iio

added theorem measure_theory.ae_cover_Ioc

added theorem measure_theory.ae_cover_Ioi

added theorem measure_theory.ae_cover_Ioo

added theorem measure_theory.ae_cover_restrict_of_ae_imp

added theorem measure_theory.integrable_of_interval_integral_norm_tendsto

added theorem measure_theory.integrable_on_Iic_of_interval_integral_norm_tendsto

added theorem measure_theory.integrable_on_Ioi_of_interval_integral_norm_tendsto

added theorem measure_theory.interval_integral_tendsto_integral

added theorem measure_theory.interval_integral_tendsto_integral_Iic

added theorem measure_theory.interval_integral_tendsto_integral_Ioi

Modified src/measure_theory/interval_integral.lean

Modified src/measure_theory/set_integral.lean