convexOn_Ioi_klFun — Mathlib

English

The function klFun is convex on the positive real axis (0, ∞).

Русский

Функция klFun выпукла на области (0, ∞).

LaTeX

$$$\\displaystyle \\forall a,b>0,\\; \\forall t\\in[0,1],\\; klFun((1-t)a+t b) \\le (1-t)\\,klFun(a) + t\\,klFun(b)$$$

Lean4

/-- `klFun` is convex on (0,∞).
This is an often useful consequence of `convexOn_klFun`, which states convexity on [0, ∞). -/
theorem convexOn_Ioi_klFun : ConvexOn ℝ (Ioi 0) klFun :=
  convexOn_klFun.subset (Ioi_subset_Ici le_rfl) (convex_Ioi _)

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