Commit 2020-09-01 12:58 329393a7

View on Github →

feat(analysis/calculus/times_cont_diff): iterated smoothness in terms of deriv (#4017) Currently, iterated smoothness is only formulated in terms of the Fréchet derivative. For one-dimensional functions, it is more handy to use the one-dimensional derivative deriv. This PR provides a basic interface in this direction.

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem deriv_within_of_open

Modified src/analysis/calculus/fderiv.lean

added theorem fderiv_within_of_open

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff_on.continuous_on_deriv_of_open

added theorem times_cont_diff_on.continuous_on_deriv_within

added theorem times_cont_diff_on.continuous_on_fderiv_of_open

added theorem times_cont_diff_on.deriv_of_open

added theorem times_cont_diff_on.deriv_within

added theorem times_cont_diff_on.fderiv_of_open

added theorem times_cont_diff_on_succ_iff_deriv_of_open

added theorem times_cont_diff_on_succ_iff_deriv_within

added theorem times_cont_diff_on_succ_iff_fderiv_of_open

added theorem times_cont_diff_on_top_iff_deriv_of_open

added theorem times_cont_diff_on_top_iff_deriv_within

added theorem times_cont_diff_on_top_iff_fderiv_of_open