English
Let S be a convex subset of E and f: E → β. f is strictly concave on S if S is convex and for all x ≠ y in S and a,b > 0 with a + b = 1, we have f(a x + b y) > a f(x) + b f(y).
Русский
Пусть S выпукло. Тогда f строго конкавна на S, если для любых x ≠ y в S и любых a,b > 0 с a + b = 1 выполняется f(a x + b y) > a f(x) + b f(y).
LaTeX
$$$$ \\operatorname{StrictConcaveOn}_{\\mathsf{𝕜}}(S,f) \\;:\\\\iff\\\\; \\operatorname{Convex}_{\\mathsf{𝕜}}(S) \\land \\forall x,y\\in S, x \\neq y, \\forall a,b\\in 𝕜, 0 < a, 0 < b, a+b=1 \\Rightarrow a\\,f(x) + b\\,f(y) < f(a\\,x + b\\,y). $$$$
Lean4
/-- Strict concavity of functions -/
def StrictConcaveOn : Prop :=
Convex 𝕜 s ∧
∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • f x + b • f y < f (a • x + b • y)
