English
A local minimum of a convex function on the segment Icc[a,b] is a global minimum on that segment.
Русский
Локальный минимум выпуклой функции на отрезке Icc(a,b) является глобальным минимумом на этом отрезке.
LaTeX
$$$$ a < b \to IsLocalMinOn f (Icc a b) a \to ConvexOn ℝ (Icc a b) f \to IsMinOn f (Icc a b) a. $$$$
Lean4
/-- Helper lemma for the more general case: `IsMinOn.of_isLocalMinOn_of_convexOn`.
-/
theorem of_isLocalMinOn_of_convexOn_Icc {f : ℝ → β} {a b : ℝ} (a_lt_b : a < b)
(h_local_min : IsLocalMinOn f (Icc a b) a) (h_conv : ConvexOn ℝ (Icc a b) f) : IsMinOn f (Icc a b) a :=
by
rintro c hc
dsimp only [mem_setOf_eq]
rw [IsLocalMinOn, nhdsWithin_Icc_eq_nhdsGE a_lt_b] at h_local_min
rcases hc.1.eq_or_lt with (rfl | a_lt_c)
· exact le_rfl
have H₁ : ∀ᶠ y in 𝓝[>] a, f a ≤ f y := h_local_min.filter_mono (nhdsWithin_mono _ Ioi_subset_Ici_self)
have H₂ : ∀ᶠ y in 𝓝[>] a, y ∈ Ioc a c := Ioc_mem_nhdsGT a_lt_c
rcases (H₁.and H₂).exists with ⟨y, hfy, hy_ac⟩
rcases (Convex.mem_Ioc a_lt_c).mp hy_ac with ⟨ya, yc, ya₀, yc₀, yac, rfl⟩
suffices ya • f a + yc • f a ≤ ya • f a + yc • f c from
(smul_le_smul_iff_of_pos_left yc₀).1 (le_of_add_le_add_left this)
calc
ya • f a + yc • f a = f a := by rw [← add_smul, yac, one_smul]
_ ≤ f (ya * a + yc * c) := hfy
_ ≤ ya • f a + yc • f c := h_conv.2 (left_mem_Icc.2 a_lt_b.le) hc ya₀ yc₀.le yac
