le_on_segment — Mathlib

English

If f is convex on s, then for any x,y in s and z on the segment between them, f(z) ≤ max{f(x), f(y)}.

Русский

Если f выпукла на s, то для любых x,y в s и z на отрезке между ними f(z) ≤ max{f(x), f(y)}.

LaTeX

$$$\ConvexOn(\mathfrak{K}, s, f) \Rightarrow \forall x,y\in s, z\in \mathrm{segment}(\mathfrak{K}, x, y): f(z) \le \max\{f(x), f(y)\}$$$

Lean4

/-- A convex function on a segment is upper-bounded by the max of its endpoints. -/
theorem le_on_segment (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) :
    f z ≤ max (f x) (f y) :=
  let ⟨_, _, ha, hb, hab, hz⟩ := hz
  hz ▸ hf.le_on_segment' hx hy ha hb hab

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