Documentation

Verification.PowerPerspective

← Mathematical handbook
theorem Verification.concave_power_perspective {f : ℝ → ℝ} (hf : ConcaveOn ℝ (Set.Icc 0 1) f) (hf0 : f 0 = 0) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1) :
ConcaveOn ℝ (Set.Icc 0 1) fun (x : ℝ) => x ^ r * f (x ^ (1 - r))

A grounded concave function remains concave under the power-perspective transform.