Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-10 17:42
9afedb2c
View on Github →
feat(Analysis/Calculus): norm bound for iterated derivatives of composition with CLM (
#32572
)
Estimated changes
Modified
Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
added
theorem
ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left
added
theorem
ContinuousLinearMap.norm_iteratedFDeriv_comp_left