mathlib documentation

analysis.​convex.​extrema

analysis.​convex.​extrema

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 is_min_on.​of_is_local_min_on_of_convex_on_Icc {β : Type u_2} [decidable_linear_ordered_add_comm_group β] [ordered_semimodule β] {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) (x : ) :
x set.Icc a bf a f x

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] [topological_vector_space E] [decidable_linear_ordered_add_comm_group β] [ordered_semimodule β] {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) (x : E) :
x sf a f x

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] [topological_vector_space E] [decidable_linear_ordered_add_comm_group β] [ordered_semimodule β] {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) (x : E) :
x sf x f 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] [topological_vector_space E] [decidable_linear_ordered_add_comm_group β] [ordered_semimodule β] {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] [topological_vector_space E] [decidable_linear_ordered_add_comm_group β] [ordered_semimodule β] {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.