mathlib
66dea297 - feat(analysis/convex/specific_functions): Strict convexity of `exp`, `log` and `pow` (#10123)

Commit
4 years ago
feat(analysis/convex/specific_functions): Strict convexity of `exp`, `log` and `pow` (#10123) This strictifies the results of convexity/concavity of `exp`/`log` and add the strict versions for `pow`, `zpow`, `rpow`. I'm also renaming `convex_on_pow_of_even` to `even.convex_on_pow` for dot notation.
Author
Parents
Loading