Commit 2023-05-20 16:09 62e46941

View on Github →

feat: port Analysis.SpecialFunctions.Log.Monotone (#4144)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean

added theorem Real.log_div_self_antitoneOn

added theorem Real.log_div_self_rpow_antitoneOn

added theorem Real.log_div_sqrt_antitoneOn

added theorem Real.log_mul_self_monotoneOn