Commit 2026-08-13 17:23 89efb57b

View on Github →

feat: trivial estimates for the positive part of the logarithm (#42000) Complete API for posLog by adding several trivial but useful estimates.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

added theorem Real.abs_log_eq_posLog_add_posLog_inv

added theorem Real.antitoneOn_posLog

added theorem Real.log_one_add_le_posLog

modified theorem Real.monotoneOn_posLog

added theorem Real.posLog_le_abs

added theorem Real.posLog_le_log_one_add

modified theorem Real.posLog_le_posLog

added theorem Real.posLog_rpow