Commit 2023-06-09 12:20 512a73ef

View on Github →

feat: port MeasureTheory.Integral.IntegralEqImproper (#4864)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem MeasureTheory.AECover.ae_tendsto_indicator

added theorem MeasureTheory.AECover.aemeasurable

added theorem MeasureTheory.AECover.aestronglyMeasurable

added theorem MeasureTheory.AECover.biInter_Ici_aecover

added theorem MeasureTheory.AECover.biUnion_Iic_aecover

added theorem MeasureTheory.AECover.comp_tendsto

added theorem MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated

added theorem MeasureTheory.AECover.integrable_of_integral_bounded_of_nonneg_ae

added theorem MeasureTheory.AECover.integrable_of_integral_norm_bounded

added theorem MeasureTheory.AECover.integrable_of_integral_norm_tendsto

added theorem MeasureTheory.AECover.integrable_of_integral_tendsto_of_nonneg_ae

added theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded'

added theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded

added theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_tendsto'

added theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_tendsto

added theorem MeasureTheory.AECover.integral_eq_of_tendsto

added theorem MeasureTheory.AECover.integral_eq_of_tendsto_of_nonneg_ae

added theorem MeasureTheory.AECover.integral_tendsto_of_countably_generated

added theorem MeasureTheory.AECover.inter

added theorem MeasureTheory.AECover.inter_restrict

added theorem MeasureTheory.AECover.lintegral_eq_of_tendsto

added theorem MeasureTheory.AECover.lintegral_tendsto_of_countably_generated

added theorem MeasureTheory.AECover.lintegral_tendsto_of_nat

added theorem MeasureTheory.AECover.mono

added theorem MeasureTheory.AECover.mono_ac

added theorem MeasureTheory.AECover.superset

added structure MeasureTheory.AECover

added theorem MeasureTheory.aecover_Icc

added theorem MeasureTheory.aecover_Icc_of_Icc

added theorem MeasureTheory.aecover_Icc_of_Ico

added theorem MeasureTheory.aecover_Icc_of_Ioc

added theorem MeasureTheory.aecover_Icc_of_Ioo

added theorem MeasureTheory.aecover_Ici

added theorem MeasureTheory.aecover_Ico

added theorem MeasureTheory.aecover_Ico_of_Icc

added theorem MeasureTheory.aecover_Ico_of_Ico

added theorem MeasureTheory.aecover_Ico_of_Ioc

added theorem MeasureTheory.aecover_Ico_of_Ioo

added theorem MeasureTheory.aecover_Iic

added theorem MeasureTheory.aecover_Iio

added theorem MeasureTheory.aecover_Iio_of_Iic

added theorem MeasureTheory.aecover_Iio_of_Iio

added theorem MeasureTheory.aecover_Ioc

added theorem MeasureTheory.aecover_Ioc_of_Icc

added theorem MeasureTheory.aecover_Ioc_of_Ico

added theorem MeasureTheory.aecover_Ioc_of_Ioc

added theorem MeasureTheory.aecover_Ioc_of_Ioo

added theorem MeasureTheory.aecover_Ioi

added theorem MeasureTheory.aecover_Ioi_of_Ici

added theorem MeasureTheory.aecover_Ioi_of_Ioi

added theorem MeasureTheory.aecover_Ioo

added theorem MeasureTheory.aecover_Ioo_of_Icc

added theorem MeasureTheory.aecover_Ioo_of_Ico

added theorem MeasureTheory.aecover_Ioo_of_Ioc

added theorem MeasureTheory.aecover_Ioo_of_Ioo

added theorem MeasureTheory.aecover_restrict_of_ae_imp

added theorem MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_bounded

added theorem MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto

added theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded

added theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_left

added theorem MeasureTheory.integrableOn_Ioc_of_interval_integral_norm_bounded_right

added theorem MeasureTheory.integrableOn_Ioi_comp_mul_left_iff

added theorem MeasureTheory.integrableOn_Ioi_comp_mul_right_iff

added theorem MeasureTheory.integrableOn_Ioi_comp_rpow_iff'

added theorem MeasureTheory.integrableOn_Ioi_comp_rpow_iff

added theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg'

added theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg

added theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonpos'

added theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonpos

added theorem MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_bounded

added theorem MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto

added theorem MeasureTheory.integrable_of_intervalIntegral_norm_bounded

added theorem MeasureTheory.integrable_of_intervalIntegral_norm_tendsto

added theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg'

added theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg

added theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos'

added theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos

added theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'

added theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto

added theorem MeasureTheory.integral_comp_mul_deriv_Ioi

added theorem MeasureTheory.integral_comp_mul_left_Ioi

added theorem MeasureTheory.integral_comp_mul_right_Ioi

added theorem MeasureTheory.integral_comp_rpow_Ioi

added theorem MeasureTheory.integral_comp_rpow_Ioi_of_pos

added theorem MeasureTheory.integral_comp_smul_deriv_Ioi

added theorem MeasureTheory.intervalIntegral_tendsto_integral

added theorem MeasureTheory.intervalIntegral_tendsto_integral_Iic

added theorem MeasureTheory.intervalIntegral_tendsto_integral_Ioi

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.eventually_forall_ge_atTop

added theorem Filter.eventually_forall_le_atBot