English
For integer m with m ≠ 0 and m ≠ 1, the map x ↦ x^m is strictly convex on (0, ∞).
Русский
Для целого m, m ≠ 0, m ≠ 1, отображение x^m строго выпукло на (0, ∞).
LaTeX
$$(m ∈ ℤ) ∧ (m ≠ 0) ∧ (m ≠ 1) ⇒ StrictConvexOn ℝ (Ioi 0) (fun x => x^m)$$
Lean4
/-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m` except `0` and `1`. -/
theorem strictConvexOn_zpow {m : ℤ} (hm₀ : m ≠ 0) (hm₁ : m ≠ 1) : StrictConvexOn ℝ (Ioi 0) fun x : ℝ => x ^ m :=
by
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
· exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx
intro x hx
rw [mem_Ioi] at hx
rw [iter_deriv_zpow]
refine mul_pos ?_ (zpow_pos hx _)
norm_cast
refine int_prod_range_pos (by decide) fun hm => ?_
rw [← Finset.coe_Ico] at hm
norm_cast at hm
fin_cases hm <;> simp_all
