Commit 2026-02-10 18:25 a5ff9c09

View on Github →

feat(Mathlib/Analysis/SpecialFunctions/Log/Base): More log asymptotics (#33389) A common utility in proving asymptotics is logb b =O[⊤] log and (log ∘ (c * ·)) =O[atTop] log and related lemmas logb. This PR fills these in for future use.

Estimated changes

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

added theorem Real.isBigO_log_const_mul_log_atTop

added theorem Real.isBigO_log_mul_const_log_atTop

added theorem Real.isBigO_logb_const_mul_log_atTop

added theorem Real.isBigO_logb_log

added theorem Real.isBigO_logb_mul_const_log_atTop

modified theorem Real.logb_neg_base_eq_logb