strictConcaveOn_rpow — Mathlib

English

For Real p with 0 < p < 1, the function x ↦ x^p is strictly concave on [0, ∞).

Русский

Для p с 0 < p < 1 отображение x^p строго вогнуто на [0, ∞).

LaTeX

$${p ∈ ℝ | 0 < p < 1} ⇒ StrictConcaveOn Real (Set.Ici 0) (x^p)$$

Lean4

theorem strictConcaveOn_rpow {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : StrictConcaveOn ℝ (Set.Ici 0) fun x : ℝ ↦ x ^ p :=
  by
  refine ⟨convex_Ici _, fun x hx y hy hxy a b ha hb hab => ?_⟩
  let x' : ℝ≥0 := ⟨x, hx⟩
  let y' : ℝ≥0 := ⟨y, hy⟩
  let a' : ℝ≥0 := ⟨a, ha.le⟩
  let b' : ℝ≥0 := ⟨b, hb.le⟩
  have hxy' : x' ≠ y' := Subtype.coe_ne_coe.1 hxy
  have hab' : a' + b' = 1 := by ext; simp [a', b', hab]
  exact_mod_cast
    (NNReal.strictConcaveOn_rpow hp₀ hp₁).2 (Set.mem_univ x') (Set.mem_univ y') hxy' (mod_cast ha) (mod_cast hb) hab'

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