lt_on_open_segment' — Mathlib

English

A strictly concave function on an open segment is strictly greater than the minimum of its endpoint values on any interior point.

Русский

Строго увклонная функция на открытом отрезке больше минимума значений концов на любой внутренней точке.

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

/-- A strictly concave function on an open segment is strictly lower-bounded by the min of its
endpoints. -/
theorem lt_on_open_segment' (hf : StrictConcaveOn 𝕜 s f) {x y : E} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) {a b : 𝕜}
    (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : min (f x) (f y) < f (a • x + b • y) :=
  hf.dual.lt_on_open_segment' hx hy hxy ha hb hab

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