lt_right_of_left_lt' — Mathlib

English

On an open segment, a strictly concave function satisfies a strict inequality against the endpoints on interior points.

Русский

На открытом отрезке строго увклонная функция удовлетворяет строгому неравенству по концам на внутренних точках.

LaTeX

$$$\StrictConcaveOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, x\neq y, a,b>0:\ f(a x + b y) > \min\{f(x), f(y)\}$$$

Lean4

theorem lt_right_of_left_lt' (hf : ConcaveOn 𝕜 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 (a • x + b • y) < f x) : f y < f (a • x + b • y) :=
  hf.dual.lt_right_of_left_lt' hx hy ha hb hab hfx

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