Commit 2020-04-29 16:12 8490c545

View on Github →

refactor(analysis/complex/exponential): define log x = log |x| for x < 0 (#2564) Previously we had log x = 0 for x < 0. This PR changes it to log x = log (-x), to make sure that the formulas log (xy) = log x + log y and log' = 1/x are true for all nonzero variables. Also, add a few simp lemmas on the differentiability properties of log to make sure that the following works:

example (x : ℝ) (h : x ≠ 0) : deriv (λ x, x * (log x - 1)) x = log x :=
by simp [h]

Estimated changes

Modified src/analysis/complex/exponential.lean

added theorem complex.log_of_real_re

added theorem deriv_log'

added theorem deriv_within_log'

added theorem differentiable.log

added theorem differentiable_at.log

added theorem differentiable_on.log

added theorem differentiable_within_at.log

added theorem has_deriv_at.log

added theorem has_deriv_within_at.log

modified theorem real.exp_log

added theorem real.exp_log_eq_abs

modified theorem real.has_deriv_at_log

added theorem real.has_deriv_at_log_of_pos

added theorem real.log_abs

modified theorem real.log_le_log

modified theorem real.log_mul

added theorem real.log_neg_eq_log

modified theorem real.log_nonpos

modified theorem real.log_pos

modified theorem real.log_pos_iff

modified theorem real.rpow_def_of_neg

Modified test/differentiable.lean