strictConcaveOn_sqrt — Mathlib

English

The square root on NNReal is strictly concave: NNReal.sqrt is strictly concave on Set.univ.

Русский

Квадратный корень на NNReal строго вогнут: NNReal.sqrt строго вогнута на Set.univ.

LaTeX

$$StrictConcaveOn NNReal Set.univ NNReal.sqrt$$

Lean4

theorem strictConcaveOn_sqrt : StrictConcaveOn ℝ≥0 univ NNReal.sqrt :=
  by
  have : NNReal.sqrt = fun x : ℝ≥0 ↦ x ^ (1 / (2 : ℝ)) := by ext x; exact mod_cast NNReal.sqrt_eq_rpow x
  rw [this]
  exact strictConcaveOn_rpow (by positivity) (by linarith)

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