Commit 2023-12-18 01:51 6a04469e

View on Github →

feat: properties of x ↦ - x * log x (#8922) Continuity, concavity, first two derivatives of x ↦ - x * log x. From the PFR project.

Estimated changes

added theorem Real.convexOn_mul_log
added theorem Real.deriv2_mul_log
added theorem Real.deriv2_negMulLog
added theorem Real.deriv_mul_log
added theorem Real.deriv_negMulLog
added theorem Real.mul_log_nonneg
added theorem Real.mul_log_nonpos
added theorem Real.negMulLog_def
added theorem Real.negMulLog_eq_neg
added theorem Real.negMulLog_mul
added theorem Real.negMulLog_nonneg
added theorem Real.negMulLog_one
added theorem Real.negMulLog_zero