Theorem Real.half_mul_log_add_log_abs

Modification history

2025-10-31 17:31
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
chore(Analysis/SpecialFunctions/Log/PosLog): uniformize variable names (#31084) …
Modified Real.half_mul_log_add_log_absView on Github →
2025-01-31 20:04
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) …
Added Real.half_mul_log_add_log_absView on Github →