Commit 2026-03-31 21:25 20848cd3

View on Github →

feat(Calculus): Taylor with integral remainder (#34871) This PR proves Taylor's theorem with the integral remainder. It provides two versions:

  1. based on $f^{(n)}$ is absolutely continuous
  2. based on $f \in C^{(n+1)}$ It also weakens the hypotheses (hx : x₀ < x) to (hx : x₀ ≠ x) in the following theorems:
  • taylor_mean_remainder
  • taylor_mean_remainder_lagrange
  • taylor_mean_remainder_lagrange_iteratedDeriv
  • taylor_mean_remainder_cauchy

Estimated changes

modified theorem iteratedDerivWithin_succ'
modified theorem iteratedDerivWithin_succ
modified theorem taylor_mean_remainder