concaveOn_rpow — Mathlib

English

For 0 ≤ p ≤ 1, the function x ↦ x^p is concave on NNReal Set.univ.

Русский

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

LaTeX

$$ConcaveOn NNReal Set.univ (x^p)$$

Lean4

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

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