Commit 2025-08-13 12:33 ba27a424

View on Github →

refactor(Intervalintegral): generalise to enorms (#27418) Not exhaustive yet; the remaining lemmas require further progress in LocallyIntegrable.

Estimated changes

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

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

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

modified theorem IntervalIntegrable.add

modified theorem IntervalIntegrable.comp_mul_left_iff

modified theorem IntervalIntegrable.comp_sub_left

modified theorem IntervalIntegrable.comp_sub_left_iff

modified theorem IntervalIntegrable.congr

modified theorem IntervalIntegrable.congr_codiscreteWithin

added theorem IntervalIntegrable.enorm

modified theorem IntervalIntegrable.iff_comp_neg

added theorem IntervalIntegrable.intervalIntegrable_enorm_iff

modified theorem IntervalIntegrable.mono_fun'

modified theorem IntervalIntegrable.mono_fun

added theorem IntervalIntegrable.mono_fun_enorm'

added theorem IntervalIntegrable.mono_fun_enorm

modified theorem IntervalIntegrable.neg

modified theorem IntervalIntegrable.norm

modified theorem IntervalIntegrable.smul

modified theorem IntervalIntegrable.sub

modified theorem IntervalIntegrable.sum

modified def IntervalIntegrable

modified theorem intervalIntegrable_congr_codiscreteWithin

modified theorem intervalIntegrable_const

modified theorem intervalIntegrable_const_iff