Commit 2024-12-10 06:48 78302698

View on Github →

feat: more API for iteratedFDeriv (#19769) Notably, iteratedFDeriv commutes with composition with a translation

Estimated changes

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

added theorem FormalMultilinearSeries.derivSeries_eq_zero

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

modified theorem contDiff_prodAssoc

modified theorem contDiff_prodAssoc_symm

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

added theorem ContDiff.ftaylorSeries

added theorem iteratedFDerivWithin_eq_iteratedFDeriv

added theorem iteratedFDerivWithin_subset

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

added theorem iteratedFDerivWithin_comp_add_left'

added theorem iteratedFDerivWithin_comp_add_left

added theorem iteratedFDerivWithin_comp_add_right'

added theorem iteratedFDerivWithin_comp_add_right

added theorem iteratedFDerivWithin_comp_sub'

added theorem iteratedFDerivWithin_comp_sub

added theorem iteratedFDerivWithin_two_apply'

added theorem iteratedFDeriv_comp_add_left'

added theorem iteratedFDeriv_comp_add_left

added theorem iteratedFDeriv_comp_add_right'

added theorem iteratedFDeriv_comp_add_right

added theorem iteratedFDeriv_comp_sub'

added theorem iteratedFDeriv_comp_sub

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

added theorem differentiableAt_comp_add_left

added theorem differentiableAt_comp_add_right

added theorem differentiableAt_comp_sub

added theorem differentiableWithinAt_comp_add_left

added theorem differentiableWithinAt_comp_add_right

added theorem differentiableWithinAt_comp_sub

added theorem fderivWithin_comp_add_left

added theorem fderivWithin_comp_add_right

added theorem fderivWithin_comp_sub

added theorem fderiv_comp_add_left

added theorem fderiv_comp_add_right

added theorem fderiv_comp_sub

added theorem hasFDerivAt_comp_add_left

added theorem hasFDerivAt_comp_add_right

added theorem hasFDerivAt_comp_sub

added theorem hasFDerivWithinAt_comp_add_left

added theorem hasFDerivWithinAt_comp_add_right

added theorem hasFDerivWithinAt_comp_sub

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

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

added theorem FormalMultilinearSeries.add_apply

added theorem FormalMultilinearSeries.congr_zero

added theorem FormalMultilinearSeries.sub_apply

Modified Mathlib/Data/Fintype/Card.lean

deleted theorem Function.Embedding.equiv_of_fintype_self_embedding_to_embedding

added theorem Function.Embedding.toEmbedding_equivOfFiniteSelfEmbedding

Modified Mathlib/Topology/Homeomorph.lean

added theorem Homeomorph.image_eq_preimage