English
If a convex function reaches its maximum on a convex hull, it must occur at a vertex of the hull.
Русский
Если выпуклая функция достигает максимума на выпуклой оболочке, максимум достигается в вершине оболочки.
LaTeX
$$$ \text{ConvexOn}_{\mathbb{K}}(s,f) \Rightarrow \exists i \in t, f(p_i) = \max_{j} f(p_j)$$$
Lean4
/-- **Maximum principle** for convex functions on a segment. If a function `f` is convex on the
segment `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`. -/
theorem le_max_of_mem_segment (hf : ConvexOn 𝕜 s f) (hx : x ∈ s) (hy : y ∈ s) (hz : z ∈ [x -[𝕜] y]) :
f z ≤ max (f x) (f y) := by rw [← convexHull_pair] at hz;
simpa using hf.exists_ge_of_mem_convexHull (pair_subset hx hy) hz
