English
If f is convex on a segment between x and y, the maximum of f on that segment is achieved at x or y.
Русский
Если f выпукла на отрезке между x и y, максимум достигается в концах отрезка.
LaTeX
$$$ \text{ConvexOn}_{\mathbb{K}}(s,f) \Rightarrow f(z) \le \max\{f(x), f(y)\} \text{ for } z \in \text{segment}(x,y)$$$
Lean4
/-- **Maximum principle** for convex functions. If a function `f` is convex on the convex hull of
`s`, then the eventual maximum of `f` on `convexHull 𝕜 s` lies in `s`. -/
theorem exists_ge_of_mem_convexHull {t : Set E} (hf : ConvexOn 𝕜 s f) (hts : t ⊆ s) (hx : x ∈ convexHull 𝕜 t) :
∃ y ∈ t, f x ≤ f y := by
rw [_root_.convexHull_eq] at hx
obtain ⟨α, t, w, p, hw₀, hw₁, hp, rfl⟩ := hx
obtain ⟨i, hit, Hi⟩ := hf.exists_ge_of_centerMass hw₀ (hw₁.symm ▸ zero_lt_one) fun i hi ↦ hts (hp i hi)
exact ⟨p i, hp i hit, Hi⟩
