Commit 2025-01-15 10:30 8a921747

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.