Commit 2021-09-23 22:18 c950c45e

View on Github →

feat(analysis/calculus/[f]deriv): derivative of pointwise composition/application of continuous linear maps (#9174) This introduces useful analogs to the product rule when working with derivatives in spaces of continuous linear maps.

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem deriv_clm_apply

added theorem deriv_clm_comp

added theorem deriv_within_clm_apply

added theorem deriv_within_clm_comp

added theorem has_deriv_at.clm_apply

added theorem has_deriv_at.clm_comp

added theorem has_deriv_within_at.clm_apply

added theorem has_deriv_within_at.clm_comp

added theorem has_strict_deriv_at.clm_apply

added theorem has_strict_deriv_at.clm_comp

Modified src/analysis/calculus/fderiv.lean

added theorem differentiable.clm_apply

added theorem differentiable.clm_comp

added theorem differentiable_at.clm_apply

added theorem differentiable_at.clm_comp

added theorem differentiable_on.clm_apply

added theorem differentiable_on.clm_comp

added theorem differentiable_within_at.clm_apply

added theorem differentiable_within_at.clm_comp

added theorem fderiv_clm_apply

added theorem fderiv_clm_comp

added theorem fderiv_within_clm_apply

added theorem fderiv_within_clm_comp

added theorem has_fderiv_at.clm_apply

added theorem has_fderiv_at.clm_comp

added theorem has_fderiv_within_at.clm_apply

added theorem has_fderiv_within_at.clm_comp

added theorem has_strict_fderiv_at.clm_apply

added theorem has_strict_fderiv_at.clm_comp

Modified src/topology/algebra/module.lean

added theorem continuous_linear_map.comp_apply