Commit 2025-01-15 10:30 8a921747
View on Github →feat: establish integrability and integrals of Real.log on arbitrary intervals (#20682)
Establish interval integrability for Real.log on arbitrary intervals, remove an unnecessary assumption in the theorem
integral_log
which computes the integrals, and remove the theorems integral_log_of_pos
and integral_log_of_neg
which are now superfluous. Add theorems concerning integrability of even/odd functions; these are used in the proof and might be of general interest. Minor docu change: Add a missing section heading in Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
Rationale: I considered adding a new theorem rather than changing integral_log
, but I see no value in having a theorem with unnecessary assumptions. For improved compatibility, I also considered depreciating integral_log_of_pos
and integral_log_of_neg
rather than removing them, but then the linter complained about unused assumptions in those theorems.
Breaking change: Deleted assumptions in integral_log
. Removed theorems integral_log_of_pos
and integral_log_of_neg
. These are replaced by integral_log
, which gives the same conclusion without assumption.