concaveOn — Mathlib

English

If a function f is strictly concave on a set S, then f is concave on S.

Русский

Если функция f строго вогнутая на множестве S, то она вогнутая на S.

LaTeX

$$$\forall x,y\in s\;\forall 0<\lambda<1:\ f(\lambda x+(1-\lambda) y) < \lambda f(x)+(1-\lambda) f(y) \Rightarrow \forall x,y\in s\;\forall 0\le\lambda\le 1:\ f(\lambda x+(1-\lambda) y) \le \lambda f(x)+(1-\lambda) f(y)$$

Lean4

theorem concaveOn {s : Set E} {f : E → β} (hf : StrictConcaveOn 𝕜 s f) : ConcaveOn 𝕜 s f :=
  hf.dual.convexOn

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