English
If f is strictly concave on s, then for any x,y in s and any a,b ≥ 0 with a+b=1, the value at a point on the segment is at least the minimum of the endpoint values.
Русский
Если f строго увклена на s, то на отрезке между x и y значение f на любой внутренней точке не меньше минимума значений на концах.
LaTeX
$$$\StrictConcaveOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s,\forall a,b\in \mathfrak{K}_{+},\ a+b=1:\min\{f(x),f(y)\} \le f(a\,x+b\,y)$$$
Lean4
/-- A concave function on a segment is lower-bounded by the min of its endpoints. -/
theorem ge_on_segment' (hf : ConcaveOn 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b)
(hab : a + b = 1) : min (f x) (f y) ≤ f (a • x + b • y) :=
hf.dual.le_on_segment' hx hy ha hb hab
