Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-23 09:03 2f516593

View on Github →

feat(analysis/special_functions/exp_log): exp is infinitely smooth (#5086)

  • Prove that complex.exp and real.exp are infinitely smooth.
  • Generalize lemmas about exp ∘ f to f : E → ℂ or f : E → ℝ instead of f : ℂ → ℂ or f : ℝ → ℝ.

Estimated changes

added theorem fderiv_exp
added theorem fderiv_within_exp
added theorem has_fderiv_at.cexp
added theorem has_fderiv_at.exp
modified theorem measurable.cexp
modified theorem measurable.exp
added theorem times_cont_diff.cexp
added theorem times_cont_diff.exp
added theorem times_cont_diff_at.exp
added theorem times_cont_diff_on.exp