le_right_of_left_le — Mathlib

English

If f is convex on s, and f(x) ≤ f(a x + b y) with a,b≥0, a+b=1, then f(a x + b y) ≤ f(y).

Русский

Если f выпукла на s и f(x) ≤ f(a x + b y) при a,b≥0, a+b=1, тогда f(a x + b y) ≤ f(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(y).$$$

Lean4

theorem le_right_of_left_le (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ openSegment 𝕜 x y)
    (hxz : f x ≤ f z) : f z ≤ f y := by
  obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz
  exact hf.le_right_of_left_le' hx hy ha.le hb hab hxz

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