Commit 2023-06-17 15:50 e93039b7
View on Github →feat: prove concavity of x ↦ x^p for p ∈ (0,1) (#4916)
This PR prove the (strict) concavity of x ↦ x^p for p between 0 and 1.
The main results are in a new file to avoid adding dependencies to Analysis.Convex.SpecificFunctions.Basic which is carefully designed to be low in the import hierarchy.