mathlib

abffbaa3 - feat(analysis/convex/specific_functions): log is concave (#5508)

feat(analysis/convex/specific_functions): log is concave (#5508) This PR proves that the real log is concave on `Ioi 0` and `Iio 0`, and adds lemmas about concavity of functions along the way. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>