Commit 2023-06-01 10:18 eaa69ef7

View on Github →

feat: port Analysis.Calculus.IteratedDeriv (#4545)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/IteratedDeriv.lean

added theorem ContDiff.continuous_iteratedDeriv

added theorem ContDiff.differentiable_iteratedDeriv

added theorem ContDiffOn.continuousOn_iteratedDerivWithin

added theorem ContDiffOn.differentiableOn_iteratedDerivWithin

added theorem ContDiffWithinAt.differentiableWithinAt_iteratedDerivWithin

added theorem contDiffOn_iff_continuousOn_differentiableOn_deriv

added theorem contDiffOn_of_continuousOn_differentiableOn_deriv

added theorem contDiffOn_of_differentiableOn_deriv

added theorem contDiff_iff_iteratedDeriv

added theorem contDiff_of_differentiable_iteratedDeriv

added def iteratedDeriv

added def iteratedDerivWithin

added theorem iteratedDerivWithin_eq_equiv_comp

added theorem iteratedDerivWithin_eq_iterate

added theorem iteratedDerivWithin_eq_iteratedFDerivWithin

added theorem iteratedDerivWithin_one

added theorem iteratedDerivWithin_succ'

added theorem iteratedDerivWithin_succ

added theorem iteratedDerivWithin_univ

added theorem iteratedDerivWithin_zero

added theorem iteratedDeriv_eq_equiv_comp

added theorem iteratedDeriv_eq_iterate

added theorem iteratedDeriv_eq_iteratedFDeriv

added theorem iteratedDeriv_one

added theorem iteratedDeriv_succ'

added theorem iteratedDeriv_succ

added theorem iteratedDeriv_zero

added theorem iteratedFDerivWithin_apply_eq_iteratedDerivWithin_mul_prod

added theorem iteratedFDerivWithin_eq_equiv_comp

added theorem iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod

added theorem iteratedFDeriv_eq_equiv_comp

added theorem norm_iteratedFDerivWithin_eq_norm_iteratedDerivWithin

added theorem norm_iteratedFDeriv_eq_norm_iteratedDeriv