mathlib

a8b2226c - feat(analysis/convex/specific_functions): elementary convexity proofs (#19026)

feat(analysis/convex/specific_functions): elementary convexity proofs (#19026) Give elementary proofs for the convexity of `pow`, `zpow`, `exp`, `log` and `rpow`, avoiding the second derivative test. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Shortcut.20to.20integration)