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 : α} :
0 < rfilter.tendsto (λ (n : ), (r + 1) ^ n) filter.at_top filter.at_top

theorem tendsto_pow_at_top_at_top_of_one_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] {r : α} :

theorem lim_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 {r : } :
0 rr < 1filter.tendsto (λ (n : ), r ^ n) filter.at_top (𝓝 0)

theorem geom_lt {u : } {k : } (hk : 0 < k) {n : } :
(∀ (m : ), m nk * u m < u (m + 1))(k ^ (n + 1)) * u 0 < u (n + 1)

theorem tendsto_at_top_of_geom_lt {v : } {k : } :
0 < v 01 < k(∀ (n : ), k * v n < v (n + 1))filter.tendsto v filter.at_top filter.at_top

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} :
x < 1filter.tendsto (λ (n : ), x ^ n) filter.at_top (𝓝 0)

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

Geometric series

theorem has_sum_geometric_of_lt_1 {r : } :
0 rr < 1has_sum (λ (n : ), r ^ n) (1 - r)⁻¹

theorem summable_geometric_of_lt_1 {r : } :
0 rr < 1summable (λ (n : ), r ^ n)

theorem tsum_geometric_of_lt_1 {r : } :
0 rr < 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} :
r < 1has_sum (λ (n : ), r ^ n) (1 - r)⁻¹

theorem nnreal.summable_geometric {r : ℝ≥0} :
r < 1summable (λ (n : ), r ^ n)

theorem tsum_geometric_nnreal {r : ℝ≥0} :
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} :
ξ < 1has_sum (λ (n : ), ξ ^ n) (1 - ξ)⁻¹

theorem summable_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} :
ξ < 1summable (λ (n : ), ξ ^ n)

theorem tsum_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} :
ξ < 1(∑' (n : ), ξ ^ n) = (1 - ξ)⁻¹

theorem has_sum_geometric_of_abs_lt_1 {r : } :
abs r < 1has_sum (λ (n : ), r ^ n) (1 - r)⁻¹

theorem summable_geometric_of_abs_lt_1 {r : } :
abs r < 1summable (λ (n : ), r ^ n)

theorem tsum_geometric_of_abs_lt_1 {r : } :
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 : → α} :
(∀ (n : ), edist (f n) (f (n + 1)) C * r ^ n)cauchy_seq f

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 : α} :
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 : → α} :
(∀ (n : ), edist (f n) (f (n + 1)) C / 2 ^ n)cauchy_seq f

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 : α} :
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 : → α} :
(∀ (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 : → α} :
(∀ (n : ), dist (f n) (f (n + 1)) C * r ^ n)cauchy_seq f

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 : α} :
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 : → α} :
(∀ (n : ), dist (f n) (f (n + 1)) C / 2 / 2 ^ n)cauchy_seq f

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 : α} :

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 : → α} :
r < 1(∀ (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) :
x < 1summable (λ (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) :
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) :
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) :
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

Harmonic series

Here we define the harmonic series and prove some basic lemmas about it, leading to a proof of its divergence to +∞

def harmonic_series  :

The harmonic series 1 + 1/2 + 1/3 + ... + 1/n

Equations

The harmonic series diverges to +∞