Commit 2025-04-19 15:05 90fd7ea4

View on Github →

feat: drop measurability assumption in norm_setIntegral_le_of_norm_le_const_ae' (#24134)

Estimated changes

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean

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

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

deleted theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const'

modified theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const

deleted theorem MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae''

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

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

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean