English
On an open segment, a strictly convex function is strictly less than the maximum of endpoint values at interior points.
Русский
На открытом отрезке строго выпуклая функция на внутренних точках строго меньше максимума значений концов.
LaTeX
$$$\StrictConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, x\neq y, z\in openSegment(\mathfrak{K}, x, y): f(z) < \max\{f(x), f(y)\}$$$
Lean4
theorem le_left_of_right_le' (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) (hfy : f y ≤ f (a • x + b • y)) : f (a • x + b • y) ≤ f x :=
le_of_not_gt fun h ↦
lt_irrefl (f (a • x + b • y)) <|
calc
f (a • x + b • y) ≤ a • f x + b • f y := hf.2 hx hy ha.le hb hab
_ < a • f (a • x + b • y) + b • f (a • x + b • y) :=
(add_lt_add_of_lt_of_le (smul_lt_smul_of_pos_left h ha) (smul_le_smul_of_nonneg_left hfy hb))
_ = f (a • x + b • y) := Convex.combo_self hab _
