← Mathematical handbook

theorem Verification.hasDerivAt_positivePart_rpow {p : ℝ} (hp : 1 < p) (x : ℝ) : HasDerivAt (fun (y : ℝ) => max 0 y ^ p) (p * max 0 x ^ (p - 1)) x