Commit 2025-02-17 23:56 f1ac0a02

View on Github →

feat(Analysis): lower bound for log (1 + x) (#21671)

Estimated changes

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

added theorem Real.hasSum_log_one_add

added theorem Real.le_log_one_add_of_nonneg

added theorem Real.lt_log_one_add_of_pos

Modified Mathlib/Topology/Algebra/InfiniteSum/Order.lean

added theorem lt_hasProd