English
For 0 < p < 1, the function x ↦ x^p is strictly concave on NNReal Set.univ.
Русский
Для 0 < p < 1 функция x^p строго вогнута на NNReal.
LaTeX
$$∀ {p : Real}, p ∈ (0,1) ⇒ StrictConcaveOn NNReal Set.univ (x^p)$$
Lean4
theorem strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : StrictConcaveOn ℝ≥0 univ fun x : ℝ≥0 ↦ x ^ p :=
by
have hp₀' : 0 < 1 / p := div_pos zero_lt_one hp₀
have hp₁' : 1 < 1 / p := by rw [one_lt_div hp₀]; exact hp₁
let f := NNReal.orderIsoRpow (1 / p) hp₀'
have h₁ : StrictConvexOn ℝ≥0 univ f :=
by
refine ⟨convex_univ, fun x _ y _ hxy a b ha hb hab => ?_⟩
exact (strictConvexOn_rpow hp₁').2 x.2 y.2 (by simp [hxy]) ha hb (by simp; norm_cast)
have h₂ : ∀ x, f.symm x = x ^ p := by simp [f, NNReal.orderIsoRpow_symm_eq]
refine ⟨convex_univ, fun x mx y my hxy a b ha hb hab => ?_⟩
simp only [← h₂]
exact (f.strictConcaveOn_symm h₁).2 mx my hxy ha hb hab
