le_right_of_left_le' — Mathlib

English

A strictly convex function on an open segment satisfies a strict inequality on interior points against the endpoints.

Русский

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

LaTeX

$$$\StrictConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y,z\in openSegment(\mathfrak{K}, x, y): f(z) < \max\{f(x), f(y)\}$$$

Lean4

theorem le_right_of_left_le' (hf : ConvexOn 𝕜 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 x ≤ f (a • x + b • y)) : f (a • x + b • y) ≤ f y :=
  by
  rw [add_comm] at hab hfx ⊢
  exact hf.le_left_of_right_le' hy hx hb ha hab hfx

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