Commit 2023-06-02 11:07 cdbd878a

View on Github →

feat: port Analysis.Calculus.Taylor (#4582)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Taylor.lean

added theorem continuousOn_taylorWithinEval

added theorem exists_taylor_mean_remainder_bound

added theorem hasDerivWithinAt_taylorWithinEval

added theorem hasDerivWithinAt_taylor_coeff_within

added theorem has_deriv_within_taylorWithinEval_at_Icc

added theorem monomial_has_deriv_aux

added theorem taylorWithinEval_hasDerivAt_Ioo

added theorem taylorWithinEval_self

added theorem taylorWithinEval_succ

added theorem taylorWithin_succ

added theorem taylor_mean_remainder

added theorem taylor_mean_remainder_bound

added theorem taylor_mean_remainder_cauchy

added theorem taylor_mean_remainder_lagrange

added theorem taylor_within_apply

added theorem taylor_within_zero_eval