x^3 is convex on positive

Stream: new members

[Li Xuanji]

I want to show that the function $x \mapsto x^3$ is convex on $(0, ∞)$, which seems tailor-made for convexOn_zpow, but I can't get the apply to work.

import Mathlib

example : ConvexOn ℝ (Set.Ioi (0: ℝ)) (fun x => x ^ 3) := by
  apply convexOn_zpow

error:

tactic 'apply' failed, failed to unify
  ConvexOn ?𝕜 (Set.Ioi 0) fun x => x ^ ?n
with
  ConvexOn ℝ (Set.Ioi 0) fun x => x ^ 3

Not sure what the issue is, since it looks like ?𝕜=ℝ, ?n=3 should work.

[Li Xuanji]

Oh, it looks like I need the 3 to be integer...

example : ConvexOn ℝ (Set.Ioi (0: ℝ)) (fun x => x ^ (3: ℤ)) := by
    apply convexOn_zpow

[Ruben Van de Velde]

Indeed, that's what the "z" in "zpow" means. There's also convexOn_pow which is even slightly stronger