mathlib

cf8b46d7 - feat(analysis/convex/special_functions): `sqrt * log` is strictly convex on x>1 (#14822)

feat(analysis/convex/special_functions): `sqrt * log` is strictly convex on x>1 (#14822) This convexity result can be used to golf the proof of the main inequality in the proof of Bertrand's postulate (#8002).