# `Filter.atTop` filter and archimedean (semi)rings/fields #

In this file we prove that for a linear ordered archimedean semiring `R` and a function `f : α → ℕ`, the function `Nat.cast ∘ f : α → R` tends to `Filter.atTop` along a filter `l` if and only if so does `f`. We also prove that `Nat.cast : ℕ → R` tends to `Filter.atTop` along `Filter.atTop`, as well as version of these two results for `ℤ` (and a ring `R`) and `ℚ` (and a field `R`).

source
@[simp]
theorem Nat.comap_cast_atTop {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
Filter.comap Nat.cast Filter.atTop = Filter.atTop
source
theorem tendsto_natCast_atTop_iff {α : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℕ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
theorem tendsto_natCast_atTop_atTop {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
Filter.Tendsto Nat.cast Filter.atTop Filter.atTop
source
theorem Filter.Eventually.natCast_atTop {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atTop, p x) :
∀ᶠ (n : ℕ) in atTop, p ↑n
source
@[simp]
theorem Int.comap_cast_atTop {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
Filter.comap Int.cast Filter.atTop = Filter.atTop
source
@[simp]
theorem Int.comap_cast_atBot {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
Filter.comap Int.cast Filter.atBot = Filter.atBot
source
theorem tendsto_intCast_atTop_iff {α : Type u_1} {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
theorem tendsto_intCast_atBot_iff {α : Type u_1} {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
source
theorem tendsto_intCast_atTop_atTop {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] :
Filter.Tendsto Int.cast Filter.atTop Filter.atTop
source
theorem Filter.Eventually.intCast_atTop {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atTop, p x) :
∀ᶠ (n : ℤ) in atTop, p ↑n
source
theorem Filter.Eventually.intCast_atBot {R : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atBot, p x) :
∀ᶠ (n : ℤ) in atBot, p ↑n
source
@[simp]
theorem Rat.comap_cast_atTop {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] :
Filter.comap Rat.cast Filter.atTop = Filter.atTop
source
@[simp]
theorem Rat.comap_cast_atBot {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] :
Filter.comap Rat.cast Filter.atBot = Filter.atBot
source
theorem tendsto_ratCast_atTop_iff {α : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
theorem tendsto_ratCast_atBot_iff {α : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
source
theorem Filter.Eventually.ratCast_atTop {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atTop, p x) :
∀ᶠ (n : ℚ) in atTop, p ↑n
source
theorem Filter.Eventually.ratCast_atBot {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in atBot, p x) :
∀ᶠ (n : ℚ) in atBot, p ↑n
source
theorem atTop_hasAntitoneBasis_of_archimedean {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
Filter.atTop.HasAntitoneBasis fun (n : ℕ) => Set.Ici ↑n
source
theorem atTop_hasCountableBasis_of_archimedean {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
Filter.atTop.HasCountableBasis (fun (x : ℕ) => True) fun (n : ℕ) => Set.Ici ↑n
source
theorem atBot_hasCountableBasis_of_archimedean {R : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
Filter.atBot.HasCountableBasis (fun (x : ℤ) => True) fun (m : ℤ) => Set.Iic ↑m
source
@[instance 100]
instance atTop_isCountablyGenerated_of_archimedean {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
Filter.atTop.IsCountablyGenerated
source
@[instance 100]
instance atBot_isCountablyGenerated_of_archimedean {R : Type u_2} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] :
Filter.atBot.IsCountablyGenerated
source
theorem Filter.map_add_atTop_eq {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (k : α) :
map (fun (a : α) => a + k) atTop = atTop
source
theorem Filter.map_sub_atTop_eq {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (k : α) :
map (fun (a : α) => a - k) atTop = atTop
source
theorem Filter.Tendsto.const_mul_atTop' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => r * f x) l atTop

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`).

source
theorem Filter.Tendsto.atTop_mul_const' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x * r) l atTop

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`).

source
theorem Filter.Tendsto.atTop_mul_const_of_neg' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] (hr : r < 0) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x * r) l atBot

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.

source
theorem Filter.Tendsto.atBot_mul_const' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] (hr : 0 < r) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => f x * r) l atBot

See also `Filter.Tendsto.atBot_mul_const` for a version of this lemma for `LinearOrderedField`s which does not require the `Archimedean` assumption.

source
theorem Filter.Tendsto.atBot_mul_const_of_neg' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] (hr : r < 0) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => f x * r) l atTop

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.

source
theorem Filter.Tendsto.atTop_nsmul_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [AddCommMonoid R] [LinearOrder R] [IsOrderedCancelAddMonoid R] [Archimedean R] {f : α → ℕ} (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x • r) l atTop
source
theorem Filter.Tendsto.atTop_nsmul_neg_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℕ} (hr : r < 0) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x • r) l atBot
source
theorem Filter.Tendsto.atTop_zsmul_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x • r) l atTop
source
theorem Filter.Tendsto.atTop_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atTop) :
Tendsto (fun (x : α) => f x • r) l atBot
source
theorem Filter.Tendsto.atBot_zsmul_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ} (hr : 0 < r) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => f x • r) l atBot
source
theorem Filter.Tendsto.atBot_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ} (hr : r < 0) (hf : Tendsto f l atBot) :
Tendsto (fun (x : α) => f x • r) l atTop