Commit 2023-03-21 06:51 4601791e

View on Github →

feat(analysis/calculus/cont_diff): formula for iterated derivative of composition with linear maps (#18592) And missing API for derivatives and iterated derivatives.

Estimated changes

Modified src/analysis/calculus/cont_diff.lean

added theorem cont_diff.fderiv_right

deleted theorem cont_diff_at.cont_diff_at_fderiv

added theorem cont_diff_at.fderiv

added theorem cont_diff_at.fderiv_right

added theorem cont_diff_iff_ftaylor_series

deleted theorem cont_diff_on_iff_ftaylor_series

added theorem continuous_linear_equiv.iterated_fderiv_within_comp_left

added theorem continuous_linear_equiv.iterated_fderiv_within_comp_right

added theorem continuous_linear_map.iterated_fderiv_comp_left

added theorem continuous_linear_map.iterated_fderiv_comp_right

added theorem continuous_linear_map.iterated_fderiv_within_comp_left

added theorem continuous_linear_map.iterated_fderiv_within_comp_right

added theorem iterated_fderiv_add_apply'

added theorem iterated_fderiv_within_add_apply'

added theorem linear_isometry.norm_iterated_fderiv_comp_left

added theorem linear_isometry.norm_iterated_fderiv_within_comp_left

added theorem linear_isometry_equiv.norm_iterated_fderiv_comp_left

added theorem linear_isometry_equiv.norm_iterated_fderiv_comp_right

added theorem linear_isometry_equiv.norm_iterated_fderiv_within_comp_left

added theorem linear_isometry_equiv.norm_iterated_fderiv_within_comp_right

modified theorem norm_iterated_fderiv_within_zero

modified theorem norm_iterated_fderiv_zero

Modified src/analysis/calculus/fderiv.lean

added theorem continuous_linear_equiv.comp_right_differentiable_at_iff

added theorem continuous_linear_equiv.comp_right_differentiable_iff

added theorem continuous_linear_equiv.comp_right_differentiable_on_iff

added theorem continuous_linear_equiv.comp_right_differentiable_within_at_iff

added theorem continuous_linear_equiv.comp_right_fderiv

added theorem continuous_linear_equiv.comp_right_fderiv_within

added theorem continuous_linear_equiv.comp_right_has_fderiv_at_iff'

added theorem continuous_linear_equiv.comp_right_has_fderiv_at_iff

added theorem continuous_linear_equiv.comp_right_has_fderiv_within_at_iff'

added theorem continuous_linear_equiv.comp_right_has_fderiv_within_at_iff

added theorem continuous_linear_map.fderiv_of_bilinear

added theorem continuous_linear_map.fderiv_within_of_bilinear

added theorem continuous_linear_map.has_fderiv_at_of_bilinear

added theorem continuous_linear_map.has_fderiv_within_at_of_bilinear

added theorem fderiv_within_congr'

Modified src/analysis/normed_space/linear_isometry.lean

added def linear_isometry_equiv.ulift

Modified src/analysis/normed_space/multilinear.lean

added def continuous_linear_equiv.comp_continuous_multilinear_mapL

added theorem continuous_linear_equiv.comp_continuous_multilinear_mapL_apply

added theorem continuous_linear_equiv.comp_continuous_multilinear_mapL_symm

modified theorem continuous_multilinear_map.comp_continuous_linear_mapL_apply

added def continuous_multilinear_map.comp_continuous_linear_map_equivL

added theorem continuous_multilinear_map.comp_continuous_linear_map_equivL_apply

added theorem continuous_multilinear_map.comp_continuous_linear_map_equivL_symm

added theorem continuous_multilinear_map.norm_comp_continuous_linear_isometry_equiv

added theorem continuous_multilinear_map.norm_comp_continuous_linear_isometry_le

added theorem linear_isometry.norm_comp_continuous_multilinear_map

Modified src/analysis/normed_space/operator_norm.lean

added theorem continuous_linear_map.norm_compL_le

added theorem continuous_linear_map.norm_compSL_le

added theorem continuous_linear_map.norm_precompL_le

added theorem continuous_linear_map.norm_precompR_le

Modified src/topology/algebra/module/multilinear.lean