Commit 2025-08-11 13:56 89c6ea1f

View on Github →

chore(IntegrableOn): generalise one more section to enorms (#27419)

Estimated changes

Modified Mathlib/Analysis/MellinTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals/LogTrigonometric.lean

Modified Mathlib/MeasureTheory/Integral/ExpDecay.lean

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

modified theorem integrableOn_Icc_iff_integrableOn_Ico'

modified theorem integrableOn_Icc_iff_integrableOn_Ico

modified theorem integrableOn_Icc_iff_integrableOn_Ioc'

modified theorem integrableOn_Icc_iff_integrableOn_Ioc

modified theorem integrableOn_Icc_iff_integrableOn_Ioo'

modified theorem integrableOn_Icc_iff_integrableOn_Ioo

modified theorem integrableOn_Ici_iff_integrableOn_Ioi'

modified theorem integrableOn_Ici_iff_integrableOn_Ioi

modified theorem integrableOn_Ico_iff_integrableOn_Ioo'

modified theorem integrableOn_Ico_iff_integrableOn_Ioo

modified theorem integrableOn_Iic_iff_integrableOn_Iio'

modified theorem integrableOn_Iic_iff_integrableOn_Iio

modified theorem integrableOn_Ioc_iff_integrableOn_Ioo'

modified theorem integrableOn_Ioc_iff_integrableOn_Ioo

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

modified theorem IntervalIntegrable.comp_add_left

modified theorem IntervalIntegrable.comp_add_right

modified theorem IntervalIntegrable.comp_mul_left

modified theorem IntervalIntegrable.comp_mul_left_iff

modified theorem IntervalIntegrable.comp_mul_right

modified theorem IntervalIntegrable.comp_sub_left

modified theorem IntervalIntegrable.comp_sub_left_iff

modified theorem IntervalIntegrable.comp_sub_right

modified theorem IntervalIntegrable.iff_comp_neg

modified theorem intervalIntegrable_iff'

modified theorem intervalIntegrable_iff_integrableOn_Icc_of_le

modified theorem intervalIntegrable_iff_integrableOn_Ico_of_le

modified theorem intervalIntegrable_iff_integrableOn_Ioo_of_le

modified theorem intervalIntegrable_of_odd₀

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean

modified theorem Function.Periodic.intervalIntegrable

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean

Modified Mathlib/NumberTheory/AbelSummation.lean

Modified Mathlib/NumberTheory/LSeries/SumCoeff.lean