Commit 2024-08-10 08:13 a43394c0

View on Github →

feat: Generalize statements about deriv of MulLog (#14594) Uses non-differentiability to generalize statements about deriv of MulLog

Estimated changes

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

modified theorem Real.deriv2_mul_log

modified theorem Real.deriv2_negMulLog

added theorem Real.deriv_mul_log_zero

added theorem Real.differentiableAt_negMulLog_iff

added theorem Real.not_DifferentiableAt_log_mul_zero

added theorem Real.not_continuousAt_deriv_mul_log_zero

Modified Mathlib/Topology/Basic.lean

added theorem not_continuousAt_of_tendsto