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

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

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

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

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

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

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

theorem tendsto_coe_nat_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 ℂ.

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

@[simp]

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

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

theorem uniformity_basis_dist_pow_of_lt_1 {α : Type u_4} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) : Filter.HasBasis (uniformity α) (fun x => True) fun k => {p | 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_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_0_of_lt_1 {r : NNReal} (hr : r < 1) : Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)

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)

Geometric series

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

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

theorem tsum_geometric_of_lt_1 {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 : ℕ) : (Finset.sum (Finset.range n) fun i => (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 ∞.

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 : ℝ} (hr : r < 1) {f : ℕ → α} (hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) : HasSum (fun n => C * r ^ n) (C / (1 - r))

theorem cauchySeq_of_le_geometric {α : Type u_1} [PseudoMetricSpace α] (r : ℝ) (C : ℝ) (hr : r < 1) {f : ℕ → α} (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 : ℝ) (hr : r < 1) {f : ℕ → α} (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 : ℝ) (hr : r < 1) {f : ℕ → α} (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

• One or more equations did not get rendered due to their size.

theorem Set.Countable.exists_pos_hasSum_le {ι : Type u_4} {s : Set ι} (hs : Set.Countable s) {ε : ℝ} (hε : 0 < ε) : ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε

theorem Set.Countable.exists_pos_forall_sum_le {ι : Type u_4} {s : Set ι} (hs : Set.Countable s) {ε : ℝ} (hε : 0 < ε) : ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → (Finset.sum t fun i => ε' i) ≤ ε

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

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

theorem ENNReal.exists_pos_sum_of_countable' {ε : ENNReal} (hε : ε ≠ 0) (ι : Type u_4) [Countable ι] : ∃ ε', (∀ (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 ≠ ⊤) : ∃ δ, (∀ (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 => ↑(Nat.factorial n) / ↑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_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 => ↑⌊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 => ↑⌊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 => ↑⌈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 => ↑⌈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