[Merged by Bors] - feat: re-port #4738, with porting note for leanprover/lean4#2220#4746

Closed

Parcly-Taxel wants to merge 4 commits intomasterfrom port/Analysis.Convex.SpecificFunctions.Deriv-again

+6-13