convexOn_pow — Mathlib

English

For any natural exponent n ≥ 0, the function x ↦ x^n is convex on the interval (0, ∞).

Русский

Для любого натурального показателя n ≥ 0 функция x ↦ x^n выпукла на интервале (0, ∞).

LaTeX

$$$\forall n \in \mathbb{N},\; \text{ConvexOn} \ 𝕜 \ (\mathrm{Ioi}\,0)\ (\lambda x. x^n).$$$

Lean4

/-- `x^n`, `n : ℕ` is convex on `[0, +∞)` for all `n`. -/
theorem convexOn_pow : ∀ n, ConvexOn 𝕜 (Ici 0) fun x : 𝕜 ↦ x ^ n :=
  (convexOn_id <| convex_Ici _).pow fun _ ↦ id

Похожие утверждения