mathlib documentation

analysis.specific_limits

A collection of specific limit computations

source
theorem tendsto_norm_at_top_at_top  :
filter.tendsto norm filter.at_top filter.at_top

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

source
theorem tendsto_inverse_at_top_nhds_0_nat  :
filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (𝓝 0)

source
theorem tendsto_const_div_at_top_nhds_0_nat (C : ℝ) :
filter.tendsto (λ (n : ℕ), C / ↑n) filter.at_top (𝓝 0)

source
theorem nnreal.tendsto_inverse_at_top_nhds_0_nat  :
filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (𝓝 0)

source
theorem nnreal.tendsto_const_div_at_top_nhds_0_nat (C : ℝ≥0) :
filter.tendsto (λ (n : ℕ), C / ↑n) filter.at_top (𝓝 0)

source
theorem tendsto_one_div_add_at_top_nhds_0_nat  :
filter.tendsto (λ (n : ℕ), 1 / (↑n + 1)) filter.at_top (𝓝 0)

Powers

source
theorem tendsto_add_one_pow_at_top_at_top_of_pos {α : Type u_1} [linear_ordered_semiring α] [archimedean α] {r : α} (h : 0 < r) :
filter.tendsto (λ (n : ℕ), (r + 1) ^ n) filter.at_top filter.at_top

source
theorem tendsto_pow_at_top_at_top_of_one_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] {r : α} (h : 1 < r) :
filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top filter.at_top

source
theorem nat.tendsto_pow_at_top_at_top_of_one_lt {m : ℕ} (h : 1 < m) :
filter.tendsto (λ (n : ℕ), m ^ n) filter.at_top filter.at_top

source
theorem lim_norm_zero' {𝕜 : Type u_1} [normed_group 𝕜] :
filter.tendsto norm (𝓝[{x : 𝕜 | x ≠ 0}] 0) (𝓝[set.Ioi 0] 0)

source
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

source
theorem tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (𝓝 0)

source
theorem geom_lt {u : ℕ → ℝ} {k : ℝ} (hk : 0 < k) {n : ℕ} (h : ∀ (m : ℕ), m ≤ n → k * u m < u (m + 1)) :
(k ^ (n + 1)) * u 0 < u (n + 1)

source
theorem tendsto_at_top_of_geom_lt {v : ℕ → ℝ} {k : ℝ} (h₀ : 0 < v 0) (hk : 1 < k) (hu : ∀ (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 +∞.

source
theorem nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ≥0} (hr : r < 1) :
filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (𝓝 0)

source
theorem ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 {r : ennreal} (hr : r < 1) :
filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (𝓝 0)

source
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.

source
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

source
theorem has_sum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
has_sum (λ (n : ℕ), r ^ n) (1 - r)⁻¹

source
theorem summable_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
summable (λ (n : ℕ), r ^ n)

source
theorem tsum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
(∑' (n : ℕ), r ^ n) = (1 - r)⁻¹

source
theorem has_sum_geometric_two  :
has_sum (λ (n : ℕ), (1 / 2) ^ n) 2

source
theorem summable_geometric_two  :
summable (λ (n : ℕ), (1 / 2) ^ n)

source
theorem tsum_geometric_two  :
(∑' (n : ℕ), (1 / 2) ^ n) = 2

source
theorem sum_geometric_two_le (n : ℕ) :
∑ (i : ℕ) in finset.range n, (1 / 2) ^ i ≤ 2

source
theorem has_sum_geometric_two' (a : ℝ) :
has_sum (λ (n : ℕ), a / 2 / 2 ^ n) a

source
theorem summable_geometric_two' (a : ℝ) :
summable (λ (n : ℕ), a / 2 / 2 ^ n)

source
theorem tsum_geometric_two' (a : ℝ) :
(∑' (n : ℕ), a / 2 / 2 ^ n) = a

source
theorem nnreal.has_sum_geometric {r : ℝ≥0} (hr : r < 1) :
has_sum (λ (n : ℕ), r ^ n) (1 - r)⁻¹

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

source
theorem tsum_geometric_nnreal {r : ℝ≥0} (hr : r < 1) :
(∑' (n : ℕ), r ^ n) = (1 - r)⁻¹

source
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 ∞.

source
theorem has_sum_geometric_of_norm_lt_1 {K : Type u_4} [normed_field K] {ξ : K} (h : ∥ξ∥ < 1) :
has_sum (λ (n : ℕ), ξ ^ n) (1 - ξ)⁻¹

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

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

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

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

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

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.

source
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) :
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.

source
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).

source
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).

source
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) :
cauchy_seq f

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

source
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.

source
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.

source
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))

source
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) :
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.

source
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).

source
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).

source
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) :
cauchy_seq f

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

source
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.

source
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.

source
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

source
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.

source
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.

source
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.

source
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.

source
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

source
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

source
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
source
theorem nnreal.exists_pos_sum_of_encodable {ε : ℝ≥0} (hε : 0 < ε) (ι : Type u_1) [encodable ι] :
∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), has_sum ε' c ∧ c < ε

source
theorem ennreal.exists_pos_sum_of_encodable {ε : ennreal} (hε : 0 < ε) (ι : Type u_1) [encodable ι] :
∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ (∑' (i : ι), ↑(ε' i)) < ε

Harmonic series

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

source
def harmonic_series (n : ℕ) :
ℝ

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

Equations
source
theorem mono_harmonic  :
monotone harmonic_series

source
theorem half_le_harmonic_double_sub_harmonic (n : ℕ) (hn : 0 < n) :
1 / 2 ≤ harmonic_series (2 * n) - harmonic_series n

source
theorem self_div_two_le_harmonic_two_pow (n : ℕ) :
↑n / 2 ≤ harmonic_series (2 ^ n)

source
theorem harmonic_tendsto_at_top  :
filter.tendsto harmonic_series filter.at_top filter.at_top

The harmonic series diverges to +∞