mathlib3 documentation

order.filter.archimedean

`at_top` filter and archimedean (semi)rings/fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[simp]

theorem nat.comap_coe_at_top {R : Type u_2} [strict_ordered_semiring R] [archimedean R] :

filter.comap coe filter.at_top = filter.at_top

theorem tendsto_coe_nat_at_top_iff {α : Type u_1} {R : Type u_2} [strict_ordered_semiring R] [archimedean R] {f : α → ℕ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top

theorem tendsto_coe_nat_at_top_at_top {R : Type u_2} [strict_ordered_semiring R] [archimedean R] :

filter.tendsto coe filter.at_top filter.at_top

@[simp]

theorem int.comap_coe_at_top {R : Type u_2} [strict_ordered_ring R] [archimedean R] :

filter.comap coe filter.at_top = filter.at_top

@[simp]

theorem int.comap_coe_at_bot {R : Type u_2} [strict_ordered_ring R] [archimedean R] :

filter.comap coe filter.at_bot = filter.at_bot

theorem tendsto_coe_int_at_top_iff {α : Type u_1} {R : Type u_2} [strict_ordered_ring R] [archimedean R] {f : α → ℤ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top

theorem tendsto_coe_int_at_bot_iff {α : Type u_1} {R : Type u_2} [strict_ordered_ring R] [archimedean R] {f : α → ℤ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_bot ↔ filter.tendsto f l filter.at_bot

theorem tendsto_coe_int_at_top_at_top {R : Type u_2} [strict_ordered_ring R] [archimedean R] :

filter.tendsto coe filter.at_top filter.at_top

@[simp]

theorem rat.comap_coe_at_top {R : Type u_2} [linear_ordered_field R] [archimedean R] :

filter.comap coe filter.at_top = filter.at_top

@[simp]

theorem rat.comap_coe_at_bot {R : Type u_2} [linear_ordered_field R] [archimedean R] :

filter.comap coe filter.at_bot = filter.at_bot

theorem tendsto_coe_rat_at_top_iff {α : Type u_1} {R : Type u_2} [linear_ordered_field R] [archimedean R] {f : α → ℚ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_top ↔ filter.tendsto f l filter.at_top

theorem tendsto_coe_rat_at_bot_iff {α : Type u_1} {R : Type u_2} [linear_ordered_field R] [archimedean R] {f : α → ℚ} {l : filter α} :

filter.tendsto (λ (n : α), ↑(f n)) l filter.at_bot ↔ filter.tendsto f l filter.at_bot

theorem at_top_countable_basis_of_archimedean {R : Type u_2} [linear_ordered_semiring R] [archimedean R] :

filter.at_top.has_countable_basis (λ (n : ℕ), true) (λ (n : ℕ), set.Ici ↑n)

theorem at_bot_countable_basis_of_archimedean {R : Type u_2} [linear_ordered_ring R] [archimedean R] :

filter.at_bot.has_countable_basis (λ (m : ℤ), true) (λ (m : ℤ), set.Iic ↑m)

@[protected, instance]

def at_top_countably_generated_of_archimedean {R : Type u_2} [linear_ordered_semiring R] [archimedean R] :

filter.at_top.is_countably_generated

@[protected, instance]

def at_bot_countably_generated_of_archimedean {R : Type u_2} [linear_ordered_ring R] [archimedean R] :

filter.at_bot.is_countably_generated

theorem filter.tendsto.const_mul_at_top' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [linear_ordered_semiring R] [archimedean R] (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), r * f x) l filter.at_top

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

theorem filter.tendsto.at_top_mul_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [linear_ordered_semiring R] [archimedean R] (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), f x * r) l filter.at_top

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

theorem filter.tendsto.at_top_mul_neg_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [linear_ordered_ring R] [archimedean R] (hr : r < 0) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), f x * r) l filter.at_bot

See also filter.tendsto.at_top_mul_neg_const for a version of this lemma for linear_ordered_fields which does not require the archimedean assumption.

theorem filter.tendsto.at_bot_mul_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [linear_ordered_ring R] [archimedean R] (hr : 0 < r) (hf : filter.tendsto f l filter.at_bot) :

filter.tendsto (λ (x : α), f x * r) l filter.at_bot

See also filter.tendsto.at_bot_mul_const for a version of this lemma for linear_ordered_fields which does not require the archimedean assumption.

theorem filter.tendsto.at_bot_mul_neg_const' {α : Type u_1} {R : Type u_2} {l : filter α} {f : α → R} {r : R} [linear_ordered_ring R] [archimedean R] (hr : r < 0) (hf : filter.tendsto f l filter.at_bot) :

filter.tendsto (λ (x : α), f x * r) l filter.at_top

See also filter.tendsto.at_bot_mul_neg_const for a version of this lemma for linear_ordered_fields which does not require the archimedean assumption.

theorem filter.tendsto.at_top_nsmul_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [linear_ordered_cancel_add_comm_monoid R] [archimedean R] {f : α → ℕ} (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), f x • r) l filter.at_top

theorem filter.tendsto.at_top_nsmul_neg_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [linear_ordered_add_comm_group R] [archimedean R] {f : α → ℕ} (hr : r < 0) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), f x • r) l filter.at_bot

theorem filter.tendsto.at_top_zsmul_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [linear_ordered_add_comm_group R] [archimedean R] {f : α → ℤ} (hr : 0 < r) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), f x • r) l filter.at_top

theorem filter.tendsto.at_top_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [linear_ordered_add_comm_group R] [archimedean R] {f : α → ℤ} (hr : r < 0) (hf : filter.tendsto f l filter.at_top) :

filter.tendsto (λ (x : α), f x • r) l filter.at_bot

theorem filter.tendsto.at_bot_zsmul_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [linear_ordered_add_comm_group R] [archimedean R] {f : α → ℤ} (hr : 0 < r) (hf : filter.tendsto f l filter.at_bot) :

filter.tendsto (λ (x : α), f x • r) l filter.at_bot

theorem filter.tendsto.at_bot_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : filter α} {r : R} [linear_ordered_add_comm_group R] [archimedean R] {f : α → ℤ} (hr : r < 0) (hf : filter.tendsto f l filter.at_bot) :

filter.tendsto (λ (x : α), f x • r) l filter.at_top