English
A strictly convex function on a set has at most one global minimum. If x and y are both global minimizers of f on a set s, then x = y.
Русский
У строго выпуклой функции на множестве существует как минимум одно глобальное минимальное значение, но не более одного минимального элемента; если два элемента являются глобальными минимума, то они совпадают.
LaTeX
$$$$\\text{If } f \\text{ is strictly convex on } s, \\text{ and } x,y \\in s \\text{ are minimizers of } f\\text{ on } s, \\text{ then } x=y.$$$$
Lean4
/-- A strictly convex function admits at most one global minimum. -/
theorem eq_of_isMinOn (hf : StrictConvexOn 𝕜 s f) (hfx : IsMinOn f s x) (hfy : IsMinOn f s y) (hx : x ∈ s)
(hy : y ∈ s) : x = y := by
by_contra hxy
let z := (2 : 𝕜)⁻¹ • x + (2 : 𝕜)⁻¹ • y
have hz : z ∈ s := hf.1 hx hy (by simp) (by simp) <| by norm_num
refine lt_irrefl (f z) ?_
calc
f z < _ := hf.2 hx hy hxy (by simp) (by simp) <| by norm_num
_ ≤ (2 : 𝕜)⁻¹ • f z + (2 : 𝕜)⁻¹ • f z := by gcongr; exacts [hfx hz, hfy hz]
_ = f z := by rw [← _root_.add_smul]; norm_num
