strictConcaveOn_sqrt — Mathlib

English

The square root function is strictly concave on the nonnegative real axis. In particular, for all x, y ≥ 0 and all α with 0 < α < 1, sqrt(α x + (1 − α) y) > α sqrt(x) + (1 − α) sqrt(y).

Русский

Функция квадратного корня на неотрицательных вещественных числах строго вогнута. То есть для всех x, y ≥ 0 и 0 < α < 1 выполняется sqrt(α x + (1 − α) y) > α sqrt(x) + (1 − α) sqrt(y).

LaTeX

$$$$\forall x,y \ge 0,\ 0<\alpha<1:\ \sqrt{\alpha x+(1-\alpha)y} > \alpha\sqrt{x} + (1-\alpha)\sqrt{y}.$$$$

Lean4

theorem strictConcaveOn_sqrt : StrictConcaveOn ℝ (Set.Ici 0) (√· : ℝ → ℝ) :=
  by
  rw [funext Real.sqrt_eq_rpow]
  exact strictConcaveOn_rpow (by positivity) (by linarith)

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