Local maxima from monotonicity and antitonicity #
In this file we prove a lemma that is useful for the First Derivative Test in calculus, and its dual.
Main statements #
isLocalMax_of_mono_anti: if a functionfis monotone to the left ofxand antitone to the right ofxthenfhas a local maximum atx.isLocalMin_of_anti_mono: the dual statement for minima.isLocalMax_of_mono_anti': a version ofisLocalMax_of_mono_antifor filters.isLocalMin_of_anti_mono': a version ofisLocalMax_of_mono_anti'for minima.
theorem
isLocalMax_of_mono_anti
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{β : Type u_2}
[Preorder β]
{a : α}
{b : α}
{c : α}
(g₀ : a < b)
(g₁ : b < c)
{f : α → β}
(h₀ : MonotoneOn f (Set.Ioc a b))
(h₁ : AntitoneOn f (Set.Ico b c))
:
IsLocalMax f b
If f is monotone on (a,b] and antitone on [b,c) then f has
a local maximum at b.
theorem
isLocalMin_of_anti_mono
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
[OrderClosedTopology α]
{β : Type u_2}
[Preorder β]
{a : α}
{b : α}
{c : α}
(g₀ : a < b)
(g₁ : b < c)
{f : α → β}
(h₀ : AntitoneOn f (Set.Ioc a b))
(h₁ : MonotoneOn f (Set.Ico b c))
:
IsLocalMin f b
If f is antitone on (a,b] and monotone on [b,c) then f has
a local minimum at b.