English
A strictly convex function on an open segment is strictly less than the maximum of its endpoint values on any interior point.
Русский
Строго выпуклая функция на открытом отрезке принимает значения строго меньшие максимума значений концов на любой внутренней точке.
LaTeX
$$$\StrictConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, x\neq y, a,b>0:\ f(a x + b y) < \max\{f(x), f(y)\}$$$
Lean4
/-- A strictly convex function on an open segment is strictly upper-bounded by the max of its
endpoints. -/
theorem lt_on_open_segment' (hf : StrictConvexOn 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {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 hxy 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 _
