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

theorem tendsto_coe_nat_at_top_iff {α : Type u_1} {R : Type u_2} [strict_ordered_semiring R] [archimedean R] {f : α } {l : filter α} :
theorem tendsto_coe_int_at_top_iff {α : Type u_1} {R : Type u_2} [strict_ordered_ring R] [archimedean R] {f : α } {l : filter α} :
theorem tendsto_coe_int_at_bot_iff {α : Type u_1} {R : Type u_2} [strict_ordered_ring R] [archimedean R] {f : α } {l : filter α} :
theorem tendsto_coe_rat_at_top_iff {α : Type u_1} {R : Type u_2} [linear_ordered_field R] [archimedean R] {f : α } {l : filter α} :
theorem tendsto_coe_rat_at_bot_iff {α : Type u_1} {R : Type u_2} [linear_ordered_field R] [archimedean R] {f : α } {l : filter α} :
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