# mathlibdocumentation

analysis.specific_limits

# A collection of specific limit computations #

theorem summable_of_absolute_convergence_real {f : } :
(∃ (r : ), filter.tendsto (λ (n : ), ∑ (i : ) in , abs (f i)) filter.at_top (𝓝 r))

### Powers #

theorem tendsto_add_one_pow_at_top_at_top_of_pos {α : Type u_1} [archimedean α] {r : α} (h : 0 < r) :
theorem tendsto_pow_at_top_at_top_of_one_lt {α : Type u_1} [archimedean α] {r : α} (h : 1 < r) :
theorem tendsto_norm_zero' {𝕜 : Type u_1} [normed_group 𝕜] :
(𝓝[{x : 𝕜 | x 0}] 0) (𝓝[] 0)
theorem normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type u_1} [normed_field 𝕜] :
filter.tendsto (λ (x : 𝕜), x⁻¹) (𝓝[{x : 𝕜 | x 0}] 0) filter.at_top
theorem tendsto_pow_at_top_nhds_0_of_lt_1 {𝕜 : Type u_1} [archimedean 𝕜] {r : 𝕜} (h₁ : 0 r) (h₂ : r < 1) :
filter.tendsto (λ (n : ), r ^ n) filter.at_top (𝓝 0)
theorem tendsto_pow_at_top_nhds_within_0_of_lt_1 {𝕜 : Type u_1} [archimedean 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) :
theorem is_o_pow_pow_of_lt_left {r₁ r₂ : } (h₁ : 0 r₁) (h₂ : r₁ < r₂) :
asymptotics.is_o (λ (n : ), r₁ ^ n) (λ (n : ), r₂ ^ n) filter.at_top
theorem is_O_pow_pow_of_le_left {r₁ r₂ : } (h₁ : 0 r₁) (h₂ : r₁ r₂) :
asymptotics.is_O (λ (n : ), r₁ ^ n) (λ (n : ), r₂ ^ n) filter.at_top
theorem is_o_pow_pow_of_abs_lt_left {r₁ r₂ : } (h : abs r₁ < abs r₂) :
asymptotics.is_o (λ (n : ), r₁ ^ n) (λ (n : ), r₂ ^ n) filter.at_top
theorem tfae_exists_lt_is_o_pow (f : ) (R : ) :
[∃ (a : ) (H : a set.Ioo (-R) R), , ∃ (a : ) (H : a R), , ∃ (a : ) (H : a set.Ioo (-R) R), , ∃ (a : ) (H : a R), , ∃ (a : ) (H : a < R) (C : ) (h₀ : 0 < C 0 < R), ∀ (n : ), abs (f n) C * a ^ n, ∃ (a : ) (H : a R) (C : ) (H : C > 0), ∀ (n : ), abs (f n) C * a ^ n, ∃ (a : ) (H : a < R), ∀ᶠ (n : ) in filter.at_top, abs (f n) a ^ n, ∃ (a : ) (H : a R), ∀ᶠ (n : ) in filter.at_top, abs (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 uniformity_basis_dist_pow_of_lt_1 {α : Type u_1} [metric_space α] {r : } (h₀ : 0 < r) (h₁ : r < 1) :
(𝓤 α).has_basis (λ (k : ), true) (λ (k : ), {p : α × α | dist p.fst p.snd < r ^ k})
theorem geom_lt {u : } {c : } (hc : 0 c) {n : } (hn : 0 < n) (h : ∀ (k : ), k < nc * u k < u (k + 1)) :
(c ^ n) * u 0 < u n
theorem geom_le {u : } {c : } (hc : 0 c) (n : ) (h : ∀ (k : ), k < nc * u k u (k + 1)) :
(c ^ n) * u 0 u n
theorem lt_geom {u : } {c : } (hc : 0 c) {n : } (hn : 0 < n) (h : ∀ (k : ), k < nu (k + 1) < c * u k) :
u n < (c ^ n) * u 0
theorem le_geom {u : } {c : } (hc : 0 c) (n : ) (h : ∀ (k : ), k < nu (k + 1) c * u k) :
u n (c ^ n) * u 0
theorem is_o_pow_const_const_pow_of_one_lt {R : Type u_1} [normed_ring R] (k : ) {r : } (hr : 1 < r) :
asymptotics.is_o (λ (n : ), n ^ k) (λ (n : ), r ^ n) filter.at_top

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

theorem is_o_coe_const_pow_of_one_lt {R : Type u_1} [normed_ring R] {r : } (hr : 1 < r) :
(λ (n : ), r ^ n) filter.at_top

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

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₂) :
asymptotics.is_o (λ (n : ), (n ^ k) * r₁ ^ n) (λ (n : ), r₂ ^ n) filter.at_top

If ∥r₁∥ < r₂, then for any naturak 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 (λ (n : ), n ^ k / r ^ n) filter.at_top (𝓝 0)
theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ) {r : } (hr : abs r < 1) :
filter.tendsto (λ (n : ), (n ^ k) * r ^ n) filter.at_top (𝓝 0)

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

theorem tendsto_at_top_of_geom_le {v : } {c : } (h₀ : 0 < v 0) (hc : 1 < c) (hu : ∀ (n : ), c * v n v (n + 1)) :

If a sequence v of real numbers satisfies k * v n ≤ v (n+1) with 1 < k, then it goes to +∞.

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 (𝓝 0)

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

theorem tendsto_pow_at_top_nhds_0_of_abs_lt_1 {r : } (h : abs r < 1) :
filter.tendsto (λ (n : ), r ^ n) filter.at_top (𝓝 0)

### Geometric series #

theorem has_sum_geometric_of_lt_1 {r : } (h₁ : 0 r) (h₂ : r < 1) :
has_sum (λ (n : ), r ^ n) (1 - r)⁻¹
theorem summable_geometric_of_lt_1 {r : } (h₁ : 0 r) (h₂ : r < 1) :
summable (λ (n : ), r ^ n)
theorem tsum_geometric_of_lt_1 {r : } (h₁ : 0 r) (h₂ : r < 1) :
∑' (n : ), r ^ n = (1 - r)⁻¹
theorem has_sum_geometric_two  :
has_sum (λ (n : ), (1 / 2) ^ n) 2
theorem summable_geometric_two  :
summable (λ (n : ), (1 / 2) ^ n)
theorem tsum_geometric_two  :
∑' (n : ), (1 / 2) ^ n = 2
theorem sum_geometric_two_le (n : ) :
∑ (i : ) in , (1 / 2) ^ i 2
theorem has_sum_geometric_two' (a : ) :
has_sum (λ (n : ), a / 2 / 2 ^ n) a
theorem summable_geometric_two' (a : ) :
summable (λ (n : ), a / 2 / 2 ^ n)
theorem tsum_geometric_two' (a : ) :
∑' (n : ), a / 2 / 2 ^ n = a
theorem nnreal.has_sum_geometric {r : ℝ≥0} (hr : r < 1) :
has_sum (λ (n : ), r ^ n) (1 - r)⁻¹
theorem nnreal.summable_geometric {r : ℝ≥0} (hr : r < 1) :
summable (λ (n : ), r ^ n)
theorem tsum_geometric_nnreal {r : ℝ≥0} (hr : r < 1) :
∑' (n : ), r ^ n = (1 - r)⁻¹
theorem ennreal.tsum_geometric (r : ℝ≥0∞) :
∑' (n : ), r ^ n = (1 - r)⁻¹

The series pow r converges to (1-r)⁻¹. For r < 1 the RHS is a finite number, and for 1 ≤ r the RHS equals ∞.

theorem has_sum_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ξ < 1) :
has_sum (λ (n : ), ξ ^ n) (1 - ξ)⁻¹
theorem summable_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ξ < 1) :
summable (λ (n : ), ξ ^ n)
theorem tsum_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ξ < 1) :
∑' (n : ), ξ ^ n = (1 - ξ)⁻¹
theorem has_sum_geometric_of_abs_lt_1 {r : } (h : abs r < 1) :
has_sum (λ (n : ), r ^ n) (1 - r)⁻¹
theorem summable_geometric_of_abs_lt_1 {r : } (h : abs r < 1) :
summable (λ (n : ), r ^ n)
theorem tsum_geometric_of_abs_lt_1 {r : } (h : abs r < 1) :
∑' (n : ), r ^ n = (1 - r)⁻¹
@[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.

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)
theorem summable_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)
theorem has_sum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_1} [normed_field 𝕜] {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.

theorem tsum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_1} [normed_field 𝕜] {r : 𝕜} (hr : r < 1) :
∑' (n : ), (n) * r ^ n = r / (1 - r) ^ 2

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

### Sequences with geometrically decaying distance in metric spaces #

In this paragraph, we discuss sequences in metric spaces or emetric spaces for which the distance between two consecutive terms decays geometrically. We show that such sequences are Cauchy sequences, and bound their distances to the limit. We also discuss series with geometrically decaying terms.

theorem cauchy_seq_of_edist_le_geometric {α : Type u_1} (r C : ℝ≥0∞) (hr : r < 1) (hC : C ) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C * r ^ n) :

If edist (f n) (f (n+1)) is bounded by C * r^n, C ≠ ∞, r < 1, then f is a Cauchy sequence.

theorem edist_le_of_edist_le_geometric_of_tendsto {α : Type u_1} (r C : ℝ≥0∞) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C * r ^ n) {a : α} (ha : (𝓝 a)) (n : ) :
edist (f n) a C * r ^ n / (1 - r)

If edist (f n) (f (n+1)) is bounded by C * r^n, then the distance from f n to the limit of f is bounded above by C * r^n / (1 - r).

theorem edist_le_of_edist_le_geometric_of_tendsto₀ {α : Type u_1} (r C : ℝ≥0∞) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C * r ^ n) {a : α} (ha : (𝓝 a)) :
edist (f 0) a C / (1 - r)

If edist (f n) (f (n+1)) is bounded by C * r^n, then the distance from f 0 to the limit of f is bounded above by C / (1 - r).

theorem cauchy_seq_of_edist_le_geometric_two {α : Type u_1} (C : ℝ≥0∞) (hC : C ) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C / 2 ^ n) :

If edist (f n) (f (n+1)) is bounded by C * 2^-n, then f is a Cauchy sequence.

theorem edist_le_of_edist_le_geometric_two_of_tendsto {α : Type u_1} (C : ℝ≥0∞) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C / 2 ^ n) {a : α} (ha : (𝓝 a)) (n : ) :
edist (f n) a 2 * C / 2 ^ n

If edist (f n) (f (n+1)) is bounded by C * 2^-n, then the distance from f n to the limit of f is bounded above by 2 * C * 2^-n.

theorem edist_le_of_edist_le_geometric_two_of_tendsto₀ {α : Type u_1} (C : ℝ≥0∞) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C / 2 ^ n) {a : α} (ha : (𝓝 a)) :
edist (f 0) a 2 * C

If edist (f n) (f (n+1)) is bounded by C * 2^-n, then the distance from f 0 to the limit of f is bounded above by 2 * C.

theorem aux_has_sum_of_le_geometric {α : Type u_1} [metric_space α] {r C : } (hr : r < 1) {f : → α} (hu : ∀ (n : ), dist (f n) (f (n + 1)) C * r ^ n) :
has_sum (λ (n : ), C * r ^ n) (C / (1 - r))
theorem cauchy_seq_of_le_geometric {α : Type u_1} [metric_space α] (r C : ) (hr : r < 1) {f : → α} (hu : ∀ (n : ), dist (f n) (f (n + 1)) C * r ^ n) :

If dist (f n) (f (n+1)) is bounded by C * r^n, r < 1, then f is a Cauchy sequence. Note that this lemma does not assume 0 ≤ C or 0 ≤ r.

theorem dist_le_of_le_geometric_of_tendsto₀ {α : Type u_1} [metric_space α] (r C : ) (hr : r < 1) {f : → α} (hu : ∀ (n : ), dist (f n) (f (n + 1)) C * r ^ n) {a : α} (ha : (𝓝 a)) :
dist (f 0) a C / (1 - r)

If dist (f n) (f (n+1)) is bounded by C * r^n, r < 1, then the distance from f n to the limit of f is bounded above by C * r^n / (1 - r).

theorem dist_le_of_le_geometric_of_tendsto {α : Type u_1} [metric_space α] (r C : ) (hr : r < 1) {f : → α} (hu : ∀ (n : ), dist (f n) (f (n + 1)) C * r ^ n) {a : α} (ha : (𝓝 a)) (n : ) :
dist (f n) a C * r ^ n / (1 - r)

If dist (f n) (f (n+1)) is bounded by C * r^n, r < 1, then the distance from f 0 to the limit of f is bounded above by C / (1 - r).

theorem cauchy_seq_of_le_geometric_two {α : Type u_1} [metric_space α] (C : ) {f : → α} (hu₂ : ∀ (n : ), dist (f n) (f (n + 1)) C / 2 / 2 ^ n) :

If dist (f n) (f (n+1)) is bounded by (C / 2) / 2^n, then f is a Cauchy sequence.

theorem dist_le_of_le_geometric_two_of_tendsto₀ {α : Type u_1} [metric_space α] (C : ) {f : → α} (hu₂ : ∀ (n : ), dist (f n) (f (n + 1)) C / 2 / 2 ^ n) {a : α} (ha : (𝓝 a)) :
dist (f 0) a C

If dist (f n) (f (n+1)) is bounded by (C / 2) / 2^n, then the distance from f 0 to the limit of f is bounded above by C.

theorem dist_le_of_le_geometric_two_of_tendsto {α : Type u_1} [metric_space α] (C : ) {f : → α} (hu₂ : ∀ (n : ), dist (f n) (f (n + 1)) C / 2 / 2 ^ n) {a : α} (ha : (𝓝 a)) (n : ) :
dist (f n) a C / 2 ^ n

If dist (f n) (f (n+1)) is bounded by (C / 2) / 2^n, then the distance from f n to the limit of f is bounded above by C / 2^n.

theorem dist_partial_sum_le_of_le_geometric {α : Type u_1} [normed_group α] {r C : } {f : → α} (hf : ∀ (n : ), f n C * r ^ n) (n : ) :
dist (∑ (i : ) in , f i) (∑ (i : ) in finset.range (n + 1), f i) C * r ^ n
theorem cauchy_seq_finset_of_geometric_bound {α : Type u_1} [normed_group α] {r C : } {f : → α} (hr : r < 1) (hf : ∀ (n : ), f n C * r ^ n) :
cauchy_seq (λ (s : , ∑ (x : ) in 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_has_sum {α : Type u_1} [normed_group α] {r C : } {f : → α} (hr : r < 1) (hf : ∀ (n : ), f n C * r ^ n) {a : α} (ha : a) (n : ) :
∑ (x : ) in , 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.

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

theorem normed_ring.tsum_geometric_of_norm_lt_1 {R : Type u_4} [normed_ring 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} [normed_ring R] (x : R) (h : x < 1) :
(∑' (i : ), x ^ i) * (1 - x) = 1
theorem mul_neg_geom_series {R : Type u_4} [normed_ring R] (x : R) (h : x < 1) :
(1 - x) * ∑' (i : ), x ^ i = 1

### Summability tests based on comparison with geometric series #

theorem summable_of_ratio_norm_eventually_le {α : Type u_1} {f : → α} {r : } (hr₁ : r < 1) (h : ∀ᶠ (n : ) in filter.at_top, f (n + 1) r * f n) :
theorem summable_of_ratio_test_tendsto_lt_one {α : Type u_1} [normed_group α] {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 (𝓝 l)) :
theorem not_summable_of_ratio_norm_eventually_ge {α : Type u_1} {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)) :
theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type u_1} {f : → α} {l : } (hl : 1 < l) (h : filter.tendsto (λ (n : ), f (n + 1) / f n) filter.at_top (𝓝 l)) :

### Positive sequences with small sums on encodable types #

def pos_sum_of_encodable {ε : } (hε : 0 < ε) (ι : Type u_1) [encodable ι] :
{ε' // (∀ (i : ι), 0 < ε' i) ∃ (c : ), has_sum ε' c c ε}

For any positive ε, define on an encodable type a positive sequence with sum less than ε

Equations
theorem nnreal.exists_pos_sum_of_encodable {ε : ℝ≥0} (hε : 0 < ε) (ι : Type u_1) [encodable ι] :
∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∃ (c : ℝ≥0), has_sum ε' c c < ε
theorem ennreal.exists_pos_sum_of_encodable {ε : ℝ≥0∞} (hε : 0 < ε) (ι : Type u_1) [encodable ι] :
∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∑' (i : ι), (ε' i) < ε