Commit 2024-11-28 15:29 9c17b7f9

View on Github →

feat: manifold derivative of operations in vector spaces (#18849) We have a comprehensive API for higher smoothness in the manifold sense of functions on vector spaces. We copy this API to deal with manifold differentiability.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

added theorem Differentiable.comp_mdifferentiable

added theorem Differentiable.comp_mdifferentiableAt

added theorem Differentiable.comp_mdifferentiableWithinAt

added theorem DifferentiableAt.comp_mdifferentiableAt

added theorem DifferentiableAt.comp_mdifferentiableWithinAt

added theorem DifferentiableWithinAt.comp_mdifferentiableWithinAt

added theorem MDifferentiable.cle_arrowCongr

added theorem MDifferentiable.clm_apply

added theorem MDifferentiable.clm_comp

added theorem MDifferentiable.clm_postcomp

added theorem MDifferentiable.clm_precomp

added theorem MDifferentiable.clm_prodMap

added theorem MDifferentiable.smul

added theorem MDifferentiableAt.cle_arrowCongr

added theorem MDifferentiableAt.clm_apply

added theorem MDifferentiableAt.clm_comp

added theorem MDifferentiableAt.clm_postcomp

added theorem MDifferentiableAt.smul

added theorem MDifferentiableOn.cle_arrowCongr

added theorem MDifferentiableOn.clm_apply

added theorem MDifferentiableOn.clm_comp

added theorem MDifferentiableOn.clm_precomp

added theorem MDifferentiableOn.clm_prodMap

added theorem MDifferentiableOn.smul

added theorem MDifferentiableWithinAt.cle_arrowCongr

added theorem MDifferentiableWithinAt.clm_apply

added theorem MDifferentiableWithinAt.clm_comp

added theorem MDifferentiableWithinAt.clm_postcomp

added theorem MDifferentiableWithinAt.clm_precomp

added theorem MDifferentiableWithinAt.clm_prodMap

added theorem MDifferentiableWithinAt.smul