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).
@[simp]
theorem
Nat.comap_cast_atTop
{R : Type u_2}
[StrictOrderedSemiring R]
[Archimedean R]
:
Filter.comap Nat.cast Filter.atTop = Filter.atTop
theorem
tendsto_natCast_atTop_iff
{α : Type u_1}
{R : Type u_2}
[StrictOrderedSemiring R]
[Archimedean R]
{f : α → ℕ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
@[deprecated tendsto_natCast_atTop_iff]
theorem
tendsto_nat_cast_atTop_iff
{α : Type u_1}
{R : Type u_2}
[StrictOrderedSemiring R]
[Archimedean R]
{f : α → ℕ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
Alias of tendsto_natCast_atTop_iff.
theorem
tendsto_natCast_atTop_atTop
{R : Type u_2}
[OrderedSemiring R]
[Archimedean R]
:
Filter.Tendsto Nat.cast Filter.atTop Filter.atTop
@[deprecated tendsto_natCast_atTop_atTop]
theorem
tendsto_nat_cast_atTop_atTop
{R : Type u_2}
[OrderedSemiring R]
[Archimedean R]
:
Filter.Tendsto Nat.cast Filter.atTop Filter.atTop
Alias of tendsto_natCast_atTop_atTop.
theorem
Filter.Eventually.natCast_atTop
{R : Type u_2}
[OrderedSemiring R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atTop, p x)
:
∀ᶠ (n : ℕ) in Filter.atTop, p ↑n
@[deprecated Filter.Eventually.natCast_atTop]
theorem
Filter.Eventually.nat_cast_atTop
{R : Type u_2}
[OrderedSemiring R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atTop, p x)
:
∀ᶠ (n : ℕ) in Filter.atTop, p ↑n
Alias of Filter.Eventually.natCast_atTop.
@[simp]
theorem
Int.comap_cast_atTop
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
:
Filter.comap Int.cast Filter.atTop = Filter.atTop
@[simp]
theorem
Int.comap_cast_atBot
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
:
Filter.comap Int.cast Filter.atBot = Filter.atBot
theorem
tendsto_intCast_atTop_iff
{α : Type u_1}
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{f : α → ℤ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
@[deprecated tendsto_intCast_atTop_iff]
theorem
tendsto_int_cast_atTop_iff
{α : Type u_1}
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{f : α → ℤ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
Alias of tendsto_intCast_atTop_iff.
theorem
tendsto_intCast_atBot_iff
{α : Type u_1}
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{f : α → ℤ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
@[deprecated tendsto_intCast_atBot_iff]
theorem
tendsto_int_cast_atBot_iff
{α : Type u_1}
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{f : α → ℤ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
Alias of tendsto_intCast_atBot_iff.
theorem
tendsto_intCast_atTop_atTop
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
:
Filter.Tendsto Int.cast Filter.atTop Filter.atTop
@[deprecated tendsto_intCast_atTop_atTop]
theorem
tendsto_int_cast_atTop_atTop
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
:
Filter.Tendsto Int.cast Filter.atTop Filter.atTop
Alias of tendsto_intCast_atTop_atTop.
theorem
Filter.Eventually.intCast_atTop
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atTop, p x)
:
∀ᶠ (n : ℤ) in Filter.atTop, p ↑n
@[deprecated Filter.Eventually.intCast_atTop]
theorem
Filter.Eventually.int_cast_atTop
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atTop, p x)
:
∀ᶠ (n : ℤ) in Filter.atTop, p ↑n
Alias of Filter.Eventually.intCast_atTop.
theorem
Filter.Eventually.intCast_atBot
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atBot, p x)
:
∀ᶠ (n : ℤ) in Filter.atBot, p ↑n
@[deprecated Filter.Eventually.intCast_atBot]
theorem
Filter.Eventually.int_cast_atBot
{R : Type u_2}
[StrictOrderedRing R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atBot, p x)
:
∀ᶠ (n : ℤ) in Filter.atBot, p ↑n
Alias of Filter.Eventually.intCast_atBot.
@[simp]
theorem
Rat.comap_cast_atTop
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
:
Filter.comap Rat.cast Filter.atTop = Filter.atTop
@[simp]
theorem
Rat.comap_cast_atBot
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
:
Filter.comap Rat.cast Filter.atBot = Filter.atBot
theorem
tendsto_ratCast_atTop_iff
{α : Type u_1}
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{f : α → ℚ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
@[deprecated tendsto_ratCast_atTop_iff]
theorem
tendsto_rat_cast_atTop_iff
{α : Type u_1}
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{f : α → ℚ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
Alias of tendsto_ratCast_atTop_iff.
theorem
tendsto_ratCast_atBot_iff
{α : Type u_1}
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{f : α → ℚ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
@[deprecated tendsto_ratCast_atBot_iff]
theorem
tendsto_rat_cast_atBot_iff
{α : Type u_1}
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{f : α → ℚ}
{l : Filter α}
:
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
Alias of tendsto_ratCast_atBot_iff.
theorem
Filter.Eventually.ratCast_atTop
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atTop, p x)
:
∀ᶠ (n : ℚ) in Filter.atTop, p ↑n
@[deprecated Filter.Eventually.ratCast_atTop]
theorem
Filter.Eventually.rat_cast_atTop
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atTop, p x)
:
∀ᶠ (n : ℚ) in Filter.atTop, p ↑n
Alias of Filter.Eventually.ratCast_atTop.
theorem
Filter.Eventually.ratCast_atBot
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atBot, p x)
:
∀ᶠ (n : ℚ) in Filter.atBot, p ↑n
@[deprecated Filter.Eventually.ratCast_atBot]
theorem
Filter.Eventually.rat_cast_atBot
{R : Type u_2}
[LinearOrderedField R]
[Archimedean R]
{p : R → Prop}
(h : ∀ᶠ (x : R) in Filter.atBot, p x)
:
∀ᶠ (n : ℚ) in Filter.atBot, p ↑n
Alias of Filter.Eventually.ratCast_atBot.
theorem
atTop_hasCountableBasis_of_archimedean
{R : Type u_2}
[StrictOrderedSemiring R]
[Archimedean R]
:
theorem
atBot_hasCountableBasis_of_archimedean
{R : Type u_2}
[LinearOrderedRing R]
[Archimedean R]
:
@[instance 100]
instance
atTop_isCountablyGenerated_of_archimedean
{R : Type u_2}
[StrictOrderedSemiring R]
[Archimedean R]
:
Filter.atTop.IsCountablyGenerated
Equations
- ⋯ = ⋯
@[instance 100]
instance
atBot_isCountablyGenerated_of_archimedean
{R : Type u_2}
[LinearOrderedRing R]
[Archimedean R]
:
Filter.atBot.IsCountablyGenerated
Equations
- ⋯ = ⋯
theorem
Filter.Tendsto.const_mul_atTop'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedSemiring R]
[Archimedean R]
(hr : 0 < r)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => r * f x) l Filter.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).
theorem
Filter.Tendsto.atTop_mul_const'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedSemiring R]
[Archimedean R]
(hr : 0 < r)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x * r) l Filter.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).
theorem
Filter.Tendsto.atTop_mul_const_of_neg'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedRing R]
[Archimedean R]
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atBot
See also Filter.Tendsto.atTop_mul_const_of_neg for a version of this lemma for
LinearOrderedFields which does not require the Archimedean assumption.
theorem
Filter.Tendsto.atBot_mul_const'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedRing R]
[Archimedean R]
(hr : 0 < r)
(hf : Filter.Tendsto f l Filter.atBot)
:
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atBot
See also Filter.Tendsto.atBot_mul_const for a version of this lemma for
LinearOrderedFields which does not require the Archimedean assumption.
theorem
Filter.Tendsto.atBot_mul_const_of_neg'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedRing R]
[Archimedean R]
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atBot)
:
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atTop
See also Filter.Tendsto.atBot_mul_const_of_neg for a version of this lemma for
LinearOrderedFields which does not require the Archimedean assumption.
@[deprecated Filter.Tendsto.atTop_mul_const_of_neg']
theorem
Filter.Tendsto.atTop_mul_neg_const'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedRing R]
[Archimedean R]
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atBot
Alias of Filter.Tendsto.atTop_mul_const_of_neg'.
See also Filter.Tendsto.atTop_mul_const_of_neg for a version of this lemma for
LinearOrderedFields which does not require the Archimedean assumption.
@[deprecated Filter.Tendsto.atBot_mul_const_of_neg']
theorem
Filter.Tendsto.atBot_mul_neg_const'
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{f : α → R}
{r : R}
[LinearOrderedRing R]
[Archimedean R]
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atBot)
:
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atTop
Alias of Filter.Tendsto.atBot_mul_const_of_neg'.
See also Filter.Tendsto.atBot_mul_const_of_neg for a version of this lemma for
LinearOrderedFields which does not require the Archimedean assumption.
theorem
Filter.Tendsto.atTop_nsmul_const
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{r : R}
[LinearOrderedCancelAddCommMonoid R]
[Archimedean R]
{f : α → ℕ}
(hr : 0 < r)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atTop
theorem
Filter.Tendsto.atTop_nsmul_neg_const
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{r : R}
[LinearOrderedAddCommGroup R]
[Archimedean R]
{f : α → ℕ}
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atBot
theorem
Filter.Tendsto.atTop_zsmul_const
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{r : R}
[LinearOrderedAddCommGroup R]
[Archimedean R]
{f : α → ℤ}
(hr : 0 < r)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atTop
theorem
Filter.Tendsto.atTop_zsmul_neg_const
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{r : R}
[LinearOrderedAddCommGroup R]
[Archimedean R]
{f : α → ℤ}
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atTop)
:
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atBot
theorem
Filter.Tendsto.atBot_zsmul_const
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{r : R}
[LinearOrderedAddCommGroup R]
[Archimedean R]
{f : α → ℤ}
(hr : 0 < r)
(hf : Filter.Tendsto f l Filter.atBot)
:
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atBot
theorem
Filter.Tendsto.atBot_zsmul_neg_const
{α : Type u_1}
{R : Type u_2}
{l : Filter α}
{r : R}
[LinearOrderedAddCommGroup R]
[Archimedean R]
{f : α → ℤ}
(hr : r < 0)
(hf : Filter.Tendsto f l Filter.atBot)
:
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atTop