Commit 2026-04-23 19:18 f96c7aca

feat(Analysis/Calculus/IteratedDeriv): add affine composition lemmas (#36357) This PR adds composition lemmas for iteratedDerivWithin and iteratedFDerivWithin on maps 𝕜 → F, covering x ↦ f (-x), x ↦ f (c + x), x ↦ f (x + c), x ↦ f (x - c), and x ↦ f (c - x). To support these statements, it also adds one-dimensional fderivWithin lemmas that do not require a UniqueDiffWithinAt hypothesis:

• fderivWithin_zero_of_not_uniqueDiffWithinAt
• fderivWithin_const_smul_field'
• fderivWithin_neg'
• fderivWithin_comp_neg Finally, it rewrites iteratedDeriv_comp_neg to follow from the new Fréchet-derivative lemmas, and shortens two proofs in ContDiff/FTaylorSeries by replacing hand-written arguments with existing general lemmas.