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