English
If f is convex on a set s, then for any x,y in s and any nonnegative a,b with a+b=1, the value at an internal point of the segment is bounded above by the maximum of the endpoints.
Русский
Если f выпукла на s, то для любых x,y в s и любых a,b ≥ 0 с a+b=1, значение на любой точке отрезка между x и y не превышает максимум между f(x) и f(y).
LaTeX
$$$\ConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s,\forall a,b\in \mathfrak{K}_{+},\ a+b=1:\ f(a\,x+b\,y) \le \max\{f(x), f(y)\}$$$
Lean4
/-- A convex function on a segment is upper-bounded by the max of its endpoints. -/
theorem le_on_segment' (hf : ConvexOn 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 ≤ b)
(hab : a + b = 1) : f (a • x + b • y) ≤ max (f x) (f y) :=
calc
f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha hb hab
_ ≤ a • max (f x) (f y) + b • max (f x) (f y) := by
gcongr
· apply le_max_left
· apply le_max_right
_ = max (f x) (f y) := Convex.combo_self hab _
