Commit 2025-01-07 19:44 576077ae

View on Github →

feat(ContDiff): weaken some assumptions (#20368) Assume ContDiffWithinAt/ContDiffAt instead of ContDiffOn/ContDiff.

Estimated changes

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

modified theorem iteratedFDerivWithin_const_smul_apply

modified theorem iteratedFDeriv_const_smul_apply'

modified theorem iteratedFDeriv_const_smul_apply

Modified Mathlib/Analysis/Calculus/ContDiff/Bounds.lean

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

modified theorem iteratedDerivWithin_const_mul

modified theorem iteratedDerivWithin_const_smul

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean