analysis.specific_limits

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem is_o_coe_const_pow_of_one_lt {R : Type u_1} [normed_ring R] {r : ℝ} (hr : 1 < r) :

asymptotics.is_o coe (λ (n : ℕ), r ^ n) filter.at_top

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

source

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

source

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)

source

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.

source

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

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 : ℝ≥0∞} (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)

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 : ℝ≥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 ∞.

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)⁻¹

source

@[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.

source

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

source

theorem summable_pow_mul_geometric_of_norm_lt_1 {R : Type u_1} [normed_ring R] [complete_space R] (k : ℕ) {r : R} (hr : ∥r∥ < 1) :

summable (λ (n : ℕ), (↑n ^ k) * r ^ n)

source

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

source

theorem tsum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_1} [normed_field 𝕜] [complete_space 𝕜] {r : 𝕜} (hr : ∥r∥ < 1) :

∑' (n : ℕ), (↑n) * r ^ n = r / (1 - r) ^ 2

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

source

theorem cauchy_seq_of_edist_le_geometric {α : Type u_1} [emetric_space α] (r C : ℝ≥0∞) (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 : ℝ≥0∞) {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 : ℝ≥0∞) {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 : ℝ≥0∞) (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 : ℝ≥0∞) {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 : ℝ≥0∞) {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

source

theorem summable_of_ratio_norm_eventually_le {α : Type u_1} [semi_normed_group α] [complete_space α] {f : ℕ → α} {r : ℝ} (hr₁ : r < 1) (h : ∀ᶠ (n : ℕ) in filter.at_top, ∥f (n + 1)∥ ≤ r * ∥f n∥) :

summable f

source

theorem summable_of_ratio_test_tendsto_lt_one {α : Type u_1} [normed_group α] [complete_space α] {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)) :

summable f

source

theorem not_summable_of_ratio_norm_eventually_ge {α : Type u_1} [semi_normed_group α] {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)∥) :

¬summable f

source

theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type u_1} [semi_normed_group α] {f : ℕ → α} {l : ℝ} (hl : 1 < l) (h : filter.tendsto (λ (n : ℕ), ∥f (n + 1)∥ / ∥f n∥) filter.at_top (𝓝 l)) :

¬summable f

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

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

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 {ε : ℝ≥0∞} (hε : 0 < ε) (ι : Type u_1) [encodable ι] :

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

source

theorem factorial_tendsto_at_top :

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

source

theorem tendsto_factorial_div_pow_self_at_top :

filter.tendsto (λ (n : ℕ), ↑n! / ↑n ^ n) filter.at_top (𝓝 0)

mathlib documentation

A collection of specific limit computations #

Powers #

Geometric series #

Sequences with geometrically decaying distance in metric spaces #

Summability tests based on comparison with geometric series #

Positive sequences with small sums on encodable types #

Factorial #