Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-25 19:59 e1a18cad

View on Github →

feat(analysis/special_functions/exponential): derivative of u ↦ exp 𝕂 (u • x) (#19062) Revived from an old branch of @ADedecker, golfed using new lemmas that I added in the meantime.

Estimated changes

Modified src/analysis/special_functions/exponential.lean

added theorem has_deriv_at_exp_smul_const'

added theorem has_deriv_at_exp_smul_const

added theorem has_deriv_at_exp_smul_const_of_mem_ball'

added theorem has_deriv_at_exp_smul_const_of_mem_ball

added theorem has_fderiv_at_exp_smul_const'

added theorem has_fderiv_at_exp_smul_const

added theorem has_fderiv_at_exp_smul_const_of_mem_ball'

added theorem has_fderiv_at_exp_smul_const_of_mem_ball

added theorem has_strict_deriv_at_exp_smul_const'

added theorem has_strict_deriv_at_exp_smul_const

added theorem has_strict_deriv_at_exp_smul_const_of_mem_ball'

added theorem has_strict_deriv_at_exp_smul_const_of_mem_ball

added theorem has_strict_fderiv_at_exp_smul_const'

added theorem has_strict_fderiv_at_exp_smul_const

added theorem has_strict_fderiv_at_exp_smul_const_of_mem_ball'

added theorem has_strict_fderiv_at_exp_smul_const_of_mem_ball