mathlib3 documentation

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} [ordered_add_comm_group β] [module β] [ordered_smul β] {f : β} {a b : } (a_lt_b : a < b) (h_local_min : is_local_min_on f (set.Icc a b) a) (h_conv : convex_on (set.Icc a b) f) :
is_min_on 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} [add_comm_group E] [topological_space E] [module E] [topological_add_group E] [has_continuous_smul E] [ordered_add_comm_group β] [module β] [ordered_smul β] {s : set E} {f : E β} {a : E} (a_in_s : a s) (h_localmin : is_local_min_on f s a) (h_conv : convex_on s f) :
is_min_on 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} [add_comm_group E] [topological_space E] [module E] [topological_add_group E] [has_continuous_smul E] [ordered_add_comm_group β] [module β] [ordered_smul β] {s : set E} {f : E β} {a : E} (a_in_s : a s) (h_localmax : is_local_max_on f s a) (h_conc : concave_on s f) :
is_max_on 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} [add_comm_group E] [topological_space E] [module E] [topological_add_group E] [has_continuous_smul E] [ordered_add_comm_group β] [module β] [ordered_smul β] {f : E β} {a : E} (h_local_min : is_local_min f a) (h_conv : convex_on set.univ 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} [add_comm_group E] [topological_space E] [module E] [topological_add_group E] [has_continuous_smul E] [ordered_add_comm_group β] [module β] [ordered_smul β] {f : E β} {a : E} (h_local_max : is_local_max f a) (h_conc : concave_on set.univ f) (x : E) :
f x f a

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