Commit 2024-02-05 10:10 eedf69c9

View on Github →

feat: fderiv of ContinuousMultilinearMap applied to const; use for SchwartzMap.iteratedPDeriv (#9576) add ContinuousMultilinearMap.apply; use for fderiv, iteratedFDeriv, SchwartzMap.iteratedPDeriv Defining ContinuousMultilinearMap.apply as a CLM (using existing proof of continuity) enables the proof that the application of a ContinuousMultilinearMap to a constant commutes with differentiation. This closes a todo in Mathlib/Analysis/Distribution/SchwartzSpace.lean.

Estimated changes

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

added theorem iteratedFDerivWithin_clm_apply_const_apply

added theorem iteratedFDeriv_clm_apply_const_apply

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

added theorem Differentiable.continuousMultilinear_apply_const

added theorem DifferentiableAt.continuousMultilinear_apply_const

added theorem DifferentiableOn.continuousMultilinear_apply_const

added theorem DifferentiableWithinAt.continuousMultilinear_apply_const

added theorem HasFDerivAt.continuousMultilinear_apply_const

added theorem HasFDerivWithinAt.continuousMultilinear_apply_const

added theorem HasStrictFDerivAt.continuousMultilinear_apply_const

added theorem fderivWithin_continuousMultilinear_apply_const

added theorem fderivWithin_continuousMultilinear_apply_const_apply

added theorem fderiv_continuousMultilinear_apply_const

added theorem fderiv_continuousMultilinear_apply_const_apply

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem SchwartzMap.iteratedPDeriv_eq_iteratedFDeriv

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

added def ContinuousMultilinearMap.apply

added theorem ContinuousMultilinearMap.apply_apply