# mathlib3documentation

analysis.convex.extrema

# Minima and maxima of convex functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_min_on.of_is_local_min_on_of_convex_on_Icc {β : Type u_2} [ β] [ β] {f : β} {a b : } (a_lt_b : a < b) (h_local_min : (set.Icc a b) a) (h_conv : (set.Icc a b) f) :
(set.Icc a b) a

Helper lemma for the more general case: is_min_on.of_is_local_min_on_of_convex_on.

theorem is_min_on.of_is_local_min_on_of_convex_on {E : Type u_1} {β : Type u_2} [ E] [ β] [ β] {s : set E} {f : E β} {a : E} (a_in_s : a s) (h_localmin : a) (h_conv : f) :
s a

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

theorem is_max_on.of_is_local_max_on_of_concave_on {E : Type u_1} {β : Type u_2} [ E] [ β] [ β] {s : set E} {f : E β} {a : E} (a_in_s : a s) (h_localmax : a) (h_conc : f) :
s a

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

theorem is_min_on.of_is_local_min_of_convex_univ {E : Type u_1} {β : Type u_2} [ E] [ β] [ β] {f : E β} {a : E} (h_local_min : a) (h_conv : f) (x : E) :
f a f x

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

theorem is_max_on.of_is_local_max_of_convex_univ {E : Type u_1} {β : Type u_2} [ E] [ β] [ β] {f : E β} {a : E} (h_local_max : a) (h_conc : f) (x : E) :
f x f a

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