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}
[OrderedAddCommGroup β]
[Module ℝ β]
[OrderedSMul ℝ β]
{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)
:
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}
[AddCommGroup E]
[TopologicalSpace E]
[Module ℝ E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
[OrderedAddCommGroup β]
[Module ℝ β]
[OrderedSMul ℝ β]
{s : Set E}
{f : E → β}
{a : E}
(a_in_s : a ∈ s)
(h_localmin : IsLocalMinOn f s a)
(h_conv : ConvexOn ℝ s f)
:
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}
[AddCommGroup E]
[TopologicalSpace E]
[Module ℝ E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
[OrderedAddCommGroup β]
[Module ℝ β]
[OrderedSMul ℝ β]
{s : Set E}
{f : E → β}
{a : E}
(a_in_s : a ∈ s)
(h_localmax : IsLocalMaxOn f s a)
(h_conc : ConcaveOn ℝ s f)
:
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}
[AddCommGroup E]
[TopologicalSpace E]
[Module ℝ E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
[OrderedAddCommGroup β]
[Module ℝ β]
[OrderedSMul ℝ β]
{f : E → β}
{a : E}
(h_local_min : IsLocalMin f a)
(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}
[AddCommGroup E]
[TopologicalSpace E]
[Module ℝ E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
[OrderedAddCommGroup β]
[Module ℝ β]
[OrderedSMul ℝ β]
{f : E → β}
{a : E}
(h_local_max : IsLocalMax f a)
(h_conc : ConcaveOn ℝ Set.univ f)
(x : E)
:
f x ≤ f a
A local maximum of a concave function is a global maximum.