lt_right_of_left_lt' — Mathlib

English

On an open segment, a strictly convex function satisfies strict inequality against endpoints on 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 lt_right_of_left_lt' (hf : ConvexOn 𝕜 s f) {x y : E} {a b : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (ha : 0 < a)
    (hb : 0 < b) (hab : a + b = 1) (hfx : f x < f (a • x + b • y)) : f (a • x + b • y) < f y :=
  by
  rw [add_comm] at hab hfx ⊢
  exact hf.lt_left_of_right_lt' hy hx hb ha hab hfx

Похожие утверждения