right_le_of_le_left' — Mathlib

English

If f is convex on s, and f(y) ≤ f(a x + b y) with a,b≥0, a+b=1, then f(a x + b y) ≤ f(x) whenever z lies on the segment between x and y.

Русский

Если f выпукла на s и f(y) ≤ f(a x + b y) с a,b≥0, a+b=1, тогда f(a x + b y) ≤ f(x) для z на отрезке между x и y.

LaTeX

$$$\ConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y \in s, a,b\ge 0, a+b=1:\ f(a x + b y) \le f(x)$ под условиями.$$

Lean4

theorem right_le_of_le_left' (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.le_right_of_left_le' hx hy ha hb hab hfx

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