Convergence to ±infinity in ordered commutative monoids #
theorem
Filter.Tendsto.one_eventuallyLE_mul_atTop
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : 1 ≤ᶠ[l] f)
(hg : Tendsto g l atTop)
:
theorem
Filter.Tendsto.zero_eventuallyLE_add_atTop
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : 0 ≤ᶠ[l] f)
(hg : Tendsto g l atTop)
:
theorem
Filter.Tendsto.eventuallyLE_one_mul_atBot
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : f ≤ᶠ[l] 1)
(hg : Tendsto g l atBot)
:
theorem
Filter.Tendsto.eventuallyLE_zero_add_atBot
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : f ≤ᶠ[l] 0)
(hg : Tendsto g l atBot)
:
theorem
Filter.Tendsto.one_le_mul_atTop
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∀ (x : α), 1 ≤ f x)
(hg : Tendsto g l atTop)
:
theorem
Filter.Tendsto.nonneg_add_atTop
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∀ (x : α), 0 ≤ f x)
(hg : Tendsto g l atTop)
:
theorem
Filter.Tendsto.le_one_mul_atBot
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∀ (x : α), f x ≤ 1)
(hg : Tendsto g l atBot)
:
theorem
Filter.Tendsto.nonpos_add_atBot
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∀ (x : α), f x ≤ 0)
(hg : Tendsto g l atBot)
:
theorem
Filter.Tendsto.atTop_mul_one_eventuallyLE
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : 1 ≤ᶠ[l] g)
:
theorem
Filter.Tendsto.atTop_add_zero_eventuallyLE
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : 0 ≤ᶠ[l] g)
:
theorem
Filter.Tendsto.atBot_mul_eventuallyLE_one
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : g ≤ᶠ[l] 1)
:
theorem
Filter.Tendsto.atBot_add_eventuallyLE_zero
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : g ≤ᶠ[l] 0)
:
theorem
Filter.Tendsto.atTop_mul_one_le
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : ∀ (x : α), 1 ≤ g x)
:
theorem
Filter.Tendsto.atTop_add_nonneg
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : ∀ (x : α), 0 ≤ g x)
:
theorem
Filter.Tendsto.atBot_mul_le_one
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : ∀ (x : α), g x ≤ 1)
:
theorem
Filter.Tendsto.atBot_add_nonpos
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : ∀ (x : α), g x ≤ 0)
:
theorem
Filter.Tendsto.atTop_mul_atTop
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : Tendsto g l atTop)
:
In an ordered multiplicative monoid, if f and g tend to +∞, then so does f * g.
Earlier, this name was used for a similar lemma about semirings,
which is now called Filter.Tendsto.atTop_mul_atTop₀.
theorem
Filter.Tendsto.atTop_add_atTop
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atTop)
(hg : Tendsto g l atTop)
:
theorem
Filter.Tendsto.atBot_mul_atBot
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : Tendsto g l atBot)
:
In an ordered multiplicative monoid, if f and g tend to -∞, then so does f * g.
Earlier, this name was used for a similar lemma about rings (with conclusion f * g → +∞),
which is now called Filter.Tendsto.atBot_mul_atBot₀.
theorem
Filter.Tendsto.atBot_add_atBot
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : Tendsto f l atBot)
(hg : Tendsto g l atBot)
:
theorem
Filter.Tendsto.atTop_pow
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f : α → M}
(hf : Tendsto f l atTop)
{n : ℕ}
(hn : 0 < n)
:
theorem
Filter.Tendsto.nsmul_atTop
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f : α → M}
(hf : Tendsto f l atTop)
{n : ℕ}
(hn : 0 < n)
:
theorem
Filter.Tendsto.atBot_pow
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedMonoid M]
{l : Filter α}
{f : α → M}
(hf : Tendsto f l atBot)
{n : ℕ}
(hn : 0 < n)
:
theorem
Filter.Tendsto.nsmul_atBot
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedAddMonoid M]
{l : Filter α}
{f : α → M}
(hf : Tendsto f l atBot)
{n : ℕ}
(hn : 0 < n)
:
theorem
Filter.Tendsto.atTop_of_const_mul
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C * f x) l atTop)
:
In an ordered cancellative multiplicative monoid, if C * f x → +∞, then f x → +∞.
Earlier, this name was used for a similar lemma about ordered rings,
which is now called Filter.Tendsto.atTop_of_const_mul₀.
theorem
Filter.Tendsto.atTop_of_const_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C + f x) l atTop)
:
theorem
Filter.Tendsto.atBot_of_const_mul
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C * f x) l atBot)
:
theorem
Filter.Tendsto.atBot_of_const_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => C + f x) l atBot)
:
theorem
Filter.Tendsto.atTop_of_mul_const
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x * C) l atTop)
:
In an ordered cancellative multiplicative monoid, if f x * C → +∞, then f x → +∞.
Earlier, this name was used for a similar lemma about ordered rings,
which is now called Filter.Tendsto.atTop_of_mul_const₀.
theorem
Filter.Tendsto.atTop_of_add_const
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x + C) l atTop)
:
theorem
Filter.Tendsto.atBot_of_mul_const
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x * C) l atBot)
:
theorem
Filter.Tendsto.atBot_of_add_const
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f : α → M}
(C : M)
(hf : Tendsto (fun (x : α) => f x + C) l atBot)
:
theorem
Filter.Tendsto.atTop_of_isBoundedUnder_le_mul
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l f)
(hfg : Tendsto (fun (x : α) => f x * g x) l atTop)
:
If f is eventually bounded from above along l and f * g tends to +∞,
then g tends to +∞.
theorem
Filter.Tendsto.atTop_of_isBoundedUnder_le_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l f)
(hfg : Tendsto (fun (x : α) => f x + g x) l atTop)
:
If f is eventually bounded from above along l and f + g tends to +∞,
then g tends to +∞.
theorem
Filter.Tendsto.atBot_of_isBoundedUnder_ge_mul
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l f)
(h : Tendsto (fun (x : α) => f x * g x) l atBot)
:
theorem
Filter.Tendsto.atBot_of_isBoundedUnder_ge_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l f)
(h : Tendsto (fun (x : α) => f x + g x) l atBot)
:
theorem
Filter.Tendsto.atTop_of_le_const_mul
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∃ (C : M), ∀ (x : α), f x ≤ C)
(hfg : Tendsto (fun (x : α) => f x * g x) l atTop)
:
theorem
Filter.Tendsto.atTop_of_le_const_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∃ (C : M), ∀ (x : α), f x ≤ C)
(hfg : Tendsto (fun (x : α) => f x + g x) l atTop)
:
theorem
Filter.Tendsto.atBot_of_const_le_mul
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∃ (C : M), ∀ (x : α), C ≤ f x)
(hfg : Tendsto (fun (x : α) => f x * g x) l atBot)
:
theorem
Filter.Tendsto.atBot_of_const_le_add
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hf : ∃ (C : M), ∀ (x : α), C ≤ f x)
(hfg : Tendsto (fun (x : α) => f x + g x) l atBot)
:
theorem
Filter.Tendsto.atTop_of_mul_isBoundedUnder_le
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l g)
(h : Tendsto (fun (x : α) => f x * g x) l atTop)
:
theorem
Filter.Tendsto.atTop_of_add_isBoundedUnder_le
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≤ x2) l g)
(h : Tendsto (fun (x : α) => f x + g x) l atTop)
:
theorem
Filter.Tendsto.atBot_of_mul_isBoundedUnder_ge
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l g)
(h : Tendsto (fun (x : α) => f x * g x) l atBot)
:
theorem
Filter.Tendsto.atBot_of_add_isBoundedUnder_ge
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hg : IsBoundedUnder (fun (x1 x2 : M) => x1 ≥ x2) l g)
(h : Tendsto (fun (x : α) => f x + g x) l atBot)
:
theorem
Filter.Tendsto.atTop_of_mul_le_const
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hg : ∃ (C : M), ∀ (x : α), g x ≤ C)
(hfg : Tendsto (fun (x : α) => f x * g x) l atTop)
:
theorem
Filter.Tendsto.atTop_of_add_le_const
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hg : ∃ (C : M), ∀ (x : α), g x ≤ C)
(hfg : Tendsto (fun (x : α) => f x + g x) l atTop)
:
theorem
Filter.Tendsto.atBot_of_mul_const_le
{α : Type u_1}
{M : Type u_2}
[CommMonoid M]
[PartialOrder M]
[IsOrderedCancelMonoid M]
{l : Filter α}
{f g : α → M}
(hg : ∃ (C : M), ∀ (x : α), C ≤ g x)
(hfg : Tendsto (fun (x : α) => f x * g x) l atBot)
:
theorem
Filter.Tendsto.atBot_of_add_const_le
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(hg : ∃ (C : M), ∀ (x : α), C ≤ g x)
(hfg : Tendsto (fun (x : α) => f x + g x) l atBot)
:
@[deprecated Filter.Tendsto.atTop_of_isBoundedUnder_le_add (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_of_add_bdd_above_left'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ᶠ (x : α) in l, f x ≤ C)
(h : Tendsto (fun (x : α) => f x + g x) l atTop)
:
@[deprecated Filter.Tendsto.atBot_of_isBoundedUnder_ge_add (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_of_add_bdd_below_left'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ᶠ (x : α) in l, C ≤ f x)
(h : Tendsto (fun (x : α) => f x + g x) l atBot)
:
@[deprecated Filter.Tendsto.atTop_of_le_const_add (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_of_add_bdd_above_left
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ (x : α), f x ≤ C)
:
@[deprecated Filter.Tendsto.atBot_of_const_le_add (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_of_add_bdd_below_left
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ (x : α), C ≤ f x)
:
@[deprecated Filter.Tendsto.atTop_of_add_isBoundedUnder_le (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_of_add_bdd_above_right'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ᶠ (x : α) in l, g x ≤ C)
(h : Tendsto (fun (x : α) => f x + g x) l atTop)
:
@[deprecated Filter.Tendsto.atBot_of_add_isBoundedUnder_ge (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_of_add_bdd_below_right'
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ᶠ (x : α) in l, C ≤ g x)
(h : Tendsto (fun (x : α) => f x + g x) l atBot)
:
@[deprecated Filter.Tendsto.atTop_of_add_le_const (since := "2025-02-13")]
theorem
Filter.tendsto_atTop_of_add_bdd_above_right
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ (x : α), g x ≤ C)
:
@[deprecated Filter.Tendsto.atBot_of_add_const_le (since := "2025-02-13")]
theorem
Filter.tendsto_atBot_of_add_bdd_below_right
{α : Type u_1}
{M : Type u_2}
[AddCommMonoid M]
[PartialOrder M]
[IsOrderedCancelAddMonoid M]
{l : Filter α}
{f g : α → M}
(C : M)
(hC : ∀ (x : α), C ≤ g x)
: