mathlib documentation

analysis.specific_limits

A collection of specific limit computations

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

Powers

theorem tendsto_add_one_pow_at_top_at_top_of_pos {α : Type u_1} [linear_ordered_semiring α] [archimedean α] {r : α} (h : 0 < r) :

theorem tendsto_pow_at_top_at_top_of_one_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] {r : α} (h : 1 < r) :

theorem tendsto_norm_zero' {𝕜 : Type u_1} [normed_group 𝕜] :
filter.tendsto norm (𝓝[{x : 𝕜 | x 0}] 0) (𝓝[set.Ioi 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} [linear_ordered_field 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {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} [linear_ordered_field 𝕜] [archimedean 𝕜] [topological_space 𝕜] [order_topology 𝕜] {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), asymptotics.is_o f (pow a) filter.at_top, ∃ (a : ) (H : a set.Ioo 0 R), asymptotics.is_o f (pow a) filter.at_top, ∃ (a : ) (H : a set.Ioo (-R) R), asymptotics.is_O f (pow a) filter.at_top, ∃ (a : ) (H : a set.Ioo 0 R), asymptotics.is_O f (pow a) filter.at_top, ∃ (a : ) (H : a < R) (C : ) (h₀ : 0 < C 0 < R), ∀ (n : ), abs (f n) C * a ^ n, ∃ (a : ) (H : a set.Ioo 0 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 set.Ioo 0 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 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 finset.range n, (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 : ennreal) :
∑' (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.

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} [emetric_space α] (r C : ennreal) (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} [emetric_space α] (r C : ennreal) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C * r ^ n) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 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} [emetric_space α] (r C : ennreal) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C * r ^ n) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 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} [emetric_space α] (C : ennreal) (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} [emetric_space α] (C : ennreal) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C / 2 ^ n) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 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} [emetric_space α] (C : ennreal) {f : → α} (hu : ∀ (n : ), edist (f n) (f (n + 1)) C / 2 ^ n) {a : α} (ha : filter.tendsto f filter.at_top (𝓝 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 : filter.tendsto f filter.at_top (𝓝 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 : filter.tendsto f filter.at_top (𝓝 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 : filter.tendsto f filter.at_top (𝓝 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 : filter.tendsto f filter.at_top (𝓝 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 finset.range n, 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 : finset ), ∑ (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 : has_sum f a) (n : ) :
∑ (x : ) in 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.

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.

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.

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

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

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 {ε : ennreal} (hε : 0 < ε) (ι : Type u_1) [encodable ι] :
∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∑' (i : ι), (ε' i) < ε

Factorial