Minima and maxima of convex functions #

We show that if a function f : E → β is convex, then a local minimum is also a global minimum, and likewise for concave functions.

theorem IsMinOn.of_isLocalMinOn_of_convexOn_Icc {β : Type u_2} [] [] {f : β} {a : } {b : } (a_lt_b : a < b) (h_local_min : IsLocalMinOn f (Set.Icc a b) a) (h_conv : ConvexOn (Set.Icc a b) f) :
IsMinOn f (Set.Icc a b) a

Helper lemma for the more general case: IsMinOn.of_isLocalMinOn_of_convexOn.

theorem IsMinOn.of_isLocalMinOn_of_convexOn {E : Type u_1} {β : Type u_2} [] [] [] [] [] [] {s : Set E} {f : Eβ} {a : E} (a_in_s : a s) (h_localmin : IsLocalMinOn f s a) (h_conv : ) :
IsMinOn f s a

A local minimum of a convex function is a global minimum, restricted to a set s.

theorem IsMaxOn.of_isLocalMaxOn_of_concaveOn {E : Type u_1} {β : Type u_2} [] [] [] [] [] [] {s : Set E} {f : Eβ} {a : E} (a_in_s : a s) (h_localmax : IsLocalMaxOn f s a) (h_conc : ) :
IsMaxOn f s a

A local maximum of a concave function is a global maximum, restricted to a set s.

theorem IsMinOn.of_isLocalMin_of_convex_univ {E : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : Eβ} {a : E} (h_local_min : ) (h_conv : ConvexOn Set.univ f) (x : E) :
f a f x

A local minimum of a convex function is a global minimum.

theorem IsMaxOn.of_isLocalMax_of_convex_univ {E : Type u_1} {β : Type u_2} [] [] [] [] [] [] {f : Eβ} {a : E} (h_local_max : ) (h_conc : ConcaveOn Set.univ f) (x : E) :
f x f a

A local maximum of a concave function is a global maximum.