Commit 2024-07-29 17:43 4196dc8a

View on Github →

feat: define logarithmic derivatives (#12804) We define the logarithmic derivative of a function as f'/f and then prove some basic facts about this. Specifially some things that will be needed for the Mittag-Leffler Expansion for Cotangent Function.

Estimated changes

added def logDeriv
added theorem logDeriv_apply
added theorem logDeriv_comp
added theorem logDeriv_const
added theorem logDeriv_const_mul
added theorem logDeriv_fun_pow
added theorem logDeriv_fun_zpow
added theorem logDeriv_id'
added theorem logDeriv_id
added theorem logDeriv_inv
added theorem logDeriv_mul
added theorem logDeriv_mul_const
added theorem logDeriv_pow
added theorem logDeriv_prod
added theorem logDeriv_zpow
added theorem Complex.LogDeriv_exp
added theorem Complex.logDeriv_cos
added theorem Complex.logDeriv_cosh
added theorem Complex.logDeriv_sin
added theorem Real.LogDeriv_exp
added theorem Real.logDeriv_cos
added theorem Real.logDeriv_cosh
added theorem Real.logDeriv_sin
added theorem Complex.cot_conj
added theorem Complex.ofReal_cot