English
If a function is strictly convex on s, then for x<y and a,b>0 with a+b=1, the strict inequality holds for f at the convex combination.
Русский
Если функция строго выпуклая на s, то для x<y и a,b>0 с a+b=1 неравенство строгого типа выполняется для f в линейной комбинации.
LaTeX
$$$\forall x0:\ a f(x) + b f(y) > f(a x + b y)$$$
Lean4
/-- For a function on a convex set in a linearly ordered space (where the order and the algebraic
structures aren't necessarily compatible), in order to prove that it is strictly concave it suffices
to verify the inequality `a • f x + b • f y < f (a • x + b • y)` for `x < y` and positive `a`, `b`.
The main use case is `E = 𝕜` however one can apply it, e.g., to `𝕜^n` with lexicographic order. -/
theorem strictConcaveOn_of_lt (hs : Convex 𝕜 s)
(hf :
∀ ⦃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)) :
StrictConcaveOn 𝕜 s f :=
LinearOrder.strictConvexOn_of_lt (β := βᵒᵈ) hs hf
