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

theorem NNRat.tendsto_inv_atTop_nhds_zero_nat : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

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)

theorem tendsto_inv_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

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)

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)

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)

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)

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)

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., ℂ).

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

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

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

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

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.

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

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

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

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

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

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)

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

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

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}

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

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

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

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

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)

@[simp]

theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : NNReal} : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ r < 1

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)

@[simp]

theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ENNReal} : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ r < 1

@[simp]

theorem ENNReal.tendsto_pow_atTop_nhds_top_iff {r : ENNReal} : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds ⊤) ↔ 1 < r

theorem ENNReal.eq_zero_of_le_mul_pow {x r : ENNReal} {ε : NNReal} (hr : r < 1) (h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n) : x = 0

Geometric series

theorem hasSum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹

theorem summable_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : Summable fun (n : ℕ) => r ^ n

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

theorem hasSum_geometric_two : HasSum (fun (n : ℕ) => (1 / 2) ^ n) 2

theorem summable_geometric_two : Summable fun (n : ℕ) => (1 / 2) ^ n

theorem summable_geometric_two_encode {ι : Type u_4} [Encodable ι] : Summable fun (i : ι) => (1 / 2) ^ Encodable.encode i

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

theorem sum_geometric_two_le (n : ℕ) : ∑ i ∈ Finset.range n, (1 / 2) ^ i ≤ 2

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

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.

theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun (n : ℕ) => a / 2 / 2 ^ n) a

theorem summable_geometric_two' (a : ℝ) : Summable fun (n : ℕ) => a / 2 / 2 ^ n

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

theorem NNReal.hasSum_geometric {r : NNReal} (hr : r < 1) : HasSum (fun (n : ℕ) => r ^ n) (1 - r)⁻¹

Sum of a Geometric Series

theorem NNReal.summable_geometric {r : NNReal} (hr : r < 1) : Summable fun (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 ∞.

theorem ENNReal.tsum_geometric_add_one (r : ENNReal) : ∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹

theorem ENNReal.tsum_two_zpow_neg_add_one : ∑' (m : ℕ), 2 ^ (-1 - ↑m) = 1

theorem ENNReal.tsum_geometric_two : ∑' (n : ℕ), 2⁻¹ ^ n = 2

theorem ENNReal.tsum_geometric_two_encode_le_two {ι : Type u_4} [Encodable ι] : ∑' (i : ι), 2⁻¹ ^ Encodable.encode i ≤ 2

theorem tsum_geometric_lt_top {r : ENNReal} : ∑' (n : ℕ), r ^ n < ⊤ ↔ r < 1

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.

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.

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

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

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.

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.

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.

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.

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.

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

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

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.

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.

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

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

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, ⋯⟩

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 ≤ ε

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 ≤ ε

theorem NNReal.exists_pos_sum_of_countable {ε : NNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] : ∃ (ε' : ι → NNReal), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : NNReal), HasSum ε' c ∧ c < ε

theorem ENNReal.exists_pos_sum_of_countable {ε : ENNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] : ∃ (ε' : ι → NNReal), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

theorem ENNReal.exists_pos_sum_of_countable' {ε : ENNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] : ∃ (ε' : ι → ENNReal), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ε' i < ε

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

theorem factorial_tendsto_atTop : Filter.Tendsto Nat.factorial Filter.atTop Filter.atTop

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

Ceil and floor

theorem tendsto_nat_floor_atTop {α : Type u_4} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] : Filter.Tendsto (fun (x : α) => ⌊x⌋₊) Filter.atTop Filter.atTop

theorem tendsto_nat_ceil_atTop {α : Type u_4} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] : Filter.Tendsto (fun (x : α) => ⌈x⌉₊) Filter.atTop Filter.atTop

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

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)

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)

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)

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)

theorem Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) : Filter.Tendsto (fun (x : ℕ) => x / n) Filter.atTop Filter.atTop

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

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

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

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

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

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