Monotone convergence on a closed half-line #
A function that is monotone and bounded above on a closed half-line [a, ∞) tends at infinity to
its supremum over that half-line, and dually for antitone functions bounded below. These are the
half-line forms of Mathlib's tendsto_atTop_ciSup and tendsto_atTop_ciInf, which ask for
monotonicity on the whole domain. They apply, for instance, to a quantity monotone along a
trajectory that is only defined, or only monotone, in forward time.
Main results #
TauCeti.tendsto_atTop_ciSup_of_monotoneOn_Ici— a function monotone and bounded above on[a, ∞)tends to its supremum there.TauCeti.tendsto_atTop_ciInf_of_antitoneOn_Ici— a function antitone and bounded below on[a, ∞)tends to its infimum there.
theorem
TauCeti.tendsto_atTop_ciSup_of_monotoneOn_Ici
{ι : Type u_1}
{α : Type u_2}
[Preorder ι]
[IsDirectedOrder ι]
[TopologicalSpace α]
{f : ι → α}
{a : ι}
[ConditionallyCompletePartialOrderSup α]
[SupConvergenceClass α]
(hf : MonotoneOn f (Set.Ici a))
(hbdd : BddAbove (f '' Set.Ici a))
:
Filter.Tendsto f Filter.atTop (nhds (⨆ (t : ↑(Set.Ici a)), f ↑t))
Monotone convergence on a half-line. A function monotone and bounded above on [a, ∞)
tends at infinity to its supremum over [a, ∞).
theorem
TauCeti.tendsto_atTop_ciInf_of_antitoneOn_Ici
{ι : Type u_1}
{α : Type u_2}
[Preorder ι]
[IsDirectedOrder ι]
[TopologicalSpace α]
{f : ι → α}
{a : ι}
[ConditionallyCompletePartialOrderInf α]
[InfConvergenceClass α]
(hf : AntitoneOn f (Set.Ici a))
(hbdd : BddBelow (f '' Set.Ici a))
:
Filter.Tendsto f Filter.atTop (nhds (⨅ (t : ↑(Set.Ici a)), f ↑t))
Antitone convergence on a half-line. A function antitone and bounded below on [a, ∞)
tends at infinity to its infimum over [a, ∞).