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 tendsto_inverse_atTop_nhds_zero_nat : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

@[deprecated tendsto_inverse_atTop_nhds_zero_nat]

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

Alias of tendsto_inverse_atTop_nhds_zero_nat.

theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ) : Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)

@[deprecated tendsto_const_div_atTop_nhds_zero_nat]

theorem tendsto_const_div_atTop_nhds_0_nat (C : ℝ) : Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)

Alias of tendsto_const_div_atTop_nhds_zero_nat.

theorem tendsto_one_div_atTop_nhds_zero_nat : Filter.Tendsto (fun (n : ℕ) => 1 / ↑n) Filter.atTop (nhds 0)

@[deprecated tendsto_one_div_atTop_nhds_zero_nat]

theorem tendsto_one_div_atTop_nhds_0_nat : Filter.Tendsto (fun (n : ℕ) => 1 / ↑n) Filter.atTop (nhds 0)

Alias of tendsto_one_div_atTop_nhds_zero_nat.

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

@[deprecated NNReal.tendsto_inverse_atTop_nhds_zero_nat]

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

Alias of NNReal.tendsto_inverse_atTop_nhds_zero_nat.

theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat (C : NNReal) : Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)

@[deprecated NNReal.tendsto_const_div_atTop_nhds_zero_nat]

theorem NNReal.tendsto_const_div_atTop_nhds_0_nat (C : NNReal) : Filter.Tendsto (fun (n : ℕ) => C / ↑n) Filter.atTop (nhds 0)

Alias of NNReal.tendsto_const_div_atTop_nhds_zero_nat.

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 : Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhds 0)

@[deprecated tendsto_one_div_add_atTop_nhds_zero_nat]

theorem tendsto_one_div_add_atTop_nhds_0_nat : Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhds 0)

Alias of tendsto_one_div_add_atTop_nhds_zero_nat.

theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type u_4) [Semiring 𝕜] [Algebra NNReal 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul NNReal 𝕜] : Filter.Tendsto (⇑(algebraMap NNReal 𝕜) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

@[deprecated NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat]

theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat (𝕜 : Type u_4) [Semiring 𝕜] [Algebra NNReal 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul NNReal 𝕜] : Filter.Tendsto (⇑(algebraMap NNReal 𝕜) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat.

theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type u_4) [Semiring 𝕜] [Algebra ℝ 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ 𝕜] : Filter.Tendsto (⇑(algebraMap ℝ 𝕜) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

@[deprecated tendsto_algebraMap_inverse_atTop_nhds_zero_nat]

theorem tendsto_algebraMap_inverse_atTop_nhds_0_nat (𝕜 : Type u_4) [Semiring 𝕜] [Algebra ℝ 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ 𝕜] : Filter.Tendsto (⇑(algebraMap ℝ 𝕜) ∘ fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of tendsto_algebraMap_inverse_atTop_nhds_zero_nat.

theorem tendsto_natCast_div_add_atTop {𝕜 : Type u_4} [DivisionRing 𝕜] [TopologicalSpace 𝕜] [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [TopologicalDivisionRing 𝕜] (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 ℝ, 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 ℂ.

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 Filter.EventuallyEq.div_mul_cancel {α : Type u_4} {G : Type u_5} [GroupWithZero G] {f : α → G} {g : α → G} {l : Filter α} (hg : Filter.Tendsto g l (Filter.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} [LinearOrderedSemifield K] {f : α → K} {g : α → K} {l : Filter α} (hg : Filter.Tendsto g l Filter.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 Tendsto.num {α : Type u_4} {K : Type u_5} [LinearOrderedField K] [TopologicalSpace K] [OrderTopology K] {f : α → K} {g : α → K} {l : Filter α} (hg : Filter.Tendsto g l Filter.atTop) {a : K} (ha : 0 < a) (hlim : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds a)) : Filter.Tendsto f l Filter.atTop

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

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

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

theorem Tendsto.num_atTop_iff_den_atTop {α : Type u_4} {K : Type u_5} [LinearOrderedField K] [TopologicalSpace K] [OrderTopology K] [ContinuousInv K] {f : α → K} {g : α → K} {l : Filter α} {a : K} (ha : 0 < a) (hlim : Filter.Tendsto (fun (x : α) => f x / g x) l (nhds a)) : Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto g l Filter.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} [LinearOrderedSemiring α] [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} [LinearOrderedRing α] [Archimedean α] {r : α} (h : 1 < r) : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop Filter.atTop

theorem Nat.tendsto_pow_atTop_atTop_of_one_lt {m : ℕ} (h : 1 < m) : Filter.Tendsto (fun (n : ℕ) => m ^ n) Filter.atTop Filter.atTop

theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type u_4} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0)

@[deprecated tendsto_pow_atTop_nhds_zero_of_lt_one]

theorem tendsto_pow_atTop_nhds_0_of_lt_1 {𝕜 : Type u_4} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0)

Alias of tendsto_pow_atTop_nhds_zero_of_lt_one.

@[simp]

theorem tendsto_pow_atTop_nhds_zero_iff {𝕜 : Type u_4} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ |r| < 1

@[deprecated tendsto_pow_atTop_nhds_zero_iff]

theorem tendsto_pow_atTop_nhds_0_iff {𝕜 : Type u_4} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhds 0) ↔ |r| < 1

Alias of tendsto_pow_atTop_nhds_zero_iff.

theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type u_4} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

@[deprecated tendsto_pow_atTop_nhdsWithin_zero_of_lt_one]

theorem tendsto_pow_atTop_nhdsWithin_0_of_lt_1 {𝕜 : Type u_4} [LinearOrderedField 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) : Filter.Tendsto (fun (n : ℕ) => r ^ n) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

Alias of tendsto_pow_atTop_nhdsWithin_zero_of_lt_one.

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}

@[deprecated uniformity_basis_dist_pow_of_lt_one]

theorem uniformity_basis_dist_pow_of_lt_1 {α : 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}

Alias of uniformity_basis_dist_pow_of_lt_one.

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)

@[deprecated NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one]

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

Alias of NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one.

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

@[deprecated ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one]

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

Alias of ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one.

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

Geometric series

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

@[deprecated hasSum_geometric_of_lt_one]

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

Alias of hasSum_geometric_of_lt_one.

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

@[deprecated summable_geometric_of_lt_one]

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

Alias of summable_geometric_of_lt_one.

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

@[deprecated tsum_geometric_of_lt_one]

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

Alias of tsum_geometric_of_lt_one.

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

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 : ENNReal) (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 : ENNReal) (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 : ENNReal) (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} [LinearOrderedSemiring α] [FloorSemiring α] : Filter.Tendsto (fun (x : α) => ⌊x⌋₊) Filter.atTop Filter.atTop

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

theorem tendsto_nat_floor_mul_atTop {α : Type u_4} [LinearOrderedSemifield α] [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] [LinearOrderedField 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] [LinearOrderedField 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] [LinearOrderedField 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] [LinearOrderedField 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