analysis.specific_limits.normed

theorem tendsto_norm_zero' {𝕜 : Type u_1} [normed_add_comm_group 𝕜] :

filter.tendsto has_norm.norm (nhds_within 0 {0}ᶜ) (nhds_within 0 (set.Ioi 0))

source

theorem normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type u_1} [normed_field 𝕜] :

filter.tendsto (λ (x : 𝕜), ‖x⁻¹ ‖) (nhds_within 0 {0}ᶜ) filter.at_top

source

theorem normed_field.tendsto_norm_zpow_nhds_within_0_at_top {𝕜 : Type u_1} [normed_field 𝕜] {m : ℤ} (hm : m < 0) :

filter.tendsto (λ (x : 𝕜), ‖x ^ m‖) (nhds_within 0 {0}ᶜ) filter.at_top

source

theorem normed_field.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι : Type u_1} {𝕜 : Type u_2} {𝔸 : Type u_3} [normed_field 𝕜] [normed_add_comm_group 𝔸] [normed_space 𝕜 𝔸] {l : filter ι} {ε : ι → 𝕜} {f : ι → 𝔸} (hε : filter.tendsto ε l (nhds 0)) (hf : filter.is_bounded_under has_le.le l (has_norm.norm ∘ f)) :

filter.tendsto (ε • f) l (nhds 0)

The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.

source

@[simp]

theorem normed_field.continuous_at_zpow {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {m : ℤ} {x : 𝕜} :

continuous_at (λ (x : 𝕜), x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m

source

@[simp]

theorem normed_field.continuous_at_inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {x : 𝕜} :

continuous_at has_inv.inv x ↔ x ≠ 0

source

theorem is_o_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) :

(λ (n : ℕ), r₁ ^ n) =o[filter.at_top ] λ (n : ℕ), r₂ ^ n

source

theorem is_O_pow_pow_of_le_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ ≤ r₂) :

(λ (n : ℕ), r₁ ^ n) =O[filter.at_top ] λ (n : ℕ), r₂ ^ n

source

theorem is_o_pow_pow_of_abs_lt_left {r₁ r₂ : ℝ} (h : |r₁| < |r₂|) :

(λ (n : ℕ), r₁ ^ n) =o[filter.at_top ] λ (n : ℕ), r₂ ^ n

source

theorem tfae_exists_lt_is_o_pow (f : ℕ → ℝ) (R : ℝ) :

[∃ (a : ℝ) (H : a ∈ set.Ioo (-R) R), f =o[filter.at_top ] has_pow.pow a, ∃ (a : ℝ) (H : a ∈ set.Ioo 0 R), f =o[filter.at_top ] has_pow.pow a, ∃ (a : ℝ) (H : a ∈ set.Ioo (-R) R), f =O[filter.at_top ] has_pow.pow a, ∃ (a : ℝ) (H : a ∈ set.Ioo 0 R), f =O[filter.at_top ] has_pow.pow a, ∃ (a : ℝ) (H : a < R) (C : ℝ) (h₀ : 0 < C ∨ 0 < R), ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ (a : ℝ) (H : a ∈ set.Ioo 0 R) (C : ℝ) (H : C > 0), ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ (a : ℝ) (H : a < R), ∀ᶠ (n : ℕ) in filter.at_top , |f n| ≤ a ^ n, ∃ (a : ℝ) (H : a ∈ set.Ioo 0 R), ∀ᶠ (n : ℕ) in filter.at_top , |f n| ≤ a ^ n].tfae

Various statements equivalent to the fact that f n grows exponentially slower than R ^ n.

0: $f n = o(a ^ n)$ for some $-R < a < R$;
1: $f n = o(a ^ n)$ for some $0 < a < R$;
2: $f n = O(a ^ n)$ for some $-R < a < R$;
3: $f n = O(a ^ n)$ for some $0 < a < R$;
4: there exist a < R and C such that one of C and R is positive and $|f n| ≤ Ca^n$ for all n;
5: there exists 0 < a < R and a positive C such that $|f n| ≤ Ca^n$ for all n;
6: there exists a < R such that $|f n| ≤ a ^ n$ for sufficiently large n;
7: there exists 0 < a < R such that $|f n| ≤ a ^ n$ for sufficiently large n.

NB: For backwards compatibility, if you add more items to the list, please append them at the end of the list.

source

theorem is_o_pow_const_const_pow_of_one_lt {R : Type u_1} [normed_ring R] (k : ℕ) {r : ℝ} (hr : 1 < r) :

(λ (n : ℕ), ↑n ^ k) =o[filter.at_top ] λ (n : ℕ), r ^ n

For any natural k and a real r > 1 we have n ^ k = o(r ^ n) as n → ∞.

source

theorem is_o_coe_const_pow_of_one_lt {R : Type u_1} [normed_ring R] {r : ℝ} (hr : 1 < r) :

coe =o[filter.at_top ] λ (n : ℕ), r ^ n

For a real r > 1 we have n = o(r ^ n) as n → ∞.

source

theorem is_o_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type u_1} [normed_ring R] (k : ℕ) {r₁ : R} {r₂ : ℝ} (h : ‖r₁‖ < r₂) :

(λ (n : ℕ), ↑n ^ k * r₁ ^ n) =o[filter.at_top ] λ (n : ℕ), r₂ ^ n

If ‖r₁‖ < r₂, then for any naturak k we have n ^ k r₁ ^ n = o (r₂ ^ n) as n → ∞.

source

theorem tendsto_pow_const_div_const_pow_of_one_lt (k : ℕ) {r : ℝ} (hr : 1 < r) :

filter.tendsto (λ (n : ℕ), ↑n ^ k / r ^ n) filter.at_top (nhds 0)

source

theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr : |r| < 1) :

filter.tendsto (λ (n : ℕ), ↑n ^ k * r ^ n) filter.at_top (nhds 0)

If |r| < 1, then n ^ k r ^ n tends to zero for any natural k.

source

theorem tendsto_pow_const_mul_const_pow_of_lt_one (k : ℕ) {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :

filter.tendsto (λ (n : ℕ), ↑n ^ k * r ^ n) filter.at_top (nhds 0)

If 0 ≤ r < 1, then n ^ k r ^ n tends to zero for any natural k. This is a specialized version of tendsto_pow_const_mul_const_pow_of_abs_lt_one, singled out for ease of application.

source

theorem tendsto_self_mul_const_pow_of_abs_lt_one {r : ℝ} (hr : |r| < 1) :

filter.tendsto (λ (n : ℕ), ↑n * r ^ n) filter.at_top (nhds 0)

If |r| < 1, then n * r ^ n tends to zero.

source

theorem tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :

filter.tendsto (λ (n : ℕ), ↑n * r ^ n) filter.at_top (nhds 0)

If 0 ≤ r < 1, then n * r ^ n tends to zero. This is a specialized version of tendsto_self_mul_const_pow_of_abs_lt_one, singled out for ease of application.

source

theorem tendsto_pow_at_top_nhds_0_of_norm_lt_1 {R : Type u_1} [normed_ring R] {x : R} (h : ‖x‖ < 1) :

filter.tendsto (λ (n : ℕ), x ^ n) filter.at_top (nhds 0)

In a normed ring, the powers of an element x with ‖x‖ < 1 tend to zero.

source

theorem tendsto_pow_at_top_nhds_0_of_abs_lt_1 {r : ℝ} (h : |r| < 1) :

filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (nhds 0)

source

theorem has_sum_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ‖ξ‖ < 1) :

has_sum (λ (n : ℕ), ξ ^ n) (1 - ξ)⁻¹

source

theorem summable_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ‖ξ‖ < 1) :

summable (λ (n : ℕ), ξ ^ n)

source

theorem tsum_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ‖ξ‖ < 1) :

∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹

source

theorem has_sum_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) :

has_sum (λ (n : ℕ), r ^ n) (1 - r)⁻¹

source

theorem summable_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) :

summable (λ (n : ℕ), r ^ n)

source

theorem tsum_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) :

∑' (n : ℕ), r ^ n = (1 - r)⁻¹

source

@[simp]

theorem summable_geometric_iff_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} :

summable (λ (n : ℕ), ξ ^ n) ↔ ‖ξ‖ < 1

A geometric series in a normed field is summable iff the norm of the common ratio is less than one.

source

theorem summable_norm_pow_mul_geometric_of_norm_lt_1 {R : Type u_1} [normed_ring R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) :

summable (λ (n : ℕ), ‖↑n ^ k * r ^ n‖)

source

theorem summable_pow_mul_geometric_of_norm_lt_1 {R : Type u_1} [normed_ring R] [complete_space R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) :

summable (λ (n : ℕ), ↑n ^ k * r ^ n)

source

theorem has_sum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_1} [normed_field 𝕜] [complete_space 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) :

has_sum (λ (n : ℕ), ↑n * r ^ n) (r / (1 - r) ^ 2)

If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, has_sum version.

source

theorem tsum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_1} [normed_field 𝕜] [complete_space 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) :

∑' (n : ℕ), ↑n * r ^ n = r / (1 - r) ^ 2

If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2.

source

theorem seminormed_add_comm_group.cauchy_seq_of_le_geometric {α : Type u_1} [seminormed_add_comm_group α] {C r : ℝ} (hr : r < 1) {u : ℕ → α} (h : ∀ (n : ℕ), ‖u n - u (n + 1)‖ ≤ C * r ^ n) :

cauchy_seq u

source

theorem dist_partial_sum_le_of_le_geometric {α : Type u_1} [seminormed_add_comm_group α] {r C : ℝ} {f : ℕ → α} (hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) (n : ℕ) :

has_dist.dist ((finset.range n).sum (λ (i : ℕ), f i)) ((finset.range (n + 1)).sum (λ (i : ℕ), f i)) ≤ C * r ^ n

source

theorem cauchy_seq_finset_of_geometric_bound {α : Type u_1} [seminormed_add_comm_group α] {r C : ℝ} {f : ℕ → α} (hr : r < 1) (hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) :

cauchy_seq (λ (s : finset ℕ), s.sum (λ (x : ℕ), f x))

If ‖f n‖ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f form a Cauchy sequence. This lemma does not assume 0 ≤ r or 0 ≤ C.

source

theorem norm_sub_le_of_geometric_bound_of_has_sum {α : Type u_1} [seminormed_add_comm_group α] {r C : ℝ} {f : ℕ → α} (hr : r < 1) (hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) {a : α} (ha : has_sum f a) (n : ℕ) :

‖(finset.range n).sum (λ (x : ℕ), f x) - a‖ ≤ C * r ^ n / (1 - r)

If ‖f n‖ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f are within distance C * r ^ n / (1 - r) of the sum of the series. This lemma does not assume 0 ≤ r or 0 ≤ C.

source

@[simp]

theorem dist_partial_sum {α : Type u_1} [seminormed_add_comm_group α] (u : ℕ → α) (n : ℕ) :

has_dist.dist ((finset.range (n + 1)).sum (λ (k : ℕ), u k)) ((finset.range n).sum (λ (k : ℕ), u k)) = ‖u n‖

source

@[simp]

theorem dist_partial_sum' {α : Type u_1} [seminormed_add_comm_group α] (u : ℕ → α) (n : ℕ) :

has_dist.dist ((finset.range n).sum (λ (k : ℕ), u k)) ((finset.range (n + 1)).sum (λ (k : ℕ), u k)) = ‖u n‖

source

theorem cauchy_series_of_le_geometric {α : Type u_1} [seminormed_add_comm_group α] {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1) (h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n) :

cauchy_seq (λ (n : ℕ), (finset.range n).sum (λ (k : ℕ), u k))

source

theorem normed_add_comm_group.cauchy_series_of_le_geometric' {α : Type u_1} [seminormed_add_comm_group α] {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1) (h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n) :

cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), u k))

source

theorem normed_add_comm_group.cauchy_series_of_le_geometric'' {α : Type u_1} [seminormed_add_comm_group α] {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ} (hr₀ : 0 < r) (hr₁ : r < 1) (h : ∀ (n : ℕ), n ≥ N → ‖u n‖ ≤ C * r ^ n) :

cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (k : ℕ), u k))

source

theorem normed_ring.summable_geometric_of_norm_lt_1 {R : Type u_4} [normed_ring R] [complete_space R] (x : R) (h : ‖x‖ < 1) :

summable (λ (n : ℕ), x ^ n)

A geometric series in a complete normed ring is summable. Proved above (same name, different namespace) for not-necessarily-complete normed fields.

source

theorem normed_ring.tsum_geometric_of_norm_lt_1 {R : Type u_4} [normed_ring R] [complete_space R] (x : R) (h : ‖x‖ < 1) :

‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹

Bound for the sum of a geometric series in a normed ring. This formula does not assume that the normed ring satisfies the axiom ‖1‖ = 1.

source

theorem geom_series_mul_neg {R : Type u_4} [normed_ring R] [complete_space R] (x : R) (h : ‖x‖ < 1) :

(∑' (i : ℕ), x ^ i) * (1 - x) = 1

source

theorem mul_neg_geom_series {R : Type u_4} [normed_ring R] [complete_space R] (x : R) (h : ‖x‖ < 1) :

(1 - x) * ∑' (i : ℕ), x ^ i = 1

source

theorem summable_of_ratio_norm_eventually_le {α : Type u_1} [seminormed_add_comm_group α] [complete_space α] {f : ℕ → α} {r : ℝ} (hr₁ : r < 1) (h : ∀ᶠ (n : ℕ) in filter.at_top , ‖f (n + 1)‖ ≤ r * ‖f n‖) :

summable f

source

theorem summable_of_ratio_test_tendsto_lt_one {α : Type u_1} [normed_add_comm_group α] [complete_space α] {f : ℕ → α} {l : ℝ} (hl₁ : l < 1) (hf : ∀ᶠ (n : ℕ) in filter.at_top , f n ≠ 0) (h : filter.tendsto (λ (n : ℕ), ‖f (n + 1)‖ / ‖f n‖) filter.at_top (nhds l)) :

summable f

source

theorem not_summable_of_ratio_norm_eventually_ge {α : Type u_1} [seminormed_add_comm_group α] {f : ℕ → α} {r : ℝ} (hr : 1 < r) (hf : ∃ᶠ (n : ℕ) in filter.at_top , ‖f n‖ ≠ 0) (h : ∀ᶠ (n : ℕ) in filter.at_top , r * ‖f n‖ ≤ ‖f (n + 1)‖) :

¬summable f

source

theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type u_1} [seminormed_add_comm_group α] {f : ℕ → α} {l : ℝ} (hl : 1 < l) (h : filter.tendsto (λ (n : ℕ), ‖f (n + 1)‖ / ‖f n‖) filter.at_top (nhds l)) :

¬summable f

source

theorem monotone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} (hfa : monotone f) (hf0 : filter.tendsto f filter.at_top (nhds 0)) (hgb : ∀ (n : ℕ), ‖(finset.range n).sum (λ (i : ℕ), z i)‖ ≤ b) :

cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), f i • z i))

Dirichlet's Test for monotone sequences.

source

theorem antitone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded {E : Type u_4} [normed_add_comm_group E] [normed_space ℝ E] {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} (hfa : antitone f) (hf0 : filter.tendsto f filter.at_top (nhds 0)) (hzb : ∀ (n : ℕ), ‖(finset.range n).sum (λ (i : ℕ), z i)‖ ≤ b) :

cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), f i • z i))

Dirichlet's test for antitone sequences.

source

theorem norm_sum_neg_one_pow_le (n : ℕ) :

‖(finset.range n).sum (λ (i : ℕ), (-1) ^ i)‖ ≤ 1

source

theorem monotone.cauchy_seq_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : monotone f) (hf0 : filter.tendsto f filter.at_top (nhds 0)) :

cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), (-1) ^ i * f i))

The alternating series test for monotone sequences. See also tendsto_alternating_series_of_monotone_tendsto_zero.

source

theorem monotone.tendsto_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : monotone f) (hf0 : filter.tendsto f filter.at_top (nhds 0)) :

∃ (l : ℝ), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), (-1) ^ i * f i)) filter.at_top (nhds l)

The alternating series test for monotone sequences.

source

theorem antitone.cauchy_seq_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : antitone f) (hf0 : filter.tendsto f filter.at_top (nhds 0)) :

cauchy_seq (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), (-1) ^ i * f i))

The alternating series test for antitone sequences. See also tendsto_alternating_series_of_antitone_tendsto_zero.

source

theorem antitone.tendsto_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : antitone f) (hf0 : filter.tendsto f filter.at_top (nhds 0)) :

∃ (l : ℝ), filter.tendsto (λ (n : ℕ), (finset.range (n + 1)).sum (λ (i : ℕ), (-1) ^ i * f i)) filter.at_top (nhds l)

The alternating series test for antitone sequences.

source

theorem real.summable_pow_div_factorial (x : ℝ) :

summable (λ (n : ℕ), x ^ n / ↑(n.factorial))

The series ∑' n, x ^ n / n! is summable of any x : ℝ. See also exp_series_div_summable for a version that also works in ℂ, and exp_series_summable' for a version that works in any normed algebra over ℝ or ℂ.

source

theorem real.tendsto_pow_div_factorial_at_top (x : ℝ) :

filter.tendsto (λ (n : ℕ), x ^ n / ↑(n.factorial)) filter.at_top (nhds 0)

mathlib3 documentation

A collection of specific limit computations #

Powers #

Geometric series #

Summability tests based on comparison with geometric series #

Dirichlet and alternating series tests #

Factorial #