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) :
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.