Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-03 05:29 e0030149

View on Github →

feat(analysis/calculus/iterated_deriv): iterated derivative of a function defined on the base field (#2067)

iterated deriv
cleanup
fix docstring
add iterated_deriv_within_succ'
remove n.succ
n+1 -> n + 1

Estimated changes

Created src/analysis/calculus/iterated_deriv.lean

added def iterated_deriv

added theorem iterated_deriv_eq_equiv_comp

added theorem iterated_deriv_eq_iterate

added theorem iterated_deriv_eq_iterated_fderiv

added theorem iterated_deriv_one

added theorem iterated_deriv_succ'

added theorem iterated_deriv_succ

added def iterated_deriv_within

added theorem iterated_deriv_within_eq_equiv_comp

added theorem iterated_deriv_within_eq_iterate

added theorem iterated_deriv_within_eq_iterated_fderiv_within

added theorem iterated_deriv_within_one

added theorem iterated_deriv_within_succ'

added theorem iterated_deriv_within_succ

added theorem iterated_deriv_within_univ

added theorem iterated_deriv_within_zero

added theorem iterated_deriv_zero

added theorem iterated_fderiv_apply_eq_iterated_deriv_mul_prod

added theorem iterated_fderiv_eq_equiv_comp

added theorem iterated_fderiv_within_apply_eq_iterated_deriv_within_mul_prod

added theorem iterated_fderiv_within_eq_equiv_comp

added theorem times_cont_diff.continuous_iterated_deriv

added theorem times_cont_diff.differentiable_iterated_deriv

added theorem times_cont_diff_iff_iterated_deriv

added theorem times_cont_diff_of_differentiable_iterated_deriv

added theorem times_cont_diff_on.continuous_on_iterated_deriv_within

added theorem times_cont_diff_on.differentiable_on_iterated_deriv_within

added theorem times_cont_diff_on_iff_continuous_on_differentiable_on_deriv

added theorem times_cont_diff_on_of_continuous_on_differentiable_on_deriv

added theorem times_cont_diff_on_of_differentiable_on_deriv

Modified src/analysis/calculus/times_cont_diff.lean

modified theorem iterated_fderiv_succ_apply_left

modified theorem iterated_fderiv_succ_apply_right

modified theorem iterated_fderiv_within_succ_apply_left