A collection of specific limit computations

This file contains important specific limit computations in (semi-)normed groups/rings/spaces, as well as such computations in ℝ when the natural proof passes through a fact about normed spaces.

theorem tendsto_natCast_atTop_cobounded {α : Type u_1} [NormedRing α] [NormSMulClass ℤ α] [Nontrivial α] : Filter.Tendsto Nat.cast Filter.atTop (Bornology.cobounded α)

theorem tendsto_intCast_atBot_sup_atTop_cobounded {α : Type u_1} [NormedRing α] [NormSMulClass ℤ α] [Nontrivial α] : Filter.Tendsto Int.cast (Filter.atBot ⊔ Filter.atTop) (Bornology.cobounded α)

theorem tendsto_intCast_atBot_cobounded {α : Type u_1} [NormedRing α] [NormSMulClass ℤ α] [Nontrivial α] : Filter.Tendsto Int.cast Filter.atBot (Bornology.cobounded α)

theorem tendsto_intCast_atTop_cobounded {α : Type u_1} [NormedRing α] [NormSMulClass ℤ α] [Nontrivial α] : Filter.Tendsto Int.cast Filter.atTop (Bornology.cobounded α)

Powers

theorem isLittleO_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) : (fun (n : ℕ) => r₁ ^ n) =o[Filter.atTop] fun (n : ℕ) => r₂ ^ n

theorem isBigO_pow_pow_of_le_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ ≤ r₂) : (fun (n : ℕ) => r₁ ^ n) =O[Filter.atTop] fun (n : ℕ) => r₂ ^ n

theorem isLittleO_pow_pow_of_abs_lt_left {r₁ r₂ : ℝ} (h : |r₁| < |r₂|) : (fun (n : ℕ) => r₁ ^ n) =o[Filter.atTop] fun (n : ℕ) => r₂ ^ n

theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) : [∃ a ∈ Set.Ioo (-R) R, f =o[Filter.atTop] fun (x : ℕ) => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[Filter.atTop] fun (x : ℕ) => a ^ x, ∃ a ∈ Set.Ioo (-R) R, f =O[Filter.atTop] fun (x : ℕ) => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[Filter.atTop] fun (x : ℕ) => a ^ x, ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n, ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in Filter.atTop, |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.

theorem isLittleO_pow_const_const_pow_of_one_lt {R : Type u_2} [NormedRing R] (k : ℕ) {r : ℝ} (hr : 1 < r) : (fun (n : ℕ) => ↑n ^ k) =o[Filter.atTop] fun (n : ℕ) => r ^ n

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

theorem isLittleO_coe_const_pow_of_one_lt {R : Type u_2} [NormedRing R] {r : ℝ} (hr : 1 < r) : Nat.cast =o[Filter.atTop] fun (n : ℕ) => r ^ n

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

theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type u_2} [NormedRing R] (k : ℕ) {r₁ : R} {r₂ : ℝ} (h : ‖r₁‖ < r₂) : (fun (n : ℕ) => ↑n ^ k * r₁ ^ n) =o[Filter.atTop] fun (n : ℕ) => r₂ ^ n

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

theorem tendsto_pow_const_div_const_pow_of_one_lt (k : ℕ) {r : ℝ} (hr : 1 < r) : Filter.Tendsto (fun (n : ℕ) => ↑n ^ k / r ^ n) Filter.atTop (nhds 0)

theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr : |r| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑n ^ k * r ^ n) Filter.atTop (nhds 0)

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

theorem tendsto_const_div_pow (r : ℝ) (k : ℕ) (hk : k ≠ 0) : Filter.Tendsto (fun (n : ℕ) => r / ↑n ^ k) Filter.atTop (nhds 0)

For k ≠ 0 and a constant r the function r / n ^ k tends to zero.

theorem tendsto_pow_const_mul_const_pow_of_lt_one (k : ℕ) {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) : Filter.Tendsto (fun (n : ℕ) => ↑n ^ k * r ^ n) Filter.atTop (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.

theorem tendsto_self_mul_const_pow_of_abs_lt_one {r : ℝ} (hr : |r| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑n * r ^ n) Filter.atTop (nhds 0)

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

theorem tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) : Filter.Tendsto (fun (n : ℕ) => ↑n * r ^ n) Filter.atTop (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.

theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one {R : Type u_2} [SeminormedRing R] {x : R} (h : ‖x‖ < 1) : Filter.Tendsto (fun (n : ℕ) => x ^ n) Filter.atTop (nhds 0)

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

theorem tendsto_pow_atTop_nhds_zero_of_abs_lt_one {r : ℝ} (h : |r| < 1) : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0)

theorem tendsto_pow_atTop_nhds_zero_iff_norm_lt_one {R : Type u_2} [SeminormedRing R] [NormMulClass R] {x : R} : Filter.Tendsto (fun (n : ℕ) => x ^ n) Filter.atTop (nhds 0) ↔ ‖x‖ < 1

theorem AbsoluteValue.tendsto_div_one_add_pow_nhds_one {R : Type u_2} {S : Type u_3} [Field R] [Field S] [LinearOrder S] [TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [_i : OrderTopology S] {v : AbsoluteValue R S} {a : R} (ha : v a < 1) : Filter.Tendsto (fun (n : ℕ) => v (1 / (1 + a ^ n))) Filter.atTop (nhds 1)

v (1 / (1 + a ^n)) tends to 1 for all v : AbsoluteValue R S for fields R and S, provided v a < 1.

theorem AbsoluteValue.tendsto_div_one_add_pow_nhds_zero {R : Type u_2} {S : Type u_3} [Field R] [Field S] [LinearOrder S] [TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [_i : OrderTopology S] {v : AbsoluteValue R S} {a : R} (ha : 1 < v a) : Filter.Tendsto (fun (n : ℕ) => v (1 / (1 + a ^ n))) Filter.atTop (nhds 0)

v (1 / (1 + a ^n)) tends to 0 whenever v : AbsoluteValue R S for fields R and S, provided 1 < v a.

Geometric series

class HasSummableGeomSeries (K : Type u_4) [NormedRing K] : Prop

A normed ring has summable geometric series if, for all ξ of norm < 1, the geometric series ∑ ξ ^ n converges. This holds both in complete normed rings and in normed fields, providing a convenient abstraction of these two classes to avoid repeating the same proofs.

• summable_geometric_of_norm_lt_one (ξ : K) : ‖ξ‖ < 1 → Summable fun (n : ℕ) => ξ ^ n

theorem summable_geometric_of_norm_lt_one {K : Type u_4} [NormedRing K] [HasSummableGeomSeries K] {x : K} (h : ‖x‖ < 1) : Summable fun (n : ℕ) => x ^ n

instance instHasSummableGeomSeriesOfCompleteSpace {R : Type u_4} [NormedRing R] [CompleteSpace R] : HasSummableGeomSeries R

theorem tsum_geometric_le_of_norm_lt_one {R : Type u_4} [NormedRing 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.

theorem geom_series_mul_neg {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : (∑' (i : ℕ), x ^ i) * (1 - x) = 1

theorem mul_neg_geom_series {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : (1 - x) * ∑' (i : ℕ), x ^ i = 1

theorem geom_series_succ {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : ∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1

theorem geom_series_mul_shift {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)

theorem geom_series_mul_one_add {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : (1 + x) * ∑' (i : ℕ), x ^ i = 2 * ∑' (i : ℕ), x ^ i - 1

noncomputable def Units.oneSub {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (t : R) (h : ‖t‖ < 1) : Rˣ

In a normed ring with summable geometric series, a perturbation of 1 by an element t of distance less than 1 from 1 is a unit. Here we construct its Units structure.

Equations

• Units.oneSub t h = { val := 1 - t, inv := ∑' (n : ℕ), t ^ n, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Units.val_oneSub {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (t : R) (h : ‖t‖ < 1) : ↑(oneSub t h) = 1 - t

theorem geom_series_eq_inverse {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : ∑' (i : ℕ), x ^ i = Ring.inverse (1 - x)

theorem hasSum_geom_series_inverse {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : ‖x‖ < 1) : HasSum (fun (i : ℕ) => x ^ i) (Ring.inverse (1 - x))

theorem isUnit_one_sub_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {x : R} (h : ‖x‖ < 1) : IsUnit (1 - x)

theorem hasSum_geometric_of_norm_lt_one {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ‖ξ‖ < 1) : HasSum (fun (n : ℕ) => ξ ^ n) (1 - ξ)⁻¹

instance instHasSummableGeomSeries {K : Type u_4} [NormedDivisionRing K] : HasSummableGeomSeries K

theorem tsum_geometric_of_norm_lt_one {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ‖ξ‖ < 1) : ∑' (n : ℕ), ξ ^ n = (1 - ξ)⁻¹

theorem hasSum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹

theorem summable_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : Summable fun (n : ℕ) => r ^ n

theorem tsum_geometric_of_abs_lt_one {r : ℝ} (h : |r| < 1) : ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

@[simp]

theorem summable_geometric_iff_norm_lt_one {K : Type u_4} [NormedDivisionRing K] {ξ : K} : (Summable fun (n : ℕ) => ξ ^ n) ↔ ‖ξ‖ < 1

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

theorem summable_norm_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] {k : ℕ} {r : R} (hr : ‖r‖ < 1) {u : ℕ → ℕ} (hu : (fun (n : ℕ) => ↑(u n)) =O[Filter.atTop] fun (n : ℕ) => ↑(n ^ k)) : Summable fun (n : ℕ) => ‖↑(u n) * r ^ n‖

theorem summable_norm_pow_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ‖↑n ^ k * r ^ n‖

theorem summable_norm_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] {r : R} (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ‖r ^ n‖

theorem hasSum_choose_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))

theorem summable_choose_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ↑((n + k).choose k) * r ^ n

theorem tsum_choose_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = Ring.inverse (1 - r) ^ (k + 1)

theorem hasSum_choose_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑((n + k).choose k) * r ^ n) (1 / (1 - r) ^ (k + 1))

theorem tsum_choose_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = 1 / (1 - r) ^ (k + 1)

theorem summable_descFactorial_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ↑((n + k).descFactorial k) * r ^ n

theorem summable_pow_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable fun (n : ℕ) => ↑n ^ k * r ^ n

theorem hasSum_coe_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {x : R} (h : ‖x‖ < 1) : HasSum (fun (n : ℕ) => ↑n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, HasSum version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see hasSum_coe_mul_geometric_of_norm_lt_one.

theorem tsum_coe_mul_geometric_of_norm_lt_one' {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑n * r ^ n = r * Ring.inverse (1 - r) ^ 2

If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see tsum_coe_mul_geometric_of_norm_lt_one.

theorem hasSum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑n * r ^ n) (r / (1 - r) ^ 2)

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

theorem tsum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑n * r ^ n = r / (1 - r) ^ 2

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

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

theorem dist_partial_sum_le_of_le_geometric {α : Type u_1} [SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α} (hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) (n : ℕ) : dist (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n

theorem cauchySeq_finset_of_geometric_bound {α : Type u_1} [SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α} (hr : r < 1) (hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) : CauchySeq fun (s : Finset ℕ) => ∑ x ∈ s, 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.

theorem norm_sub_le_of_geometric_bound_of_hasSum {α : Type u_1} [SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α} (hr : r < 1) (hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) {a : α} (ha : HasSum f a) (n : ℕ) : ‖∑ x ∈ Finset.range n, 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.

@[simp]

theorem dist_partial_sum {α : Type u_1} [SeminormedAddCommGroup α] (u : ℕ → α) (n : ℕ) : dist (∑ k ∈ Finset.range (n + 1), u k) (∑ k ∈ Finset.range n, u k) = ‖u n‖

@[simp]

theorem dist_partial_sum' {α : Type u_1} [SeminormedAddCommGroup α] (u : ℕ → α) (n : ℕ) : dist (∑ k ∈ Finset.range n, u k) (∑ k ∈ Finset.range (n + 1), u k) = ‖u n‖

theorem cauchy_series_of_le_geometric {α : Type u_1} [SeminormedAddCommGroup α] {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1) (h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n) : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range n, u k

theorem NormedAddCommGroup.cauchy_series_of_le_geometric' {α : Type u_1} [SeminormedAddCommGroup α] {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1) (h : ∀ (n : ℕ), ‖u n‖ ≤ C * r ^ n) : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), u k

theorem NormedAddCommGroup.cauchy_series_of_le_geometric'' {α : Type u_1} [SeminormedAddCommGroup α] {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ} (hr₀ : 0 < r) (hr₁ : r < 1) (h : ∀ n ≥ N, ‖u n‖ ≤ C * r ^ n) : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range (n + 1), u k

theorem exists_norm_le_of_cauchySeq {α : Type u_1} [SeminormedAddCommGroup α] {f : ℕ → α} (h : CauchySeq fun (n : ℕ) => ∑ k ∈ Finset.range n, f k) : ∃ (C : ℝ), ∀ (n : ℕ), ‖f n‖ ≤ C

The term norms of any convergent series are bounded by a constant.

Summability tests based on comparison with geometric series

theorem summable_of_ratio_norm_eventually_le {α : Type u_4} [SeminormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α} {r : ℝ} (hr₁ : r < 1) (h : ∀ᶠ (n : ℕ) in Filter.atTop, ‖f (n + 1)‖ ≤ r * ‖f n‖) : Summable f

theorem summable_of_ratio_test_tendsto_lt_one {α : Type u_4} [NormedAddCommGroup α] [CompleteSpace α] {f : ℕ → α} {l : ℝ} (hl₁ : l < 1) (hf : ∀ᶠ (n : ℕ) in Filter.atTop, f n ≠ 0) (h : Filter.Tendsto (fun (n : ℕ) => ‖f (n + 1)‖ / ‖f n‖) Filter.atTop (nhds l)) : Summable f

theorem not_summable_of_ratio_norm_eventually_ge {α : Type u_4} [SeminormedAddCommGroup α] {f : ℕ → α} {r : ℝ} (hr : 1 < r) (hf : ∃ᶠ (n : ℕ) in Filter.atTop, ‖f n‖ ≠ 0) (h : ∀ᶠ (n : ℕ) in Filter.atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖) : ¬Summable f

theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type u_4} [SeminormedAddCommGroup α] {f : ℕ → α} {l : ℝ} (hl : 1 < l) (h : Filter.Tendsto (fun (n : ℕ) => ‖f (n + 1)‖ / ‖f n‖) Filter.atTop (nhds l)) : ¬Summable f

theorem summable_powerSeries_of_norm_lt {α : Type u_1} [NormedDivisionRing α] [CompleteSpace α] {f : ℕ → α} {w z : α} (h : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, f i * w ^ i) (hz : ‖z‖ < ‖w‖) : Summable fun (n : ℕ) => f n * z ^ n

If a power series converges at w, it converges absolutely at all z of smaller norm.

theorem summable_powerSeries_of_norm_lt_one {α : Type u_1} [NormedDivisionRing α] [CompleteSpace α] {f : ℕ → α} {z : α} (h : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, f i) (hz : ‖z‖ < 1) : Summable fun (n : ℕ) => f n * z ^ n

If a power series converges at 1, it converges absolutely at all z of smaller norm.

Dirichlet and alternating series tests

theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} (hfa : Monotone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) (hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b) : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, f i • z i

Dirichlet's test for monotone sequences.

theorem Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E} (hfa : Antitone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) (hzb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b) : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, f i • z i

Dirichlet's test for antitone sequences.

theorem norm_sum_neg_one_pow_le (n : ℕ) : ‖∑ i ∈ Finset.range n, (-1) ^ i‖ ≤ 1

theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : Monotone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i

The alternating series test for monotone sequences. See also Monotone.tendsto_alternating_series_of_tendsto_zero.

theorem Monotone.tendsto_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : Monotone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) : ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)

The alternating series test for monotone sequences.

theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : Antitone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) : CauchySeq fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i

The alternating series test for antitone sequences. See also Antitone.tendsto_alternating_series_of_tendsto_zero.

theorem Antitone.tendsto_alternating_series_of_tendsto_zero {f : ℕ → ℝ} (hfa : Antitone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) : ∃ (l : ℝ), Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)

The alternating series test for antitone sequences.

Partial sum bounds on alternating convergent series

theorem Monotone.tendsto_le_alternating_series {E : Type u_4} [Ring E] [PartialOrder E] [IsOrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : ℕ → E} (hfl : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfm : Monotone f) (k : ℕ) : l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i

Partial sums of an alternating monotone series with an even number of terms provide upper bounds on the limit.

theorem Monotone.alternating_series_le_tendsto {E : Type u_4} [Ring E] [PartialOrder E] [IsOrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : ℕ → E} (hfl : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfm : Monotone f) (k : ℕ) : ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i ≤ l

Partial sums of an alternating monotone series with an odd number of terms provide lower bounds on the limit.

theorem Antitone.alternating_series_le_tendsto {E : Type u_4} [Ring E] [PartialOrder E] [IsOrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : ℕ → E} (hfl : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfa : Antitone f) (k : ℕ) : ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l

Partial sums of an alternating antitone series with an even number of terms provide lower bounds on the limit.

theorem Antitone.tendsto_le_alternating_series {E : Type u_4} [Ring E] [PartialOrder E] [IsOrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : ℕ → E} (hfl : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfa : Antitone f) (k : ℕ) : l ≤ ∑ i ∈ Finset.range (2 * k + 1), (-1) ^ i * f i

Partial sums of an alternating antitone series with an odd number of terms provide upper bounds on the limit.

theorem Summable.tendsto_alternating_series_tsum {E : Type u_5} [Ring E] [UniformSpace E] [IsUniformAddGroup E] [CompleteSpace E] {f : ℕ → E} (hfs : Summable f) : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds (∑' (i : ℕ), (-1) ^ i * f i))

theorem alternating_series_error_bound {E : Type u_5} [Ring E] [LinearOrder E] [IsOrderedRing E] [UniformSpace E] [IsUniformAddGroup E] [CompleteSpace E] [OrderClosedTopology E] (f : ℕ → E) (hfa : Antitone f) (hfs : Summable f) (n : ℕ) : |∑' (i : ℕ), (-1) ^ i * f i - ∑ i ∈ Finset.range n, (-1) ^ i * f i| ≤ f n

Factorial

theorem Real.summable_pow_div_factorial (x : ℝ) : Summable fun (n : ℕ) => x ^ n / ↑n.factorial

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

Limits when f x * g x is bounded or convergent and f tends to the cobounded filter.

theorem tendsto_zero_of_isBoundedUnder_smul_of_tendsto_cobounded {α : Type u_1} {R : Type u_4} {K : Type u_5} [NormedRing K] [IsDomain K] [NormedAddCommGroup R] [Module K R] [Module.IsTorsionFree K R] [NormSMulClass K R] {f : α → K} {g : α → R} {l : Filter α} (hmul : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f x • g x‖) (hf : Filter.Tendsto f l (Bornology.cobounded K)) : Filter.Tendsto g l (nhds 0)

theorem tendsto_smul_congr_of_tendsto_left_cobounded_of_isBoundedUnder {α : Type u_1} {R : Type u_4} {K : Type u_5} [NormedRing K] [IsDomain K] [NormedAddCommGroup R] [Module K R] [Module.IsTorsionFree K R] [NormSMulClass K R] {f₁ f₂ : α → K} {g : α → R} {t : R} {l : Filter α} (hmul : Filter.Tendsto (fun (x : α) => f₁ x • g x) l (nhds t)) (hf₁ : Filter.Tendsto f₁ l (Bornology.cobounded K)) (hbdd : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (x : α) => ‖f₁ x - f₂ x‖) : Filter.Tendsto (fun (x : α) => f₂ x • g x) l (nhds t)

theorem tendsto_smul_comp_nat_floor_of_tendsto_nsmul {R : Type u_4} {K : Type u_5} [NormedRing K] [IsDomain K] [NormedAddCommGroup R] [Module K R] [Module.IsTorsionFree K R] [NormSMulClass K R] [NormSMulClass ℤ K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [HasSolidNorm K] {g : ℕ → R} {t : R} (hg : Filter.Tendsto (fun (n : ℕ) => n • g n) Filter.atTop (nhds t)) : Filter.Tendsto (fun (x : K) => x • g ⌊x⌋₊) Filter.atTop (nhds t)

theorem tendsto_smul_comp_nat_floor_of_tendsto_mul {R : Type u_4} {K : Type u_5} [NormedRing K] [NormedRing R] [Module K R] [Module.IsTorsionFree K R] [NormSMulClass K R] [NormSMulClass ℤ K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] [HasSolidNorm K] {g : ℕ → R} {t : R} (hg : Filter.Tendsto (fun (n : ℕ) => ↑n * g n) Filter.atTop (nhds t)) : Filter.Tendsto (fun (x : K) => x • g ⌊x⌋₊) Filter.atTop (nhds t)