mathlib3 documentation

analysis.specific_limits.basic

A collection of specific limit computations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file, by design, is independent of normed_space in the import hierarchy. It contains important specific limit computations in metric spaces, in ordered rings/fields, and in specific instances of these such as ℝ, ℝ≥0 and ℝ≥0∞.

theorem tendsto_inverse_at_top_nhds_0_nat :

filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (nhds 0)

theorem tendsto_const_div_at_top_nhds_0_nat (C : ℝ) :

filter.tendsto (λ (n : ℕ), C / ↑n) filter.at_top (nhds 0)

theorem nnreal.tendsto_inverse_at_top_nhds_0_nat :

filter.tendsto (λ (n : ℕ), (↑n)⁻¹) filter.at_top (nhds 0)

theorem nnreal.tendsto_const_div_at_top_nhds_0_nat (C : nnreal) :

filter.tendsto (λ (n : ℕ), C / ↑n) filter.at_top (nhds 0)

theorem tendsto_one_div_add_at_top_nhds_0_nat :

filter.tendsto (λ (n : ℕ), 1 / (↑n + 1)) filter.at_top (nhds 0)

theorem tendsto_coe_nat_div_add_at_top {𝕜 : Type u_1} [division_ring 𝕜] [topological_space 𝕜] [char_zero 𝕜] [algebra ℝ 𝕜] [has_continuous_smul ℝ 𝕜] [topological_division_ring 𝕜] (x : 𝕜) :

filter.tendsto (λ (n : ℕ), ↑n / (↑n + x)) filter.at_top (nhds 1)

The limit of n / (n + x) is 1, for any constant x (valid in ℝ or any topological division algebra over ℝ, e.g., ℂ).

TODO: introduce a typeclass saying that 1 / n tends to 0 at top, making it possible to get this statement simultaneously on ℚ, ℝ and ℂ.

Powers #

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

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

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

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 (nhds 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) :

filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (nhds_within 0 (set.Ioi 0))

theorem uniformity_basis_dist_pow_of_lt_1 {α : Type u_1} [pseudo_metric_space α] {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) :

(uniformity α).has_basis (λ (k : ℕ), true) (λ (k : ℕ), {p : α × α | has_dist.dist p.fst p.snd < r ^ k})

theorem geom_lt {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n) (h : ∀ (k : ℕ), k < n → c * u k < u (k + 1)) :

c ^ n * u 0 < u n

theorem geom_le {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ (k : ℕ), k < n → c * 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 < n → u (k + 1) < c * u k) :

u n < c ^ n * u 0

theorem le_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ (k : ℕ), k < n → u (k + 1) ≤ c * u k) :

u n ≤ c ^ n * u 0

theorem tendsto_at_top_of_geom_le {v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (hc : 1 < c) (hu : ∀ (n : ℕ), c * 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 nnreal.tendsto_pow_at_top_nhds_0_of_lt_1 {r : nnreal} (hr : r < 1) :

filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (nhds 0)

theorem ennreal.tendsto_pow_at_top_nhds_0_of_lt_1 {r : ennreal} (hr : r < 1) :

filter.tendsto (λ (n : ℕ), r ^ n) filter.at_top (nhds 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 summable_geometric_two_encode {ι : Type u_1} [encodable ι] :

summable (λ (i : ι), (1 / 2) ^ encodable.encode i)

theorem tsum_geometric_two :

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

theorem sum_geometric_two_le (n : ℕ) :

(finset.range n).sum (λ (i : ℕ), (1 / 2) ^ i) ≤ 2

theorem tsum_geometric_inv_two :

∑' (n : ℕ), 2⁻¹ ^ n = 2

theorem tsum_geometric_inv_two_ge (n : ℕ) :

∑' (i : ℕ), ite (n ≤ i) (2⁻¹ ^ i) 0 = 2 * 2⁻¹ ^ n

The sum of 2⁻¹ ^ i for n ≤ i equals 2 * 2⁻¹ ^ n.

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 : nnreal} (hr : r < 1) :

has_sum (λ (n : ℕ), r ^ n) (1 - r)⁻¹

Sum of a Geometric Series

theorem nnreal.summable_geometric {r : nnreal} (hr : r < 1) :

summable (λ (n : ℕ), r ^ n)

theorem tsum_geometric_nnreal {r : nnreal} (hr : r < 1) :

∑' (n : ℕ), r ^ n = (1 - r)⁻¹

@[simp]

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

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} [pseudo_emetric_space α] (r C : ennreal) (hr : r < 1) (hC : C ≠ ⊤) {f : ℕ → α} (hu : ∀ (n : ℕ), has_edist.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} [pseudo_emetric_space α] (r C : ennreal) {f : ℕ → α} (hu : ∀ (n : ℕ), has_edist.edist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) (n : ℕ) :

has_edist.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} [pseudo_emetric_space α] (r C : ennreal) {f : ℕ → α} (hu : ∀ (n : ℕ), has_edist.edist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) :

has_edist.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} [pseudo_emetric_space α] (C : ennreal) (hC : C ≠ ⊤) {f : ℕ → α} (hu : ∀ (n : ℕ), has_edist.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} [pseudo_emetric_space α] (C : ennreal) {f : ℕ → α} (hu : ∀ (n : ℕ), has_edist.edist (f n) (f (n + 1)) ≤ C / 2 ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) (n : ℕ) :

has_edist.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} [pseudo_emetric_space α] (C : ennreal) {f : ℕ → α} (hu : ∀ (n : ℕ), has_edist.edist (f n) (f (n + 1)) ≤ C / 2 ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) :

has_edist.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} [pseudo_metric_space α] {r C : ℝ} (hr : r < 1) {f : ℕ → α} (hu : ∀ (n : ℕ), has_dist.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} [pseudo_metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α} (hu : ∀ (n : ℕ), has_dist.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} [pseudo_metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α} (hu : ∀ (n : ℕ), has_dist.dist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) :

has_dist.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} [pseudo_metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α} (hu : ∀ (n : ℕ), has_dist.dist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) (n : ℕ) :

has_dist.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} [pseudo_metric_space α] (C : ℝ) {f : ℕ → α} (hu₂ : ∀ (n : ℕ), has_dist.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} [pseudo_metric_space α] (C : ℝ) {f : ℕ → α} (hu₂ : ∀ (n : ℕ), has_dist.dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) :

has_dist.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} [pseudo_metric_space α] (C : ℝ) {f : ℕ → α} (hu₂ : ∀ (n : ℕ), has_dist.dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) {a : α} (ha : filter.tendsto f filter.at_top (nhds a)) (n : ℕ) :

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

Summability tests based on comparison with geometric series #

theorem summable_one_div_pow_of_le {m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi : ∀ (i : ℕ), i ≤ f i) :

summable (λ (i : ℕ), 1 / m ^ f i)

A series whose terms are bounded by the terms of a converging geometric series converges.

Positive sequences with small sums on countable types #

noncomputable 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

pos_sum_of_encodable hε ι = let f : ℕ → ℝ := λ (n : ℕ), ε / 2 / 2 ^ n in ⟨f ∘ encodable.encode, _⟩

theorem set.countable.exists_pos_has_sum_le {ι : Type u_1} {s : set ι} (hs : s.countable) {ε : ℝ} (hε : 0 < ε) :

∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), has_sum (λ (i : ↥s), ε' ↑i) c ∧ c ≤ ε

theorem set.countable.exists_pos_forall_sum_le {ι : Type u_1} {s : set ι} (hs : s.countable) {ε : ℝ} (hε : 0 < ε) :

∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : finset ι), ↑t ⊆ s → t.sum (λ (i : ι), ε' i) ≤ ε

theorem nnreal.exists_pos_sum_of_countable {ε : nnreal} (hε : ε ≠ 0) (ι : Type u_1) [countable ι] :

∃ (ε' : ι → nnreal), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : nnreal), has_sum ε' c ∧ c < ε

theorem ennreal.exists_pos_sum_of_countable {ε : ennreal} (hε : ε ≠ 0) (ι : Type u_1) [countable ι] :

∃ (ε' : ι → nnreal), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

theorem ennreal.exists_pos_sum_of_countable' {ε : ennreal} (hε : ε ≠ 0) (ι : Type u_1) [countable ι] :

∃ (ε' : ι → ennreal), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ε' i < ε

theorem ennreal.exists_pos_tsum_mul_lt_of_countable {ε : ennreal} (hε : ε ≠ 0) {ι : Type u_1} [countable ι] (w : ι → ennreal) (hw : ∀ (i : ι), w i ≠ ⊤) :

∃ (δ : ι → nnreal), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε

Factorial #

theorem factorial_tendsto_at_top :

filter.tendsto nat.factorial filter.at_top filter.at_top

theorem tendsto_factorial_div_pow_self_at_top :

filter.tendsto (λ (n : ℕ), ↑(n.factorial) / ↑n ^ n) filter.at_top (nhds 0)

Ceil and floor #

theorem tendsto_nat_floor_at_top {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] :

filter.tendsto (λ (x : α), ⌊x⌋₊) filter.at_top filter.at_top

theorem tendsto_nat_floor_mul_div_at_top {R : Type u_4} [topological_space R] [linear_ordered_field R] [order_topology R] [floor_ring R] {a : R} (ha : 0 ≤ a) :

filter.tendsto (λ (x : R), ↑⌊a * x⌋₊ / x) filter.at_top (nhds a)

theorem tendsto_nat_floor_div_at_top {R : Type u_4} [topological_space R] [linear_ordered_field R] [order_topology R] [floor_ring R] :

filter.tendsto (λ (x : R), ↑⌊x⌋₊ / x) filter.at_top (nhds 1)

theorem tendsto_nat_ceil_mul_div_at_top {R : Type u_4} [topological_space R] [linear_ordered_field R] [order_topology R] [floor_ring R] {a : R} (ha : 0 ≤ a) :

filter.tendsto (λ (x : R), ↑⌈a * x⌉₊ / x) filter.at_top (nhds a)

theorem tendsto_nat_ceil_div_at_top {R : Type u_4} [topological_space R] [linear_ordered_field R] [order_topology R] [floor_ring R] :

filter.tendsto (λ (x : R), ↑⌈x⌉₊ / x) filter.at_top (nhds 1)