refactor(analysis/convex/specific_functions): split (#19031)
Split `analysis/convex/specific_function` into a part which doesn't require differentiation (as of #19026) and a part which does. This removes the dependence of `measure_theory/integral/bochner` on differentiation, and decreases by 11 the length of the longest path in mathlib.
See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Shortcut.20to.20integration)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
