English
On an open segment, a strictly convex function is strictly less than the endpoint maximum at interior points.
Русский
На открытом сегменте строго выпуклая функция строго меньше максимума концов на внутренних точках.
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
theorem lt_left_of_right_lt' (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 :=
not_le.1 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.le hab
_ < a • f (a • x + b • y) + b • f (a • x + b • y) :=
(add_lt_add_of_le_of_lt (smul_le_smul_of_nonneg_left h ha.le) (smul_lt_smul_of_pos_left hfy hb))
_ = f (a • x + b • y) := Convex.combo_self hab _
