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) [NonUnitalNormedRing K] : Prop

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

Due to the fact that Mathlib has no Pow G ℕ+ instance for semigroups, this is currently stated using iterated multiplication. Once semigroups implement this bundled Pow instance, then we can switch the statements to use that instead, and improve the proofs.

• summable_geometric_of_norm_lt_one (ξ : K) : ‖ξ‖ < 1 → Summable fun (x : ℕ) => (fun (x : K) => x * ξ)^[x] ξ

theorem hasSummableGeomSeries_iff_summable_iterate_mul (K : Type u_4) [NonUnitalNormedRing K] : HasSummableGeomSeries K ↔ ∀ (ξ : K), ‖ξ‖ < 1 → Summable fun (x : ℕ) => (fun (x : K) => x * ξ)^[x] ξ

theorem summable_iterate_mul_of_norm_lt_one {R : Type u_4} [NonUnitalNormedRing R] [HasSummableGeomSeries R] {x : R} (h : ‖x‖ < 1) : Summable fun (x_1 : ℕ) => (fun (x_2 : R) => x_2 * x)^[x_1] x

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

theorem Summable.add_geom_series_mul_self {R : Type u_4} [NonUnitalNormedRing R] {x : R} (h : Summable fun (x_1 : ℕ) => (fun (x_2 : R) => x_2 * x)^[x_1] x) : x + (∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x) * x = ∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x

theorem Summable.add_self_mul_geom_series {R : Type u_4} [NonUnitalNormedRing R] {x : R} (h : Summable fun (x_1 : ℕ) => (fun (x_2 : R) => x_2 * x)^[x_1] x) : x + x * ∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x = ∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x

theorem tsum_iterate_mul_le_of_norm_lt_one {R : Type u_4} [NonUnitalNormedRing R] (x : R) (h : ‖x‖ < 1) : ‖∑' (n : ℕ), (fun (x_1 : R) => x_1 * x)^[n] x‖ ≤ ‖x‖ / (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 summable_iterate_mul_iff_isQuasiregular {R : Type u_4} [NonUnitalNormedRing R] {x : R} (h : ‖x‖ < 1) : (Summable fun (x_1 : ℕ) => (fun (x_2 : R) => x_2 * x)^[x_1] x) ↔ IsQuasiregular (-x)

If ‖x‖ < 1 and x lies in a non-unital normed ring, then ∑' n : ℕ, x ^ (n + 1) is summable if and only if -x is quasiregular.

theorem hasSummableGeomSeries_iff_isQuasiregular {R : Type u_4} [NonUnitalNormedRing R] : HasSummableGeomSeries R ↔ ∀ ⦃x : R⦄, ‖x‖ < 1 → IsQuasiregular x

A non-unital normed ring R has summable geometric series if and only if every element of in the open unit ball is quasiregular.

theorem IsQuasiregular.of_norm_lt_one {R : Type u_4} [NonUnitalNormedRing R] [HasSummableGeomSeries R] {x : R} (h : ‖x‖ < 1) : IsQuasiregular x

theorem add_geom_series_mul_self {R : Type u_4} [NonUnitalNormedRing R] [HasSummableGeomSeries R] {x : R} (hx : ‖x‖ < 1) : x + (∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x) * x = ∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x

theorem add_self_mul_geom_series {R : Type u_4} [NonUnitalNormedRing R] [HasSummableGeomSeries R] {x : R} (hx : ‖x‖ < 1) : x + x * ∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x = ∑' (i : ℕ), (fun (x_1 : R) => x_1 * x)^[i] x

theorem hasSummableGeomSeries_iff_summable_pow {R : Type u_4} [NormedRing R] : HasSummableGeomSeries R ↔ ∀ ⦃ξ : R⦄, ‖ξ‖ < 1 → Summable fun (n : ℕ) => ξ ^ n

theorem HasSummableGeomSeries.of_summable_pow {R : Type u_4} [NormedRing R] : (∀ ⦃ξ : R⦄, ‖ξ‖ < 1 → Summable fun (n : ℕ) => ξ ^ n) → HasSummableGeomSeries R

Alias of the reverse direction of hasSummableGeomSeries_iff_summable_pow.

theorem hasSummableGeomSeries_iff_isUnit {R : Type u_4} [NormedRing R] : HasSummableGeomSeries R ↔ ∀ ⦃x : R⦄, ‖x‖ < 1 → IsUnit (1 - x)

If ‖x‖ < 1 and x lies in a normed ring, then ∑' n : ℕ, x ^ n is summable if and only if 1 - x is invertible.

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 IsUnit.one_sub_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {x : R} (hx : ‖x‖ < 1) : IsUnit (1 - x)

The element 1 - x also available bundled as a term of Rˣ with inverse ∑' n : ℕ, x ^ n in Units.oneSub.

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

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 hasSum_descFactorial_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (j : ℕ) {r : R} (h : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑(n.descFactorial j) * r ^ n) (↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1))

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

HasSum version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see hasSum_descFactorial_mul_geometric_of_norm_lt_one.

theorem tsum_descFactorial_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (j : ℕ) {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑(n.descFactorial j) * r ^ n = ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1)

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

This is the version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see tsum_descFactorial_mul_geometric_of_norm_lt_one.

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

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

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

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

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

theorem hasSum_pow_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (h : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑n ^ k * r ^ n) (∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1))

If ‖r‖ < 1, then ∑' n : ℕ, n ^ k * r ^ n is given by the finite sum ∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j * (1 - r)⁻¹ʳ ^ (j + 1), where S(k, j) denotes the Stirling numbers of the second kind.

HasSum version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see hasSum_pow_mul_geometric_of_norm_lt_one.

theorem tsum_pow_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ k * r ^ n = ∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j * Ring.inverse (1 - r) ^ (j + 1)

If ‖r‖ < 1, then ∑' n : ℕ, n ^ k * r ^ n is given by the finite sum ∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j * (1 - r)⁻¹ʳ ^ (j + 1), where S(k, j) denotes the Stirling numbers of the second kind.

Version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see tsum_pow_mul_geometric_of_norm_lt_one.

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_pow_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑n ^ k * r ^ n) (∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j / (1 - r) ^ (j + 1))

If ‖r‖ < 1, then ∑' n : ℕ, n ^ k * r ^ n is given by the finite sum ∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j / (1 - r) ^ (j + 1), where S(k, j) denotes the Stirling numbers of the second kind.

theorem tsum_pow_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ k * r ^ n = ∑ j ∈ Finset.range (k + 1), ↑(k.stirlingSecond j) * ↑j.factorial * r ^ j / (1 - r) ^ (j + 1)

If ‖r‖ < 1, then ∑' n : ℕ, n ^ k * r ^ n is given by the finite sum ∑ j ∈ range (k + 1), S(k, j) * j ! * r ^ j / (1 - r) ^ (j + 1), where S(k, j) denotes the Stirling numbers of the second kind.

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.

This is the 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.

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 hasSum_sq_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {r : R} (h : ‖r‖ < 1) : HasSum (fun (n : ℕ) => ↑n ^ 2 * r ^ n) (r * (1 + r) * Ring.inverse (1 - r) ^ 3)

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

HasSum version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see hasSum_sq_mul_geometric_of_norm_lt_one.

theorem tsum_sq_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {r : R} (h : ‖r‖ < 1) : ∑' (n : ℕ), ↑n ^ 2 * r ^ n = r * (1 + r) * Ring.inverse (1 - r) ^ 3

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

This is the version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see tsum_sq_mul_geometric_of_norm_lt_one.

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

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

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

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

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)