English
Let S be a subset of E which is convex, and let f: E → β. Then f is concave on S if S is convex and for every x, y ∈ S and every nonnegative a, b with a + b = 1, we have a f(x) + b f(y) ≤ f(a x + b y).
Русский
Пусть S ⊆ E выпуклое множество и пусть f: E → β. Тогда f конкавна на S, если S выпукло и для любых x, y ∈ S и любых a, b ≥ 0 с a + b = 1 выполняется a f(x) + b f(y) ≤ f(a x + b y).
LaTeX
$$$$ \\operatorname{ConcaveOn}_{\\mathsf{𝕜}}(S,f) \\;:\\\\iff\\\\; \\operatorname{Convex}_{\\mathsf{𝕜}}(S) \\land \\forall x\\in S\\,\\forall y\\in S\\, \\forall a,b\\in 𝕜,\, 0 \\le a, 0 \\le b, a+b=1 \\Rightarrow a\\,f(x) + b\\,f(y) \\le f(a\\,x + b\\,y). $$$$
Lean4
/-- Concavity of functions -/
def ConcaveOn : Prop :=
Convex 𝕜 s ∧
∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • f x + b • f y ≤ f (a • x + b • y)
