Commit 2023-06-05 07:16 23cb0166

View on Github →

feat: port Analysis.SpecialFunctions.Log.Deriv (#4669)

Estimated changes

Modified Mathlib.lean

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

added theorem ContDiff.log

added theorem ContDiffAt.log

added theorem ContDiffOn.log

added theorem ContDiffWithinAt.log

added theorem Differentiable.log

added theorem DifferentiableAt.log

added theorem DifferentiableOn.log

added theorem DifferentiableWithinAt.log

added theorem HasDerivAt.log

added theorem HasDerivWithinAt.log

added theorem HasFDerivAt.log

added theorem HasFDerivWithinAt.log

added theorem HasStrictDerivAt.log

added theorem HasStrictFDerivAt.log

added theorem Real.abs_log_sub_add_sum_range_le

added theorem Real.contDiffAt_log

added theorem Real.contDiffOn_log

added theorem Real.deriv_log'

added theorem Real.deriv_log

added theorem Real.differentiableAt_log

added theorem Real.differentiableAt_log_iff

added theorem Real.differentiableOn_log

added theorem Real.hasDerivAt_log

added theorem Real.hasStrictDerivAt_log

added theorem Real.hasStrictDerivAt_log_of_pos

added theorem Real.hasSum_log_one_add_inv

added theorem Real.hasSum_log_sub_log_of_abs_lt_1

added theorem Real.hasSum_pow_div_log_of_abs_lt_1

added theorem Real.tendsto_mul_log_one_plus_div_atTop

added theorem deriv.log

added theorem derivWithin.log

added theorem fderiv.log

added theorem fderivWithin.log