Commit 2025-05-22 09:16 ae781008

View on Github →

feat(IntervalIntegral): +1 version of norm_integral_le_of_norm_le (#25075)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

modified theorem Complex.norm_log_one_add_half_le_self

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

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

added theorem intervalIntegral.norm_integral_le_abs_of_norm_le

added theorem intervalIntegral.norm_integral_le_of_norm_le