English
For any integer n, x ↦ x^n is convex on the positive real axis (0, ∞) when 𝕜 is a field and the order is strict.
Русский
Для любого целого n функция x ↦ x^n выпукла на $(0, ∞)$ при рабочем окружении поля и строгого порядка.
LaTeX
$$$\forall n \in \mathbb{Z},\; \text{ConvexOn} \ 𝕜 \ (\mathrm{Ioi}\,0)\ (\lambda x. x^n).$$$
Lean4
/-- `x^m`, `m : ℤ` is convex on `(0, +∞)` for all `m`. -/
theorem convexOn_zpow : ∀ n : ℤ, ConvexOn 𝕜 (Ioi 0) fun x : 𝕜 ↦ x ^ n
| (n : ℕ) => by
simp_rw [zpow_natCast]
exact (convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)
| -[n+1] => by
simp_rw [zpow_negSucc, ← inv_pow]
refine (convexOn_iff_forall_pos.2 ⟨convex_Ioi _, ?_⟩).pow (fun x (hx : 0 < x) ↦ by positivity) _
rintro x (hx : 0 < x) y (hy : 0 < y) a b ha hb hab
simp only [smul_eq_mul]
field_simp
have H : 0 ≤ a * b * (x - y) ^ 2 := by positivity
linear_combination H - x * y * (a + b + 1) * hab
