Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-14 16:06 c35672bb

View on Github →

feat(analysis/special_functions): strict differentiability of some functions (#6228)

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem has_strict_deriv_at.const_mul

added theorem has_strict_deriv_at.const_sub

added theorem has_strict_deriv_at.div

added theorem has_strict_deriv_at.mul_const

added theorem has_strict_deriv_at_iff_has_strict_fderiv_at

Modified src/analysis/complex/real_deriv.lean

added theorem has_strict_deriv_at.real_of_complex

Modified src/analysis/special_functions/exp_log.lean

added theorem has_strict_deriv_at.cexp

added theorem has_strict_fderiv_at.cexp

Modified src/analysis/special_functions/trigonometric.lean

added theorem complex.has_strict_deriv_at_cos

added theorem complex.has_strict_deriv_at_cosh

added theorem complex.has_strict_deriv_at_sin

added theorem complex.has_strict_deriv_at_sinh

added theorem complex.has_strict_deriv_at_tan

added theorem has_strict_deriv_at.arctan

added theorem has_strict_deriv_at.ccos

added theorem has_strict_deriv_at.ccosh

added theorem has_strict_deriv_at.cos

added theorem has_strict_deriv_at.cosh

added theorem has_strict_deriv_at.csin

added theorem has_strict_deriv_at.csinh

added theorem has_strict_deriv_at.sin

added theorem has_strict_deriv_at.sinh

added theorem has_strict_fderiv_at.arctan

added theorem has_strict_fderiv_at.ccos

added theorem has_strict_fderiv_at.ccosh

added theorem has_strict_fderiv_at.cos

added theorem has_strict_fderiv_at.cosh

added theorem has_strict_fderiv_at.csin

added theorem has_strict_fderiv_at.csinh

added theorem has_strict_fderiv_at.sin

added theorem has_strict_fderiv_at.sinh

added theorem real.has_strict_deriv_at_arccos

added theorem real.has_strict_deriv_at_arcsin

added theorem real.has_strict_deriv_at_arctan

added theorem real.has_strict_deriv_at_cos

added theorem real.has_strict_deriv_at_cosh

added theorem real.has_strict_deriv_at_sin

added theorem real.has_strict_deriv_at_sinh

added theorem real.has_strict_deriv_at_tan