Mathlib.Order.Filter.AtTopBot.Archimedean

Nat.comap_cast_atTop theorem

[Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] : comap ((↑) : ℕ → R) atTop = atTop

Full source

@[simp]
theorem Nat.comap_cast_atTop [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℕ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Nat.cast_le) exists_nat_ge

Preimage of `atTop` Filter under Natural Number Embedding in Archimedean Semirings

Informal description

For any strict ordered semiring $R$ that is Archimedean, the preimage of the `atTop` filter under the canonical embedding $\mathbb{N} \to R$ is equal to the `atTop` filter on $\mathbb{N}$. In other words, $\text{comap}\,(\uparrow : \mathbb{N} \to R)\, \text{atTop} = \text{atTop}$.

tendsto_natCast_atTop_iff theorem

 [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℕ} {l : Filter α} :
  Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop

Full source

theorem tendsto_natCast_atTop_iff [Semiring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {f : α → ℕ}
    {l : Filter α} : TendstoTendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop :=
  tendsto_atTop_embedding (fun _ _ => Nat.cast_le) exists_nat_ge

Equivalence of Tendency to Infinity for Natural Number Casts in Archimedean Semirings

Informal description

Let $R$ be a strict ordered semiring with a partial order that is Archimedean, and let $f : \alpha \to \mathbb{N}$ be a function. Then the function $n \mapsto (f(n) : R)$ tends to $\mathrm{atTop}$ along a filter $l$ if and only if $f$ tends to $\mathrm{atTop}$ along $l$.

tendsto_natCast_atTop_atTop theorem

[Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] : Tendsto ((↑) : ℕ → R) atTop atTop

Full source

theorem tendsto_natCast_atTop_atTop [Semiring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] :
    Tendsto ((↑) : ℕ → R) atTop atTop :=
  Nat.mono_cast.tendsto_atTop_atTop exists_nat_ge

Natural Number Cast Preserves Divergence to Infinity in Archimedean Semirings

Informal description

Let $R$ be a linear ordered Archimedean semiring. The canonical embedding $\mathbb{N} \to R$ tends to infinity along the filter `atTop` on $\mathbb{N}$ if and only if it tends to infinity along the filter `atTop` on $R$. In other words, the sequence of natural numbers cast as elements of $R$ diverges to infinity if and only if the original sequence of natural numbers diverges to infinity.

Filter.Eventually.natCast_atTop theorem

 [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atTop, p x) :
  ∀ᶠ (n : ℕ) in atTop, p n

Full source

theorem Filter.Eventually.natCast_atTop [Semiring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℕ) in atTop, p n :=
  tendsto_natCast_atTop_atTop.eventually h

Natural number cast preserves eventual truth at infinity in Archimedean semirings

Informal description

Let $R$ be a linear ordered Archimedean semiring. For any predicate $p : R \to \mathrm{Prop}$, if $p(x)$ holds for all sufficiently large $x \in R$ (i.e., $\forall^\infty x \in R, p(x)$), then $p(n)$ holds for all sufficiently large natural numbers $n \in \mathbb{N}$ (i.e., $\forall^\infty n \in \mathbb{N}, p(n)$).

Int.comap_cast_atTop theorem

[Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] : comap ((↑) : ℤ → R) atTop = atTop

Full source

@[simp] theorem Int.comap_cast_atTop [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] :
    comap ((↑) : ℤ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Int.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge r; ⟨n, mod_cast hn⟩

Preimage of `atTop` under Integer Cast in Archimedean Rings

Informal description

Let $R$ be a linear ordered Archimedean ring. The preimage of the filter `atTop` on $R$ under the canonical embedding $\mathbb{Z} \to R$ is equal to the filter `atTop` on $\mathbb{Z}$. In other words, for any integer $n$, the condition that $(n : R)$ tends to infinity in $R$ is equivalent to $n$ tending to infinity in $\mathbb{Z}$.

Int.comap_cast_atBot theorem

[Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] : comap ((↑) : ℤ → R) atBot = atBot

Full source

@[simp]
theorem Int.comap_cast_atBot [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℤ → R) atBot = atBot :=
  comap_embedding_atBot (fun _ _ => Int.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge (-r)
    ⟨-n, by simpa [neg_le] using hn⟩

Preimage of Negative Infinity Filter under Integer Cast in Strictly Ordered Archimedean Rings

Informal description

Let $R$ be a strictly ordered ring that is Archimedean. The preimage of the filter `atBot` under the canonical homomorphism from $\mathbb{Z}$ to $R$ is equal to the filter `atBot` on $\mathbb{Z}$. In other words, for any function $f : \alpha \to \mathbb{Z}$, the composition $\mathbb{Z} \to R$ tends to negative infinity along a filter $l$ if and only if $f$ tends to negative infinity along $l$.

tendsto_intCast_atTop_iff theorem

 [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
  Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop

Full source

theorem tendsto_intCast_atTop_iff [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R]
    {f : α → ℤ}
    {l : Filter α} : TendstoTendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop := by
  rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]; rfl

Equivalence of Tendency to Infinity for Integer Casts in Archimedean Rings

Informal description

Let $R$ be a linear ordered Archimedean ring, and let $f : \alpha \to \mathbb{Z}$ be a function. The composition $(n \mapsto (f(n) : R))$ tends to infinity along the filter $l$ if and only if $f$ tends to infinity along $l$.

tendsto_intCast_atBot_iff theorem

 [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
  Tendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot

Full source

theorem tendsto_intCast_atBot_iff [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {f : α → ℤ}
    {l : Filter α} : TendstoTendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot := by
  rw [← @Int.comap_cast_atBot R, tendsto_comap_iff]; rfl

Equivalence of Integer and Ring Limits to Negative Infinity in Archimedean Rings

Informal description

Let $R$ be a strictly ordered ring that is Archimedean, and let $f : \alpha \to \mathbb{Z}$ be a function. The composition $\mathbb{Z} \to R$ (via the canonical homomorphism) tends to negative infinity along a filter $l$ if and only if $f$ tends to negative infinity along $l$. In other words, $\lim_{l} (f(n) : R) = -\infty \leftrightarrow \lim_{l} f(n) = -\infty$.

tendsto_intCast_atTop_atTop theorem

[Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] : Tendsto ((↑) : ℤ → R) atTop atTop

Full source

theorem tendsto_intCast_atTop_atTop [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] :
    Tendsto ((↑) : ℤ → R) atTop atTop :=
  tendsto_intCast_atTop_iff.2 tendsto_id

Integer Cast Tends to Infinity in Archimedean Rings

Informal description

Let $R$ be a linear ordered Archimedean ring. The canonical embedding $\mathbb{Z} \to R$ tends to infinity along the filter `atTop` on $\mathbb{Z}$ if and only if it tends to infinity along the filter `atTop` on $R$. In other words, the sequence of integer casts $(n \mapsto (n : R))$ tends to infinity in $R$ as $n$ tends to infinity in $\mathbb{Z}$.

Filter.Eventually.intCast_atTop theorem

 [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atTop, p x) :
  ∀ᶠ (n : ℤ) in atTop, p n

Full source

theorem Filter.Eventually.intCast_atTop [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℤ) in atTop, p n := by
  rw [← Int.comap_cast_atTop (R := R)]; exact h.comap _

Eventual Truth Preservation under Integer Cast in Archimedean Rings

Informal description

Let $R$ be a linear ordered Archimedean ring. For any predicate $p : R \to \text{Prop}$, if $p(x)$ holds for all sufficiently large $x \in R$ (i.e., $\forall x \geq a, p(x)$ for some $a \in R$), then $p(n)$ holds for all sufficiently large integers $n \in \mathbb{Z}$ (i.e., $\forall n \geq b, p(n)$ for some $b \in \mathbb{Z}$).

Filter.Eventually.intCast_atBot theorem

 [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atBot, p x) :
  ∀ᶠ (n : ℤ) in atBot, p n

Full source

theorem Filter.Eventually.intCast_atBot [Ring R] [PartialOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atBot, p x) : ∀ᶠ (n : ℤ) in atBot, p n := by
  rw [← Int.comap_cast_atBot (R := R)]; exact h.comap _

Eventual Property Preservation under Integer Cast at Negative Infinity

Informal description

Let $R$ be a strictly ordered Archimedean ring. For any predicate $p : R \to \text{Prop}$, if $p(x)$ holds for all sufficiently negative $x \in R$ (i.e., $\forall x \leq a, p(x)$ for some $a \in R$), then $p(n)$ holds for all sufficiently negative integers $n \in \mathbb{Z}$ (i.e., $\forall n \leq b, p(n)$ for some $b \in \mathbb{Z}$).

Rat.comap_cast_atTop theorem

[Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] : comap ((↑) : ℚ → R) atTop = atTop

Full source

@[simp]
theorem Rat.comap_cast_atTop [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] :
    comap ((↑) : ℚ → R) atTop = atTop :=
  comap_embedding_atTop (fun _ _ => Rat.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge r; ⟨n, by simpa⟩

Equality of Filters: Preimage of `atTop` under Rational Embedding in Archimedean Fields

Informal description

Let $R$ be a linear ordered field with the Archimedean property. The preimage of the filter `atTop` under the canonical embedding $\mathbb{Q} \to R$ is equal to the filter `atTop` on $\mathbb{Q}$. In other words, for a sequence $(q_n)$ in $\mathbb{Q}$, the sequence $(q_n)$ tends to infinity in $\mathbb{Q}$ if and only if the sequence $(q_n)$ tends to infinity in $R$.

Rat.comap_cast_atBot theorem

[Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] : comap ((↑) : ℚ → R) atBot = atBot

Full source

@[simp] theorem Rat.comap_cast_atBot [Field R] [LinearOrder R] [IsStrictOrderedRing R]
    [Archimedean R] :
    comap ((↑) : ℚ → R) atBot = atBot :=
  comap_embedding_atBot (fun _ _ => Rat.cast_le) fun r =>
    let ⟨n, hn⟩ := exists_nat_ge (-r)
    ⟨-n, by simpa [neg_le]⟩

Preimage of Negative Infinity Filter under Rational Embedding Equals Negative Infinity Filter on $\mathbb{Q}$

Informal description

Let $R$ be a linearly ordered field that is strictly ordered and Archimedean. The preimage of the filter `atBot` under the canonical embedding $\mathbb{Q} \to R$ is equal to `atBot` on $\mathbb{Q}$. In other words, for a rational sequence $(q_n)$, the cast sequence $(q_n : R)$ tends to $-\infty$ in $R$ if and only if $(q_n)$ tends to $-\infty$ in $\mathbb{Q}$.

tendsto_ratCast_atTop_iff theorem

 [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
  Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop

Full source

theorem tendsto_ratCast_atTop_iff [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R]
    {f : α → ℚ}
    {l : Filter α} : TendstoTendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop := by
  rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]; rfl

Equivalence of Tendency to Infinity for Rational Sequences and Their Embeddings in Archimedean Fields

Informal description

Let $R$ be a linearly ordered field with the Archimedean property, and let $f : \alpha \to \mathbb{Q}$ be a function. For any filter $l$ on $\alpha$, the composition $\mathbb{Q} \hookrightarrow R \circ f$ tends to infinity along $l$ if and only if $f$ tends to infinity along $l$. In other words, $\lim_{l} (f(n) : R) = +\infty$ if and only if $\lim_{l} f(n) = +\infty$.

tendsto_ratCast_atBot_iff theorem

 [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
  Tendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot

Full source

theorem tendsto_ratCast_atBot_iff [Field R] [LinearOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {f : α → ℚ}
    {l : Filter α} : TendstoTendsto (fun n => (f n : R)) l atBot ↔ Tendsto f l atBot := by
  rw [← @Rat.comap_cast_atBot R, tendsto_comap_iff]; rfl

Equivalence of Rational Sequence Tending to Negative Infinity Under Canonical Embedding

Informal description

Let $R$ be a linearly ordered field that is strictly ordered and Archimedean, and let $f : \alpha \to \mathbb{Q}$ be a function. For any filter $l$ on $\alpha$, the composition $\mathbb{Q} \hookrightarrow R \circ f$ tends to $-\infty$ along $l$ if and only if $f$ tends to $-\infty$ along $l$. In other words, the sequence $(f(n) : R)_{n \in \alpha}$ tends to $-\infty$ in $R$ if and only if $(f(n))_{n \in \alpha}$ tends to $-\infty$ in $\mathbb{Q}$.

Filter.Eventually.ratCast_atTop theorem

 [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atTop, p x) :
  ∀ᶠ (n : ℚ) in atTop, p n

Full source

theorem Filter.Eventually.ratCast_atTop [Field R] [LinearOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℚ) in atTop, p n := by
  rw [← Rat.comap_cast_atTop (R := R)]; exact h.comap _

Eventual Property Preservation from Reals to Rationals at Infinity

Informal description

Let $R$ be a linear ordered field with the Archimedean property and strict ordered ring structure. For any predicate $p : R \to \text{Prop}$, if $p(x)$ holds for all sufficiently large $x \in R$ (i.e., $\forall^\infty x \in R, p(x)$), then $p(n)$ holds for all sufficiently large $n \in \mathbb{Q}$ (i.e., $\forall^\infty n \in \mathbb{Q}, p(n)$).

Filter.Eventually.ratCast_atBot theorem

 [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atBot, p x) :
  ∀ᶠ (n : ℚ) in atBot, p n

Full source

theorem Filter.Eventually.ratCast_atBot [Field R] [LinearOrder R] [IsStrictOrderedRing R]
    [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atBot, p x) : ∀ᶠ (n : ℚ) in atBot, p n := by
  rw [← Rat.comap_cast_atBot (R := R)]; exact h.comap _

Eventual Property Preservation from Reals to Rationals at Negative Infinity

Informal description

Let $R$ be a linearly ordered field that is strictly ordered and Archimedean. For any predicate $p : R \to \text{Prop}$, if $p(x)$ holds for all sufficiently small $x \in R$ (i.e., $\forall^\infty x \in R, p(x)$ with respect to the `atBot` filter), then $p(n)$ holds for all sufficiently small $n \in \mathbb{Q}$ (i.e., $\forall^\infty n \in \mathbb{Q}, p(n)$ with respect to the `atBot` filter on $\mathbb{Q}$).

atTop_hasAntitoneBasis_of_archimedean theorem

 [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
  (atTop : Filter R).HasAntitoneBasis fun n : ℕ => Ici n

Full source

theorem atTop_hasAntitoneBasis_of_archimedean [Semiring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] :
    (atTop : Filter R).HasAntitoneBasis fun n : ℕ => Ici n :=
  hasAntitoneBasis_atTop.comp_mono Nat.mono_cast tendsto_natCast_atTop_atTop

Antitone Basis of `atTop` Filter in Archimedean Semirings via Natural Numbers

Informal description

Let $R$ be a linear ordered Archimedean semiring. The filter `atTop` on $R$ has an antitone basis consisting of the left-closed right-infinite intervals $[n, \infty)$ for natural numbers $n \in \mathbb{N}$. That is, the family of sets $\{[n, \infty) \mid n \in \mathbb{N}\}$ forms a decreasing basis for the filter `atTop` on $R$.

atTop_hasCountableBasis_of_archimedean theorem

 [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
  (atTop : Filter R).HasCountableBasis (fun _ : ℕ => True) fun n => Ici n

Full source

theorem atTop_hasCountableBasis_of_archimedean [Semiring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] :
    (atTop : Filter R).HasCountableBasis (fun _ : ℕ => True) fun n => Ici n :=
  ⟨atTop_hasAntitoneBasis_of_archimedean.1, to_countable _⟩

Countable Basis Characterization of `atTop` Filter in Archimedean Ordered Semirings

Informal description

Let $R$ be a linearly ordered Archimedean semiring. The filter `atTop` on $R$ has a countable basis consisting of the left-closed right-infinite intervals $[n, \infty)$ for natural numbers $n \in \mathbb{N}$. That is, the family of sets $\{[n, \infty) \mid n \in \mathbb{N}\}$ forms a countable basis for the filter `atTop` on $R$.

atBot_hasCountableBasis_of_archimedean theorem

 [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
  (atBot : Filter R).HasCountableBasis (fun _ : ℤ => True) fun m => Iic m

Full source

theorem atBot_hasCountableBasis_of_archimedean [Ring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] :
    (atBot : Filter R).HasCountableBasis (fun _ : ℤ => True) fun m => Iic m where
  countable := to_countable _
  toHasBasis :=
    atBot_basis.to_hasBasis
      (fun x _ => let ⟨m, hm⟩ := exists_int_le x; ⟨m, trivial, Iic_subset_Iic.2 hm⟩)
      fun m _ => ⟨m, trivial, Subset.rfl⟩

Countable Basis Characterization of `atBot` Filter in Archimedean Ordered Rings

Informal description

For an Archimedean ordered ring $R$, the filter `atBot` on $R$ has a countable basis consisting of all left-infinite right-closed intervals $(-\infty, m]$ for $m \in \mathbb{Z}$. That is, a set belongs to `atBot` if and only if it contains some interval $(-\infty, m]$ for an integer $m$.

atTop_isCountablyGenerated_of_archimedean instance

[Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] : (atTop : Filter R).IsCountablyGenerated

Full source

instance (priority := 100) atTop_isCountablyGenerated_of_archimedean
    [Semiring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] : (atTop : Filter R).IsCountablyGenerated :=
  atTop_hasCountableBasis_of_archimedean.isCountablyGenerated

Countable Generation of `atTop` Filter in Archimedean Ordered Semirings

Informal description

For any linearly ordered Archimedean semiring $R$, the filter `atTop` on $R$ is countably generated.

atBot_isCountablyGenerated_of_archimedean instance

[Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] : (atBot : Filter R).IsCountablyGenerated

Full source

instance (priority := 100) atBot_isCountablyGenerated_of_archimedean
    [Ring R] [PartialOrder R] [IsOrderedRing R]
    [Archimedean R] : (atBot : Filter R).IsCountablyGenerated :=
  atBot_hasCountableBasis_of_archimedean.isCountablyGenerated

Countable Generation of `atBot` Filter in Archimedean Ordered Rings

Informal description

For any Archimedean ordered ring $R$, the filter `atBot` on $R$ is countably generated.

Filter.Tendsto.const_mul_atTop' theorem

(hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => r * f x) l atTop

Full source

/-- If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
given in `Filter.Tendsto.const_mul_atTop`). -/
theorem Tendsto.const_mul_atTop' (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => r * f x) l atTop := by
  refine tendsto_atTop.2 fun b => ?_
  obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
  rw [nsmul_eq_mul'] at hn
  filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
  calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr

Positive scalar multiplication preserves divergence to infinity: $r > 0 \implies (f \to \infty \implies r \cdot f \to \infty)$

Informal description

Let $R$ be a linearly ordered archimedean semiring, $l$ a filter on a type $\alpha$, and $f : \alpha \to R$ a function. If $f$ tends to infinity along $l$ and $r$ is a positive element of $R$, then the function $x \mapsto r \cdot f(x)$ also tends to infinity along $l$.

Filter.Tendsto.atTop_mul_const' theorem

(hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atTop

Full source

/-- If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
given in `Filter.Tendsto.atTop_mul_const`). -/
theorem Tendsto.atTop_mul_const' (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atTop := by
  refine tendsto_atTop.2 fun b => ?_
  obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
  have hn' : 1 ≤ (n : R) * r := by rwa [nsmul_eq_mul] at hn
  filter_upwards [tendsto_atTop.1 hf (max b 0 * n)] with x hx
  calc
    b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr

Right multiplication by positive constant preserves divergence to infinity: $f \to \infty \implies f \cdot r \to \infty$ for $r > 0$

Informal description

Let $R$ be a linearly ordered archimedean semiring, $l$ a filter on a type $\alpha$, and $f : \alpha \to R$ a function. If $f$ tends to infinity along $l$ and $r$ is a positive element of $R$, then the function $x \mapsto f(x) \cdot r$ also tends to infinity along $l$.

Filter.Tendsto.atTop_mul_const_of_neg' theorem

(hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => f x * r) l atBot

Full source

/-- See also `Filter.Tendsto.atTop_mul_const_of_neg` for a version of this lemma for
`LinearOrderedField`s which does not require the `Archimedean` assumption. -/
theorem Tendsto.atTop_mul_const_of_neg' (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atBot := by
  simpa only [tendsto_neg_atTop_iff, mul_neg] using hf.atTop_mul_const' (neg_pos.mpr hr)

Right multiplication by negative constant reverses divergence to negative infinity: $f \to \infty \implies f \cdot r \to -\infty$ for $r < 0$

Informal description

Let $R$ be a linearly ordered field, $l$ a filter on a type $\alpha$, and $f : \alpha \to R$ a function. If $f$ tends to infinity along $l$ and $r$ is a negative element of $R$, then the function $x \mapsto f(x) \cdot r$ tends to negative infinity along $l$.

Filter.Tendsto.atBot_mul_const' theorem

(hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atBot

Full source

/-- See also `Filter.Tendsto.atBot_mul_const` for a version of this lemma for
`LinearOrderedField`s which does not require the `Archimedean` assumption. -/
theorem Tendsto.atBot_mul_const' (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atBot := by
  simp only [← tendsto_neg_atTop_iff, ← neg_mul] at hf ⊢
  exact hf.atTop_mul_const' hr

Right multiplication by positive constant preserves divergence to negative infinity: $f \to -\infty \implies f \cdot r \to -\infty$ for $r > 0$

Informal description

Let $R$ be a linearly ordered archimedean semiring, $l$ a filter on a type $\alpha$, and $f : \alpha \to R$ a function. If $f$ tends to negative infinity along $l$ and $r$ is a positive element of $R$, then the function $x \mapsto f(x) \cdot r$ also tends to negative infinity along $l$.

Filter.Tendsto.atBot_mul_const_of_neg' theorem

(hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => f x * r) l atTop

Full source

/-- See also `Filter.Tendsto.atBot_mul_const_of_neg` for a version of this lemma for
`LinearOrderedField`s which does not require the `Archimedean` assumption. -/
theorem Tendsto.atBot_mul_const_of_neg' (hr : r < 0) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x * r) l atTop := by
  simpa only [mul_neg, tendsto_neg_atBot_iff] using hf.atBot_mul_const' (neg_pos.2 hr)

Right multiplication by negative constant reverses divergence to negative infinity: $f \to -\infty \implies f \cdot r \to \infty$ for $r < 0$

Informal description

Let $R$ be a linearly ordered archimedean semiring, $l$ a filter on a type $\alpha$, and $f : \alpha \to R$ a function. If $f$ tends to negative infinity along $l$ and $r$ is a negative element of $R$, then the function $x \mapsto f(x) \cdot r$ tends to positive infinity along $l$.

Filter.Tendsto.atTop_nsmul_const theorem

{f : α → ℕ} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atTop

Full source

theorem Tendsto.atTop_nsmul_const {f : α → ℕ} (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atTop := by
  refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

Natural number scalar multiplication preserves divergence to infinity

Informal description

Let $R$ be a linearly ordered archimedean semiring and $r \in R$ with $0 < r$. For any function $f : \alpha \to \mathbb{N}$, if $f$ tends to infinity along a filter $l$, then the function $x \mapsto f(x) \cdot r$ also tends to infinity along $l$.

Filter.Tendsto.atTop_nsmul_neg_const theorem

{f : α → ℕ} (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atBot

Full source

theorem Tendsto.atTop_nsmul_neg_const {f : α → ℕ} (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atBot := by simpa using hf.atTop_nsmul_const (neg_pos.2 hr)

Natural number scalar multiplication with negative constant reverses divergence to infinity

Informal description

Let $R$ be a linearly ordered archimedean semiring and $r \in R$ with $r < 0$. For any function $f : \alpha \to \mathbb{N}$, if $f$ tends to infinity along a filter $l$, then the function $x \mapsto f(x) \cdot r$ tends to negative infinity along $l$.

Filter.Tendsto.atTop_zsmul_const theorem

{f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atTop

Full source

theorem Tendsto.atTop_zsmul_const {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atTop := by
  refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  replace hn : s ≤ (n : ℤ) • r := by simpa
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (zsmul_le_zsmul_left hr.le ha)

Integer scalar multiplication preserves divergence to infinity for positive scalars

Informal description

Let $R$ be a linearly ordered archimedean ring and $r \in R$ with $0 < r$. For any function $f : \alpha \to \mathbb{Z}$, if $f$ tends to infinity along a filter $l$, then the function $x \mapsto f(x) \cdot r$ also tends to infinity along $l$.

Filter.Tendsto.atTop_zsmul_neg_const theorem

{f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atTop) : Tendsto (fun x => f x • r) l atBot

Full source

theorem Tendsto.atTop_zsmul_neg_const {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atBot := by simpa using hf.atTop_zsmul_const (neg_pos.2 hr)

Integer scalar multiplication with negative constant reverses divergence to infinity

Informal description

Let $R$ be a linearly ordered archimedean ring and $r \in R$ with $r < 0$. For any function $f : \alpha \to \mathbb{Z}$, if $f$ tends to infinity along a filter $l$, then the function $x \mapsto f(x) \cdot r$ tends to negative infinity along $l$.

Filter.Tendsto.atBot_zsmul_const theorem

{f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atBot) : Tendsto (fun x => f x • r) l atBot

Full source

theorem Tendsto.atBot_zsmul_const {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x • r) l atBot := by
  simp only [← tendsto_neg_atTop_iff, ← neg_zsmul] at hf ⊢
  exact hf.atTop_zsmul_const hr

Integer scalar multiplication preserves divergence to negative infinity for positive scalars

Informal description

Let $R$ be a linearly ordered archimedean ring and $r \in R$ with $0 < r$. For any function $f : \alpha \to \mathbb{Z}$, if $f$ tends to negative infinity along a filter $l$, then the function $x \mapsto f(x) \cdot r$ also tends to negative infinity along $l$.

Filter.Tendsto.atBot_zsmul_neg_const theorem

{f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atBot) : Tendsto (fun x => f x • r) l atTop

Full source

theorem Tendsto.atBot_zsmul_neg_const {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atBot) :
    Tendsto (fun x => f x • r) l atTop := by simpa using hf.atBot_zsmul_const (neg_pos.2 hr)

Integer scalar multiplication with negative constant reverses divergence to negative infinity

Informal description

Let $R$ be a linearly ordered archimedean ring and $r \in R$ with $r < 0$. For any function $f : \alpha \to \mathbb{Z}$, if $f$ tends to negative infinity along a filter $l$, then the function $x \mapsto f(x) \cdot r$ tends to positive infinity along $l$.