Theorems · Theorem · real analysis

strictConvexOn_rpow

∀ {p : ℝ}, 1 < p → StrictConvexOn ℝ (Set.Ici 0) fun x => x ^ p

For p : ℝ with 1 < p, fun x ↦ x ^ p is strictly convex on $[0, +∞)$.

Defined in

Mathlib.Analysis.Convex.SpecificFunctions.Basic

Cited by

2 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound