Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-16 18:36 7459c21c

View on Github →

feat(analysis/special_functions): strict differentiability of real.exp and real.log (#6256)

Estimated changes

Modified src/analysis/special_functions/exp_log.lean

added theorem has_strict_deriv_at.exp

added theorem has_strict_deriv_at.log

added theorem has_strict_fderiv_at.exp

added theorem has_strict_fderiv_at.log

deleted theorem real.has_deriv_at_log_of_pos

added theorem real.has_strict_deriv_at_exp

added theorem real.has_strict_deriv_at_log

added theorem real.has_strict_deriv_at_log_of_pos

modified theorem real.times_cont_diff_at_log

added theorem times_cont_diff.log

added theorem times_cont_diff_at.log

added theorem times_cont_diff_on.log

added theorem times_cont_diff_within_at.log