Commit 2024-01-19 09:25 77a16874

View on Github →

feat: add lemmas about iteratedDerivWithin (#9679) Mostly based on @CBirkbeck's work on modular forms.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Analysis/Calculus/IteratedDeriv.lean to Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

Created Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean

added theorem iteratedDerivWithin_add

added theorem iteratedDerivWithin_congr

added theorem iteratedDerivWithin_const_add

added theorem iteratedDerivWithin_const_mul

added theorem iteratedDerivWithin_const_neg

added theorem iteratedDerivWithin_const_smul

added theorem iteratedDerivWithin_neg'

added theorem iteratedDerivWithin_neg

added theorem iteratedDerivWithin_sub

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean