Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-09 04:36 1f309c52

View on Github →

feat(analysis/special_functions): real.log is infinitely smooth away from zero (#5116) Also redefine it using order_iso.to_homeomorph and prove more lemmas about limits of exp/log.

Estimated changes

added theorem times_cont_diff_on_inv
added theorem continuous.log
added theorem continuous_at.log
added theorem continuous_on.log
added theorem deriv.log
deleted theorem deriv_log'
added theorem deriv_within.log
deleted theorem deriv_within_log'
added theorem fderiv.log
added theorem fderiv_within.log
added theorem filter.tendsto.log
added theorem has_fderiv_at.log
modified theorem measurable.log
added theorem real.comap_exp_at_top
modified theorem real.continuous_at_log
modified theorem real.continuous_log'
deleted theorem real.continuous_log
added theorem real.continuous_on_log
added theorem real.deriv_log'
added theorem real.deriv_log
deleted theorem real.exists_exp_eq_of_pos
added theorem real.log_of_ne_zero
added theorem real.log_of_pos
added theorem real.map_exp_at_bot
added theorem real.map_exp_at_top
modified theorem real.range_exp
added theorem real.surj_on_log'
added theorem real.surj_on_log
deleted theorem real.tendsto_log_one_zero
added theorem real.exp_eq_exp
modified theorem real.exp_le_exp
modified theorem real.exp_lt_exp
modified theorem intermediate_value_univ
modified theorem intermediate_value_univ₂
modified theorem nhds_within_Ici_self_ne_bot
modified theorem nhds_within_Iic_self_ne_bot