Mathlib.Order.Filter.AtTopBot.Group

Filter.tendsto_atTop_mul_left_of_le' theorem

(C : G) (hf : ∀ᶠ x in l, C ≤ f x) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop

Full source

@[to_additive]
theorem tendsto_atTop_mul_left_of_le' (C : G) (hf : ∀ᶠ x in l, C ≤ f x) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop :=
  .atTop_of_isBoundedUnder_le_mul (f := f⁻¹) ⟨C⁻¹, by simpa⟩ (by simpa)

Product tends to infinity when one factor is bounded below and the other tends to infinity

Informal description

Let $G$ be an ordered commutative group, and let $f, g$ be functions from a type to $G$. Suppose there exists a constant $C \in G$ such that $C \leq f(x)$ for all $x$ in a filter $l$, and $g$ tends to positive infinity in $l$. Then the product function $x \mapsto f(x) \cdot g(x)$ also tends to positive infinity in $l$.

Filter.tendsto_atBot_mul_left_of_ge' theorem

(C : G) (hf : ∀ᶠ x in l, f x ≤ C) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot

Full source

@[to_additive]
theorem tendsto_atBot_mul_left_of_ge' (C : G) (hf : ∀ᶠ x in l, f x ≤ C) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot :=
  tendsto_atTop_mul_left_of_le' (G := Gᵒᵈ) _ C hf hg

Product tends to negative infinity when one factor is bounded above and the other tends to negative infinity

Informal description

Let $G$ be an ordered commutative group, and let $f, g$ be functions from a type to $G$. Suppose there exists a constant $C \in G$ such that $f(x) \leq C$ for all $x$ in a filter $l$, and $g$ tends to negative infinity in $l$. Then the product function $x \mapsto f(x) \cdot g(x)$ also tends to negative infinity in $l$.

Filter.tendsto_atTop_mul_left_of_le theorem

(C : G) (hf : ∀ x, C ≤ f x) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop

Full source

@[to_additive]
theorem tendsto_atTop_mul_left_of_le (C : G) (hf : ∀ x, C ≤ f x) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mul_left_of_le' l C (univ_mem' hf) hg

Product tends to infinity when one factor is uniformly bounded below and the other tends to infinity

Informal description

Let $G$ be an ordered commutative group, and let $f, g$ be functions from a type to $G$. Suppose there exists a constant $C \in G$ such that $C \leq f(x)$ for all $x$, and $g$ tends to positive infinity in a filter $l$. Then the product function $x \mapsto f(x) \cdot g(x)$ also tends to positive infinity in $l$.

Filter.tendsto_atBot_mul_left_of_ge theorem

(C : G) (hf : ∀ x, f x ≤ C) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot

Full source

@[to_additive]
theorem tendsto_atBot_mul_left_of_ge (C : G) (hf : ∀ x, f x ≤ C) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot :=
  tendsto_atTop_mul_left_of_le (G := Gᵒᵈ) _ C hf hg

Product tends to $-\infty$ when one factor is uniformly bounded above and the other tends to $-\infty$

Informal description

Let $G$ be an ordered commutative group, and let $f, g : X \to G$ be functions. If there exists a constant $C \in G$ such that $f(x) \leq C$ for all $x \in X$, and $g$ tends to $-\infty$ along a filter $l$, then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ along $l$.

Filter.tendsto_atTop_mul_right_of_le' theorem

(C : G) (hf : Tendsto f l atTop) (hg : ∀ᶠ x in l, C ≤ g x) : Tendsto (fun x => f x * g x) l atTop

Full source

@[to_additive]
theorem tendsto_atTop_mul_right_of_le' (C : G) (hf : Tendsto f l atTop) (hg : ∀ᶠ x in l, C ≤ g x) :
    Tendsto (fun x => f x * g x) l atTop :=
  .atTop_of_mul_isBoundedUnder_le (g := g⁻¹) ⟨C⁻¹, by simpa⟩ (by simpa)

Product tends to $+\infty$ when one factor tends to $+\infty$ and the other is eventually bounded below

Informal description

Let $G$ be an ordered commutative group, and let $f$ and $g$ be functions from a type $l$ to $G$. Suppose that $f$ tends to $+\infty$ along the filter $l$, and that there exists a constant $C \in G$ such that $C \leq g(x)$ for all $x$ in a set that is eventually in $l$. Then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $+\infty$ along $l$.

Filter.tendsto_atBot_mul_right_of_ge' theorem

(C : G) (hf : Tendsto f l atBot) (hg : ∀ᶠ x in l, g x ≤ C) : Tendsto (fun x => f x * g x) l atBot

Full source

@[to_additive]
theorem tendsto_atBot_mul_right_of_ge' (C : G) (hf : Tendsto f l atBot) (hg : ∀ᶠ x in l, g x ≤ C) :
    Tendsto (fun x => f x * g x) l atBot :=
  tendsto_atTop_mul_right_of_le' (G := Gᵒᵈ) _ C hf hg

Product tends to $-\infty$ when one factor tends to $-\infty$ and the other is eventually bounded above

Informal description

Let $G$ be an ordered commutative group, and let $f, g$ be functions from a type $l$ to $G$. If $f$ tends to $-\infty$ along the filter $l$ (i.e., $\text{tendsto}\, f\, l\, \text{atBot}$), and there exists a constant $C \in G$ such that $g(x) \leq C$ for all $x$ in a set that is eventually in $l$, then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ along $l$ (i.e., $\text{tendsto}\, (\lambda x, f(x) \cdot g(x))\, l\, \text{atBot}$).

Filter.tendsto_atTop_mul_right_of_le theorem

(C : G) (hf : Tendsto f l atTop) (hg : ∀ x, C ≤ g x) : Tendsto (fun x => f x * g x) l atTop

Full source

@[to_additive]
theorem tendsto_atTop_mul_right_of_le (C : G) (hf : Tendsto f l atTop) (hg : ∀ x, C ≤ g x) :
    Tendsto (fun x => f x * g x) l atTop :=
  tendsto_atTop_mul_right_of_le' l C hf (univ_mem' hg)

Product tends to $+\infty$ when one factor tends to $+\infty$ and the other is uniformly bounded below

Informal description

Let $G$ be an ordered commutative group, and let $f, g$ be functions from some type to $G$. If $f$ tends to $+\infty$ along a filter $l$, and there exists a constant $C \in G$ such that $C \leq g(x)$ for all $x$, then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $+\infty$ along $l$.

Filter.tendsto_atBot_mul_right_of_ge theorem

(C : G) (hf : Tendsto f l atBot) (hg : ∀ x, g x ≤ C) : Tendsto (fun x => f x * g x) l atBot

Full source

@[to_additive]
theorem tendsto_atBot_mul_right_of_ge (C : G) (hf : Tendsto f l atBot) (hg : ∀ x, g x ≤ C) :
    Tendsto (fun x => f x * g x) l atBot :=
  tendsto_atTop_mul_right_of_le (G := Gᵒᵈ) _  C hf hg

Product tends to $-\infty$ when one factor tends to $-\infty$ and the other is uniformly bounded above

Informal description

Let $G$ be an ordered commutative group, and let $f, g$ be functions from a type to $G$. If $f$ tends to $-\infty$ along a filter $l$ (i.e., $\lim_{x \to l} f(x) = -\infty$), and there exists a constant $C \in G$ such that $g(x) \leq C$ for all $x$, then the product function $x \mapsto f(x) \cdot g(x)$ also tends to $-\infty$ along $l$ (i.e., $\lim_{x \to l} f(x) \cdot g(x) = -\infty$).

Filter.tendsto_atTop_mul_const_left theorem

(C : G) (hf : Tendsto f l atTop) : Tendsto (fun x => C * f x) l atTop

Full source

@[to_additive]
theorem tendsto_atTop_mul_const_left (C : G) (hf : Tendsto f l atTop) :
    Tendsto (fun x => C * f x) l atTop :=
  tendsto_atTop_mul_left_of_le' l C (univ_mem' fun _ => le_refl C) hf

Product with Constant Preserves Tendency to Infinity in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group, and let $f$ be a function from a type to $G$ such that $f$ tends to positive infinity in a filter $l$. Then for any constant $C \in G$, the function $x \mapsto C \cdot f(x)$ also tends to positive infinity in $l$.

Filter.tendsto_atBot_mul_const_left theorem

(C : G) (hf : Tendsto f l atBot) : Tendsto (fun x => C * f x) l atBot

Full source

@[to_additive]
theorem tendsto_atBot_mul_const_left (C : G) (hf : Tendsto f l atBot) :
    Tendsto (fun x => C * f x) l atBot :=
  tendsto_atTop_mul_const_left (G := Gᵒᵈ) _ C hf

Product with Constant Preserves Tendency to Negative Infinity in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group, and let $f$ be a function from a type to $G$ such that $f$ tends to negative infinity in a filter $l$. Then for any constant $C \in G$, the function $x \mapsto C \cdot f(x)$ also tends to negative infinity in $l$.

Filter.tendsto_atTop_mul_const_right theorem

(C : G) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * C) l atTop

Full source

@[to_additive]
theorem tendsto_atTop_mul_const_right (C : G) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x * C) l atTop :=
  tendsto_atTop_mul_right_of_le' l C hf (univ_mem' fun _ => le_refl C)

Right Multiplication by Constant Preserves Tendency to $+\infty$ in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group, and let $f : l \to G$ be a function that tends to $+\infty$ along a filter $l$. Then for any constant $C \in G$, the function $x \mapsto f(x) \cdot C$ also tends to $+\infty$ along $l$.

Filter.tendsto_atBot_mul_const_right theorem

(C : G) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * C) l atBot

Full source

@[to_additive]
theorem tendsto_atBot_mul_const_right (C : G) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * C) l atBot :=
  tendsto_atTop_mul_const_right (G := Gᵒᵈ) _ C hf

Right Multiplication by Constant Preserves Tendency to $-\infty$ in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group, and let $f$ be a function from a type to $G$ such that $f$ tends to negative infinity along a filter $l$. Then for any constant $C \in G$, the function $x \mapsto f(x) \cdot C$ also tends to negative infinity along $l$.

Filter.map_inv_atBot theorem

: map (Inv.inv : G → G) atBot = atTop

Full source

@[to_additive]
theorem map_inv_atBot : map (Inv.inv : G → G) atBot = atTop :=
  (OrderIso.inv G).map_atBot

Inversion Maps `atBot` to `atTop` in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group. The image of the filter at negative infinity (`atBot`) under the inversion operation $x \mapsto x^{-1}$ is equal to the filter at positive infinity (`atTop$). That is, $$ (\cdot^{-1})(\text{atBot}) = \text{atTop}. $$

Filter.map_inv_atTop theorem

: map (Inv.inv : G → G) atTop = atBot

Full source

@[to_additive]
theorem map_inv_atTop : map (Inv.inv : G → G) atTop = atBot :=
  (OrderIso.inv G).map_atTop

Inversion Maps `atTop` to `atBot` in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group. The image of the filter at positive infinity (`atTop`) under the inversion operation $x \mapsto x^{-1}$ is equal to the filter at negative infinity (`atBot$). That is, $$ (\cdot^{-1})(\text{atTop}) = \text{atBot}. $$

Filter.comap_inv_atBot theorem

: comap (Inv.inv : G → G) atBot = atTop

Full source

@[to_additive]
theorem comap_inv_atBot : comap (Inv.inv : G → G) atBot = atTop :=
  (OrderIso.inv G).comap_atTop

Preimage of `atBot` under inversion equals `atTop` in ordered commutative groups

Informal description

Let $G$ be an ordered commutative group. The preimage of the filter at negative infinity (`atBot`) under the inversion operation $x \mapsto x^{-1}$ is equal to the filter at positive infinity (`atTop`). That is, $$ \text{comap } (\cdot^{-1}) \text{ atBot} = \text{atTop}. $$

Filter.comap_inv_atTop theorem

: comap (Inv.inv : G → G) atTop = atBot

Full source

@[to_additive]
theorem comap_inv_atTop : comap (Inv.inv : G → G) atTop = atBot :=
  (OrderIso.inv G).comap_atBot

Preimage of `atTop` under inversion equals `atBot` in ordered commutative groups

Informal description

Let $G$ be an ordered commutative group. The preimage of the filter at positive infinity (`atTop`) under the inversion operation $x \mapsto x^{-1}$ is equal to the filter at negative infinity (`atBot$). That is, $$ \text{comap } (\cdot^{-1}) \text{ atTop} = \text{atBot}. $$

Filter.tendsto_inv_atTop_atBot theorem

: Tendsto (Inv.inv : G → G) atTop atBot

Full source

@[to_additive]
theorem tendsto_inv_atTop_atBot : Tendsto (Inv.inv : G → G) atTop atBot :=
  (OrderIso.inv G).tendsto_atTop

Inversion Tends to Negative Infinity at Positive Infinity in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group. The inversion function $x \mapsto x^{-1}$ tends to the filter at negative infinity (`atBot`) as its input tends to the filter at positive infinity (`atTop`). That is, $$ \lim_{x \to \text{atTop}} x^{-1} = \text{atBot}. $$

Filter.tendsto_inv_atBot_atTop theorem

: Tendsto (Inv.inv : G → G) atBot atTop

Full source

@[to_additive]
theorem tendsto_inv_atBot_atTop : Tendsto (Inv.inv : G → G) atBot atTop :=
  tendsto_inv_atTop_atBot (G := Gᵒᵈ)

Inversion Tends to Positive Infinity at Negative Infinity in Ordered Commutative Groups

Informal description

Let $G$ be an ordered commutative group. The inversion function $x \mapsto x^{-1}$ tends to the filter at positive infinity (`atTop`) as its input tends to the filter at negative infinity (`atBot$). That is, $$ \lim_{x \to \text{atBot}} x^{-1} = \text{atTop}. $$

Filter.tendsto_inv_atTop_iff theorem

: Tendsto (fun x => (f x)⁻¹) l atTop ↔ Tendsto f l atBot

Full source

@[to_additive (attr := simp)]
theorem tendsto_inv_atTop_iff : TendstoTendsto (fun x => (f x)⁻¹) l atTop ↔ Tendsto f l atBot :=
  (OrderIso.inv G).tendsto_atBot_iff

Inversion Swaps Limits to Infinity: $\lim (f^{-1}) = +\infty \leftrightarrow \lim f = -\infty$

Informal description

Let $G$ be an ordered commutative group, $l$ a filter, and $f$ a function. The function $x \mapsto (f(x))^{-1}$ tends to positive infinity along $l$ if and only if $f$ tends to negative infinity along $l$. In other words: $$ \lim_{x \to l} (f(x))^{-1} = +\infty \quad \Leftrightarrow \quad \lim_{x \to l} f(x) = -\infty. $$

Filter.tendsto_inv_atBot_iff theorem

: Tendsto (fun x => (f x)⁻¹) l atBot ↔ Tendsto f l atTop

Full source

@[to_additive (attr := simp)]
theorem tendsto_inv_atBot_iff : TendstoTendsto (fun x => (f x)⁻¹) l atBot ↔ Tendsto f l atTop :=
  (OrderIso.inv G).tendsto_atTop_iff

Inversion Swaps Limits to Infinity: $\lim (f^{-1}) = -\infty \leftrightarrow \lim f = +\infty$

Informal description

Let $G$ be an ordered commutative group, $l$ a filter, and $f$ a function. The function $x \mapsto (f(x))^{-1}$ tends to negative infinity along $l$ if and only if $f$ tends to positive infinity along $l$. In other words: $$ \lim_{x \to l} (f(x))^{-1} = -\infty \quad \Leftrightarrow \quad \lim_{x \to l} f(x) = +\infty. $$

Filter.tendsto_mabs_atTop_atTop theorem

: Tendsto (mabs : G → G) atTop atTop

Full source

/-- $\lim_{x\to+\infty}|x|_m=+\infty$ -/
@[to_additive r"$\lim_{x\to+\infty}|x|=+\infty$"]
theorem tendsto_mabs_atTop_atTop : Tendsto (mabs : G → G) atTop atTop :=
  tendsto_atTop_mono le_mabs_self tendsto_id

Divergence of Multiplicative Absolute Value at Infinity: $\lim_{x \to +\infty} |x|_m = +\infty$

Informal description

For a multiplicative lattice ordered group $G$, the multiplicative absolute value function $| \cdot |_m : G \to G$ tends to infinity as its input tends to infinity. That is, $\lim_{x \to +\infty} |x|_m = +\infty$.

Filter.tendsto_mabs_atBot_atTop theorem

[IsOrderedMonoid G] : Tendsto (mabs : G → G) atBot atTop

Full source

/-- $\lim_{x\to\infty^{-1}|x|_m=+\infty$ -/
@[to_additive r"$\lim_{x\to-\infty}|x|=+\infty$"]
theorem tendsto_mabs_atBot_atTop [IsOrderedMonoid G] : Tendsto (mabs : G → G) atBot atTop :=
  tendsto_atTop_mono inv_le_mabs tendsto_inv_atBot_atTop

Divergence of Multiplicative Absolute Value at Negative Infinity: $\lim_{x \to -\infty} |x|_m = +\infty$

Informal description

Let $G$ be an ordered commutative monoid. The multiplicative absolute value function $|\cdot|_m : G \to G$ tends to positive infinity as its input tends to negative infinity. That is, $$ \lim_{x \to -\infty} |x|_m = +\infty. $$

Filter.comap_mabs_atTop theorem

[IsOrderedMonoid G] : comap (mabs : G → G) atTop = atBot ⊔ atTop

Full source

@[to_additive (attr := simp)]
theorem comap_mabs_atTop [IsOrderedMonoid G] : comap (mabs : G → G) atTop = atBotatBot ⊔ atTop := by
  refine
    le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
      (sup_le tendsto_mabs_atBot_atTop.le_comap tendsto_mabs_atTop_atTop.le_comap)
  rintro ⟨a, b⟩ -
  refine ⟨max (a⁻¹) b, trivial, fun x hx => ?_⟩
  rw [mem_preimage, mem_Ici, le_mabs', max_le_iff, ← min_inv_inv', le_min_iff, inv_inv] at hx
  exact hx.imp And.left And.right

Preimage of Positive Infinity Filter under Multiplicative Absolute Value Equals Supremum of Negative and Positive Infinity Filters

Informal description

Let $G$ be an ordered commutative monoid. The preimage of the filter at positive infinity under the multiplicative absolute value function $|\cdot|_m : G \to G$ is equal to the supremum of the filters at negative infinity and positive infinity. That is, $$ (|\cdot|_m)^{-1}(\text{atTop}) = \text{atBot} \sqcup \text{atTop}. $$