concaveOn_rpow — Mathlib

English

For 0 ≤ p ≤ 1, the function x ↦ x^p is concave on [0, ∞).

Русский

Для 0 ≤ p ≤ 1 функция x^p конкавна на [0, ∞).

LaTeX

$$ConcaveOn Real (Set.Ici 0) (fun x => x^p)$$

Lean4

theorem concaveOn_rpow {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : ConcaveOn ℝ (Set.Ici 0) fun x : ℝ ↦ x ^ p :=
  by
  rcases eq_or_lt_of_le hp₀ with (rfl | hp₀)
  · simpa only [rpow_zero] using concaveOn_const (c := 1) (convex_Ici _)
  rcases eq_or_lt_of_le hp₁ with (rfl | hp₁)
  · simpa only [rpow_one] using concaveOn_id (convex_Ici _)
  exact (strictConcaveOn_rpow hp₀ hp₁).concaveOn

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