left_lt_of_lt_right' — Mathlib

English

On an open segment, a strictly concave function is strictly greater than the endpoint minimum at 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 left_lt_of_lt_right' (hf : ConcaveOn 𝕜 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 (a • x + b • y) < f y) : f x < f (a • x + b • y) :=
  hf.dual.lt_left_of_right_lt' hx hy ha hb hab hfy

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