Commit 2026-04-28 23:23 51a49eec

feat(Analysis/SpecialFunctions/Log): Extends log_mul_self_StrictMonoOn (#37717)

• Extends log_mul_self_monotoneOn (which had a TODO indicating that it should be extended) to mul_log_self_StrictMonoOn
• Adds inequalities suggested by @SnirBroshi like x - 1 ≤ x * log x
• Consistently uses intervals in Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
• NegMulLog.lean: module docstring explains that (many) lemmas *_mul_log_* are also in this file (Re)naming of lemmas also discussed on Zulip [#mathlib4 > Naming/Spelling: `mul_log` or `log_mul_self`?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.2FSpelling.3A.20.60mul_log.60.20or.20.60log_mul_self.60.3F/with/583877549). Deprecations:
• log_mul_self_monotoneOn (superseded by mul_log_StrictMonoOn)