# A collection of specific limit computations #

This file, by design, is independent of `NormedSpace` 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∞`.

source
theorem NNRat.tendsto_inv_atTop_nhds_zero_nat :
Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)
source
theorem NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat (𝕜 : Type u_4) [Semiring 𝕜] [Algebra ℚ≥0 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
Filter.Tendsto (⇑(algebraMap ℚ≥0 𝕜) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)
source
theorem tendsto_inv_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)
source
theorem tendsto_const_div_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [ContinuousMul 𝕜] (C : 𝕜) :
Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)
source
theorem tendsto_one_div_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
Filter.Tendsto (fun (n : ℕ) => 1 / ↑n) Filter.atTop (nhds 0)
source
theorem EReal.tendsto_const_div_atTop_nhds_zero_nat {C : EReal} (h : C ≠ ⊥) (h' : C ≠ ⊤) :
Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)
source
theorem tendsto_one_div_add_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhds 0)
source
theorem tendsto_algebraMap_inv_atTop_nhds_zero_nat {𝕜 : Type u_4} (A : Type u_5) [Semifield 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [Semiring A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A] :
Filter.Tendsto (⇑(algebraMap 𝕜 A) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)
source
theorem tendsto_natCast_div_add_atTop {𝕜 : Type u_4} [DivisionSemiring 𝕜] [TopologicalSpace 𝕜] [CharZero 𝕜] [ContinuousSMul ℚ≥0 𝕜] [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (x : 𝕜) :
Filter.Tendsto (fun (n : ℕ) => ↑n / (↑n + x)) Filter.atTop (nhds 1)

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

source
theorem tendsto_add_mul_div_add_mul_atTop_nhds {𝕜 : Type u_4} [Semifield 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (a b c : 𝕜) {d : 𝕜} (hd : d ≠ 0) :
Filter.Tendsto (fun (k : ℕ) => (a + c * ↑k) / (b + d * ↑k)) Filter.atTop (nhds (c / d))
source
theorem tendsto_mod_div_atTop_nhds_zero_nat {m : ℕ} (hm : 0 < m) :
Filter.Tendsto (fun (n : ℕ) => ↑(n % m) / ↑n) Filter.atTop (nhds 0)

For any positive `m : ℕ`, `((n % m : ℕ) : ℝ) / (n : ℝ)` tends to `0` as `n` tends to `∞`.

source
theorem tendsto_mul_add_inv_atTop_nhds_zero (a c : ℝ) (ha : a ≠ 0) :
Filter.Tendsto (fun (x : ℝ) => (a * x + c)⁻¹) Filter.atTop (nhds 0)

If `a ≠ 0`, `(a * x + c)⁻¹` tends to `0` as `x` tends to `∞`.

source
theorem Filter.EventuallyEq.div_mul_cancel {α : Type u_4} {G : Type u_5} [GroupWithZero G] {f g : α → G} {l : Filter α} (hg : Tendsto g l (principal {0}ᶜ)) :
(fun (x : α) => f x / g x * g x) =ᶠ[l] fun (x : α) => f x
source
theorem Filter.EventuallyEq.div_mul_cancel_atTop {α : Type u_4} {K : Type u_5} [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K] {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) :
(fun (x : α) => f x / g x * g x) =ᶠ[l] fun (x : α) => f x

If `g` tends to `∞`, then eventually for all `x` we have `(f x / g x) * g x = f x`.

source
theorem Filter.Tendsto.num {α : Type u_4} {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K] [OrderTopology K] {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) {a : K} (ha : 0 < a) (hlim : Tendsto (fun (x : α) => f x / g x) l (nhds a)) :
Tendsto f l atTop

If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive constant, then `f` tends to `∞`.

source
theorem Filter.Tendsto.den {α : Type u_4} {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K] [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α} (hf : Tendsto f l atTop) {a : K} (ha : 0 < a) (hlim : Tendsto (fun (x : α) => f x / g x) l (nhds a)) :
Tendsto g l atTop

If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive constant, then `f` tends to `∞`.

source
theorem Filter.Tendsto.num_atTop_iff_den_atTop {α : Type u_4} {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K] [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α} {a : K} (ha : 0 < a) (hlim : Tendsto (fun (x : α) => f x / g x) l (nhds a)) :
Tendsto f l atTop ↔ Tendsto g l atTop

If when `x` tends to `∞`, `f x / g x` tends to a positive constant, then `f` tends to `∞` if and only if `g` tends to `∞`.

### Powers #

source
theorem tendsto_add_one_pow_atTop_atTop_of_pos {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α} (h : 0 < r) :
Filter.Tendsto (fun (n : ℕ) => (r + 1) ^ n) Filter.atTop Filter.atTop
source
theorem tendsto_pow_atTop_atTop_of_one_lt {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [Archimedean α] {r : α} (h : 1 < r) :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop Filter.atTop
source
theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0)
source
@[simp]
theorem tendsto_pow_atTop_nhds_zero_iff {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ |r| < 1
source
theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))
source
theorem uniformity_basis_dist_pow_of_lt_one {α : Type u_4} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) :
(uniformity α).HasBasis (fun (x : ℕ) => True) fun (k : ℕ) => {p : α × α | dist p.1 p.2 < r ^ k}
source
theorem geom_lt {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n) (h : ∀ 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 < 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 < 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 < n, u (k + 1) ≤ c * u k) :
u n ≤ c ^ n * u 0
source
theorem tendsto_atTop_of_geom_le {v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (hc : 1 < c) (hu : ∀ (n : ℕ), c * v n ≤ v (n + 1)) :
Filter.Tendsto v Filter.atTop Filter.atTop

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_atTop_nhds_zero_of_lt_one {r : NNReal} (hr : r < 1) :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0)
source
@[simp]
theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : NNReal} :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ r < 1
source
theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ENNReal} (hr : r < 1) :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0)
source
@[simp]
theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ENNReal} :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ r < 1
source
@[simp]
theorem ENNReal.tendsto_pow_atTop_nhds_top_iff {r : ENNReal} :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds ⊤) ↔ 1 < r
source
theorem ENNReal.eq_zero_of_le_mul_pow {x r : ENNReal} {ε : NNReal} (hr : r < 1) (h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n) :
x = 0

### Geometric series #

source
theorem hasSum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹
source
theorem summable_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
Summable fun (n : ℕ) => r ^ n
source
theorem tsum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
∑' (n : ℕ), r ^ n = (1 - r)⁻¹
source
theorem hasSum_geometric_two :
HasSum (fun (n : ℕ) => (1 / 2) ^ n) 2
source
theorem summable_geometric_two :
Summable fun (n : ℕ) => (1 / 2) ^ n
source
theorem summable_geometric_two_encode {ι : Type u_4} [Encodable ι] :
Summable fun (i : ι) => (1 / 2) ^ Encodable.encode i
source
theorem tsum_geometric_two :
∑' (n : ℕ), (1 / 2) ^ n = 2
source
theorem sum_geometric_two_le (n : ℕ) :
∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2
source
theorem tsum_geometric_inv_two :
∑' (n : ℕ), 2⁻¹ ^ n = 2
source
theorem tsum_geometric_inv_two_ge (n : ℕ) :
(∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n

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

source
theorem hasSum_geometric_two' (a : ℝ) :
HasSum (fun (n : ℕ) => a / 2 / 2 ^ n) a
source
theorem summable_geometric_two' (a : ℝ) :
Summable fun (n : ℕ) => a / 2 / 2 ^ n
source
theorem tsum_geometric_two' (a : ℝ) :
∑' (n : ℕ), a / 2 / 2 ^ n = a
source
theorem NNReal.hasSum_geometric {r : NNReal} (hr : r < 1) :
HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹

Sum of a Geometric Series

source
theorem NNReal.summable_geometric {r : NNReal} (hr : r < 1) :
Summable fun (n : ℕ) => r ^ n
source
theorem tsum_geometric_nnreal {r : NNReal} (hr : r < 1) :
∑' (n : ℕ), r ^ n = (1 - r)⁻¹
source
@[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 `∞`.

source
theorem ENNReal.tsum_geometric_add_one (r : ENNReal) :
∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹
source
theorem ENNReal.tsum_two_zpow_neg_add_one :
∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1
source
theorem ENNReal.tsum_geometric_two :
∑' (n : ℕ), 2⁻¹ ^ n = 2
source
theorem ENNReal.tsum_geometric_two_encode_le_two {ι : Type u_4} [Encodable ι] :
∑' (i : ι), 2⁻¹ ^ Encodable.encode i ≤ 2
source
theorem tsum_geometric_lt_top {r : ENNReal} :
∑' (n : ℕ), r ^ n < ⊤ ↔ r < 1
source
theorem tsum_geometric_encode_lt_top {r : ENNReal} (hr : r < 1) {ι : Type u_4} [Encodable ι] :
∑' (i : ι), r ^ Encodable.encode i < ⊤

### 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 cauchySeq_of_edist_le_geometric {α : Type u_1} [PseudoEMetricSpace α] (r C : ENNReal) (hr : r < 1) (hC : C ≠ ⊤) {f : ℕ → α} (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) :
CauchySeq 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} [PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α} (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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} [PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α} (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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 cauchySeq_of_edist_le_geometric_two {α : Type u_1} [PseudoEMetricSpace α] (C : ENNReal) (hC : C ≠ ⊤) {f : ℕ → α} (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) :
CauchySeq 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} [PseudoEMetricSpace α] (C : ENNReal) {f : ℕ → α} (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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} [PseudoEMetricSpace α] (C : ENNReal) {f : ℕ → α} (hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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_hasSum_of_le_geometric {α : Type u_1} [PseudoMetricSpace α] {r C : ℝ} {f : ℕ → α} (hr : r < 1) (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) :
HasSum (fun (n : ℕ) => C * r ^ n) (C / (1 - r))

If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence.

source
theorem cauchySeq_of_le_geometric {α : Type u_1} [PseudoMetricSpace α] (r C : ℝ) {f : ℕ → α} (hr : r < 1) (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) :
CauchySeq 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} [PseudoMetricSpace α] (r C : ℝ) {f : ℕ → α} (hr : r < 1) (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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} [PseudoMetricSpace α] (r C : ℝ) {f : ℕ → α} (hr : r < 1) (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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 cauchySeq_of_le_geometric_two {α : Type u_1} [PseudoMetricSpace α] {C : ℝ} {f : ℕ → α} (hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) :
CauchySeq 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} [PseudoMetricSpace α] {C : ℝ} {f : ℕ → α} (hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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} [PseudoMetricSpace α] {C : ℝ} {f : ℕ → α} (hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds 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`.

### Summability tests based on comparison with geometric series #

source
theorem summable_one_div_pow_of_le {m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi : ∀ (i : ℕ), i ≤ f i) :
Summable fun (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 #

source
def posSumOfEncodable {ε : ℝ} (hε : 0 < ε) (ι : Type u_4) [Encodable ι] :
{ ε' : ι → ℝ // (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum ε' c ∧ c ≤ ε }

For any positive `ε`, define on an encodable type a positive sequence with sum less than `ε`

Equations

- posSumOfEncodable hε ι = ⟨(fun (n : ℕ) => ε / 2 / 2 ^ n) ∘ Encodable.encode, ⋯⟩

Instances For

source
theorem Set.Countable.exists_pos_hasSum_le {ι : Type u_4} {s : Set ι} (hs : s.Countable) {ε : ℝ} (hε : 0 < ε) :
∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ), HasSum (fun (i : ↑s) => ε' ↑i) c ∧ c ≤ ε
source
theorem Set.Countable.exists_pos_forall_sum_le {ι : Type u_4} {s : Set ι} (hs : s.Countable) {ε : ℝ} (hε : 0 < ε) :
∃ (ε' : ι → ℝ), (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε
source
theorem NNReal.exists_pos_sum_of_countable {ε : NNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] :
∃ (ε' : ι → NNReal), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : NNReal), HasSum ε' c ∧ c < ε
source
theorem ENNReal.exists_pos_sum_of_countable {ε : ENNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] :
∃ (ε' : ι → NNReal), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
source
theorem ENNReal.exists_pos_sum_of_countable' {ε : ENNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] :
∃ (ε' : ι → ENNReal), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ε' i < ε
source
theorem ENNReal.exists_pos_tsum_mul_lt_of_countable {ε : ENNReal} (hε : ε ≠ 0) {ι : Type u_4} [Countable ι] (w : ι → ENNReal) (hw : ∀ (i : ι), w i ≠ ⊤) :
∃ (δ : ι → NNReal), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε

### Factorial #

source
theorem factorial_tendsto_atTop :
Filter.Tendsto Nat.factorial Filter.atTop Filter.atTop
source
theorem tendsto_factorial_div_pow_self_atTop :
Filter.Tendsto (fun (n : ℕ) => ↑n.factorial / ↑n ^ n) Filter.atTop (nhds 0)

### Ceil and floor #

source
theorem tendsto_nat_floor_atTop {α : Type u_4} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
Filter.Tendsto (fun (x : α) => ⌊x⌋₊) Filter.atTop Filter.atTop
source
theorem tendsto_nat_ceil_atTop {α : Type u_4} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
Filter.Tendsto (fun (x : α) => ⌈x⌉₊) Filter.atTop Filter.atTop
source
theorem tendsto_nat_floor_mul_atTop {α : Type u_4} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] [Archimedean α] (a : α) (ha : 0 < a) :
Filter.Tendsto (fun (x : ℕ) => ⌊a * ↑x⌋₊) Filter.atTop Filter.atTop
source
theorem tendsto_nat_floor_mul_div_atTop {R : Type u_4} [TopologicalSpace R] [Field R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] [FloorRing R] {a : R} (ha : 0 ≤ a) :
Filter.Tendsto (fun (x : R) => ↑⌊a * x⌋₊ / x) Filter.atTop (nhds a)
source
theorem tendsto_nat_floor_div_atTop {R : Type u_4} [TopologicalSpace R] [Field R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] [FloorRing R] :
Filter.Tendsto (fun (x : R) => ↑⌊x⌋₊ / x) Filter.atTop (nhds 1)
source
theorem tendsto_nat_ceil_mul_div_atTop {R : Type u_4} [TopologicalSpace R] [Field R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] [FloorRing R] {a : R} (ha : 0 ≤ a) :
Filter.Tendsto (fun (x : R) => ↑⌈a * x⌉₊ / x) Filter.atTop (nhds a)
source
theorem tendsto_nat_ceil_div_atTop {R : Type u_4} [TopologicalSpace R] [Field R] [LinearOrder R] [IsStrictOrderedRing R] [OrderTopology R] [FloorRing R] :
Filter.Tendsto (fun (x : R) => ↑⌈x⌉₊ / x) Filter.atTop (nhds 1)
source
theorem Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) :
Filter.Tendsto (fun (x : ℕ) => x / n) Filter.atTop Filter.atTop
source
@[deprecated tendsto_inv_atTop_nhds_zero_nat (since := "2025-10-27")]
theorem tendsto_inverse_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of `tendsto_inv_atTop_nhds_zero_nat`.

source
@[deprecated tendsto_inv_atTop_nhds_zero_nat (since := "2025-10-27")]
theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of `tendsto_inv_atTop_nhds_zero_nat`.

source
@[deprecated tendsto_const_div_atTop_nhds_zero_nat (since := "2025-10-27")]
theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [ContinuousMul 𝕜] (C : 𝕜) :
Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)

Alias of `tendsto_const_div_atTop_nhds_zero_nat`.

source
@[deprecated tendsto_algebraMap_inv_atTop_nhds_zero_nat (since := "2025-10-27")]
theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat {𝕜 : Type u_4} (A : Type u_5) [Semifield 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [Semiring A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A] :
Filter.Tendsto (⇑(algebraMap 𝕜 A) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of `tendsto_algebraMap_inv_atTop_nhds_zero_nat`.

source
@[deprecated tendsto_algebraMap_inv_atTop_nhds_zero_nat (since := "2025-10-27")]
theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat {𝕜 : Type u_4} (A : Type u_5) [Semifield 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [Semiring A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A] :
Filter.Tendsto (⇑(algebraMap 𝕜 A) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of `tendsto_algebraMap_inv_atTop_nhds_zero_nat`.

source
@[deprecated tendsto_pow_atTop_atTop_of_one_lt (since := "2025-10-27")]
theorem Nat.tendsto_pow_atTop_atTop_of_one_lt {α : Type u_1} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [Archimedean α] {r : α} (h : 1 < r) :
Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop Filter.atTop

Alias of `tendsto_pow_atTop_atTop_of_one_lt`.