Mathlib.Analysis.SpecificLimits.Basic

tendsto_inverse_atTop_nhds_zero_nat theorem

: Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0)

Full source

theorem tendsto_inverse_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) :=
  tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop

Limit of Reciprocals of Natural Numbers is Zero

Informal description

The sequence of reciprocals of natural numbers, viewed as real numbers, converges to $0$ as $n$ tends to infinity. That is, $\lim_{n \to \infty} \frac{1}{n} = 0$.

tendsto_const_div_atTop_nhds_zero_nat theorem

(C : ℝ) : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0)

Full source

theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
  simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_zero_nat

Limit of Constant Divided by Natural Numbers is Zero

Informal description

For any real number $C$, the sequence defined by $a_n = \frac{C}{n}$ converges to $0$ as $n$ tends to infinity, i.e., $\lim_{n \to \infty} \frac{C}{n} = 0$.

tendsto_one_div_atTop_nhds_zero_nat theorem

: Tendsto (fun n : ℕ ↦ 1 / (n : ℝ)) atTop (𝓝 0)

Full source

theorem tendsto_one_div_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ 1/(n : ℝ)) atTop (𝓝 0) :=
  tendsto_const_div_atTop_nhds_zero_nat 1

Limit of Reciprocal Sequence: $\lim_{n \to \infty} \frac{1}{n} = 0$

Informal description

The sequence defined by $a_n = \frac{1}{n}$ for $n \in \mathbb{N}$ converges to $0$ as $n$ tends to infinity, i.e., $\lim_{n \to \infty} \frac{1}{n} = 0$.

NNReal.tendsto_inverse_atTop_nhds_zero_nat theorem

: Tendsto (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0)

Full source

theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat :
    Tendsto (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0) := by
  rw [← NNReal.tendsto_coe]
  exact _root_.tendsto_inverse_atTop_nhds_zero_nat

Limit of Reciprocals of Natural Numbers in Nonnegative Reals is Zero

Informal description

The sequence of reciprocals of natural numbers, viewed as nonnegative real numbers, converges to $0$ as $n$ tends to infinity. That is, $\lim_{n \to \infty} \frac{1}{n} = 0$ in $\mathbb{R}_{\geq 0}$.

NNReal.tendsto_const_div_atTop_nhds_zero_nat theorem

(C : ℝ≥0) : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0)

Full source

theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat (C : ℝ≥0) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
  simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_zero_nat

Limit of Constant Divided by Natural Numbers in Nonnegative Reals is Zero

Informal description

For any nonnegative real number $C$, the sequence defined by $a_n = \frac{C}{n}$ for $n \in \mathbb{N}$ converges to $0$ as $n$ tends to infinity, i.e., $\lim_{n \to \infty} \frac{C}{n} = 0$.

EReal.tendsto_const_div_atTop_nhds_zero_nat theorem

{C : EReal} (h : C ≠ ⊥) (h' : C ≠ ⊤) : Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0)

Full source

theorem EReal.tendsto_const_div_atTop_nhds_zero_nat {C : EReal} (h : C ≠ ⊥) (h' : C ≠ ⊤) :
    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
  have : (fun n : ℕ ↦ C / n) = fun n : ℕ ↦ ((C.toReal / n : ℝ) : EReal) := by
    ext n
    nth_rw 1 [← coe_toReal h' h, ← coe_coe_eq_natCast n, ← coe_div C.toReal n]
  rw [this, ← coe_zero, tendsto_coe]
  exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal

Limit of Extended Real Sequence $\frac{C}{n}$ is Zero for Finite $C$

Informal description

For any extended real number $C \in \overline{\mathbb{R}}$ that is neither $-\infty$ nor $+\infty$, the sequence defined by $a_n = \frac{C}{n}$ converges to $0$ as $n$ tends to infinity, i.e., $\lim_{n \to \infty} \frac{C}{n} = 0$.

tendsto_one_div_add_atTop_nhds_zero_nat theorem

: Tendsto (fun n : ℕ ↦ 1 / ((n : ℝ) + 1)) atTop (𝓝 0)

Full source

theorem tendsto_one_div_add_atTop_nhds_zero_nat :
    Tendsto (fun n : ℕ ↦ 1 / ((n : ℝ) + 1)) atTop (𝓝 0) :=
  suffices Tendsto (fun n : ℕ ↦ 1 / (↑(n + 1) : ℝ)) atTop (𝓝 0) by simpa
  (tendsto_add_atTop_iff_nat 1).2 (_root_.tendsto_const_div_atTop_nhds_zero_nat 1)

Limit of Reciprocal of Successor Sequence is Zero

Informal description

The sequence defined by $a_n = \frac{1}{n + 1}$ for $n \in \mathbb{N}$ converges to $0$ as $n$ tends to infinity, i.e., $\lim_{n \to \infty} \frac{1}{n + 1} = 0$.

NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat theorem

 (𝕜 : Type*) [Semiring 𝕜] [Algebra ℝ≥0 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ≥0 𝕜] :
  Tendsto (algebraMap ℝ≥0 𝕜 ∘ fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0)

Full source

theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜]
    [Algebra ℝ≥0 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ≥0 𝕜] :
    Tendsto (algebraMapalgebraMap ℝ≥0 𝕜 ∘ fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0) := by
  convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp
    tendsto_inverse_atTop_nhds_zero_nat
  rw [map_zero]

Limit of Algebra Map Applied to Reciprocals of Natural Numbers in Nonnegative Reals is Zero

Informal description

Let $\mathbb{K}$ be a topological semiring with an algebra structure over the nonnegative real numbers $\mathbb{R}_{\geq 0}$, and suppose scalar multiplication by $\mathbb{R}_{\geq 0}$ is continuous. Then, the sequence defined by the composition of the algebra map $\text{algebraMap}_{\mathbb{R}_{\geq 0} \mathbb{K}}$ with the reciprocal function on natural numbers converges to $0$ in $\mathbb{K}$ as $n$ tends to infinity. That is, \[ \lim_{n \to \infty} \text{algebraMap}_{\mathbb{R}_{\geq 0} \mathbb{K}}\left(\frac{1}{n}\right) = 0. \]

tendsto_algebraMap_inverse_atTop_nhds_zero_nat theorem

 (𝕜 : Type*) [Semiring 𝕜] [Algebra ℝ 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ 𝕜] :
  Tendsto (algebraMap ℝ 𝕜 ∘ fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0)

Full source

theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜] [Algebra ℝ 𝕜]
    [TopologicalSpace 𝕜] [ContinuousSMul ℝ 𝕜] :
    Tendsto (algebraMapalgebraMap ℝ 𝕜 ∘ fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) :=
  NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat 𝕜

Limit of algebra map applied to reciprocals of natural numbers is zero

Informal description

Let $\mathbb{K}$ be a topological semiring with an algebra structure over the real numbers $\mathbb{R}$, and suppose scalar multiplication by $\mathbb{R}$ is continuous. Then, the sequence defined by the composition of the algebra map $\text{algebraMap}_{\mathbb{R} \mathbb{K}}$ with the reciprocal function on natural numbers converges to $0$ in $\mathbb{K}$ as $n$ tends to infinity. That is, \[ \lim_{n \to \infty} \text{algebraMap}_{\mathbb{R} \mathbb{K}}\left(\frac{1}{n}\right) = 0. \]

tendsto_natCast_div_add_atTop theorem

 {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜] [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜]
  [IsTopologicalDivisionRing 𝕜] (x : 𝕜) : Tendsto (fun n : ℕ ↦ (n : 𝕜) / (n + x)) atTop (𝓝 1)

Full source

/-- 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_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜]
    [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [IsTopologicalDivisionRing 𝕜] (x : 𝕜) :
    Tendsto (fun n : ℕ ↦ (n : 𝕜) / (n + x)) atTop (𝓝 1) := by
  convert Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _
  · exact fun n : ℕ ↦ 1 / (1 + x / n)
  · field_simp [Nat.cast_ne_zero.mpr hn]
  · have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [mul_zero, add_zero, div_one]
    rw [this]
    refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)
    simp_rw [div_eq_mul_inv]
    refine tendsto_const_nhds.mul ?_
    have := ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_zero_nat
    rw [map_zero, Filter.tendsto_atTop'] at this
    refine Iff.mpr tendsto_atTop' ?_
    intros
    simp_all only [comp_apply, map_inv₀, map_natCast]

Limit of $\frac{n}{n + x}$ as $n \to \infty$ is 1 in topological division rings

Informal description

Let $\mathbb{K}$ be a topological division ring of characteristic zero with a continuous scalar multiplication by $\mathbb{R}$ and an $\mathbb{R}$-algebra structure. For any fixed element $x \in \mathbb{K}$, the sequence $\frac{n}{n + x}$ (where $n$ is a natural number cast to $\mathbb{K}$) converges to $1$ as $n$ tends to infinity.

tendsto_mod_div_atTop_nhds_zero_nat theorem

{m : ℕ} (hm : 0 < m) : Tendsto (fun n : ℕ => ((n % m : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0)

Full source

/-- For any positive `m : ℕ`, `((n % m : ℕ) : ℝ) / (n : ℝ)` tends to `0` as `n` tends to `∞`. -/
theorem tendsto_mod_div_atTop_nhds_zero_nat {m : ℕ} (hm : 0 < m) :
    Tendsto (fun n : ℕ => ((n % m : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0) := by
  have h0 : ∀ᶠ n : ℕ in atTop, 0 ≤ (fun n : ℕ => ((n % m : ℕ) : ℝ)) n := by aesop
  exact tendsto_bdd_div_atTop_nhds_zero h0
    (.of_forall (fun n ↦  cast_le.mpr (mod_lt n hm).le)) tendsto_natCast_atTop_atTop

Convergence of Remainder-to-Term Ratio: $\frac{n \bmod m}{n} \to 0$ as $n \to \infty$

Informal description

For any positive integer $m$, the sequence $\frac{n \bmod m}{n}$ (where $n \bmod m$ is the remainder when $n$ is divided by $m$) converges to $0$ as $n$ tends to infinity.

Filter.EventuallyEq.div_mul_cancel theorem

 {α G : Type*} [GroupWithZero G] {f g : α → G} {l : Filter α} (hg : Tendsto g l (𝓟 {0}ᶜ)) :
  (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x

Full source

theorem Filter.EventuallyEq.div_mul_cancel {α G : Type*} [GroupWithZero G] {f g : α → G}
    {l : Filter α} (hg : Tendsto g l (𝓟 {0}{0}ᶜ)) : (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x := by
  filter_upwards [hg.le_comap <| preimage_mem_comap (m := g) (mem_principal_self {0}ᶜ)] with x hx
  aesop

Cancellation of Division and Multiplication in Group with Zero

Informal description

Let $G$ be a group with zero and $\alpha$ be a type. For functions $f, g : \alpha \to G$ and a filter $l$ on $\alpha$, if $g$ tends to the complement of $\{0\}$ along $l$, then the functions $x \mapsto f(x)/g(x) * g(x)$ and $x \mapsto f(x)$ are eventually equal along $l$.

Filter.EventuallyEq.div_mul_cancel_atTop theorem

 {α K : Type*} [Semifield 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

Full source

/-- If `g` tends to `∞`, then eventually for all `x` we have `(f x / g x) * g x = f x`. -/
theorem Filter.EventuallyEq.div_mul_cancel_atTop {α K : Type*}
    [Semifield 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 :=
  div_mul_cancel <| hg.mono_right <| le_principal_iff.mpr <|
    mem_of_superset (Ioi_mem_atTop 0) <| by simp

Cancellation of Division and Multiplication for Functions Tending to Infinity

Informal description

Let $K$ be a semifield with a linear order and strict ordered ring structure, and let $\alpha$ be a type. For functions $f, g : \alpha \to K$ and a filter $l$ on $\alpha$, if $g$ tends to infinity along $l$, then the functions $x \mapsto \frac{f(x)}{g(x)} \cdot g(x)$ and $x \mapsto f(x)$ are eventually equal along $l$.

Tendsto.num theorem

 {α K : Type*} [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 (𝓝 a)) :
  Tendsto f l atTop

Full source

/-- 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 {α K : Type*} [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 (𝓝 a)) :
    Tendsto f l atTop :=
  (hlim.pos_mul_atTop ha hg).congr' (EventuallyEq.div_mul_cancel_atTop hg)

Limit Comparison Test for Functions Tending to Infinity

Informal description

Let $K$ be a field with a linear order and strict ordered ring structure, equipped with the order topology. Let $f, g : \alpha \to K$ be functions and $l$ a filter on $\alpha$. If $g$ tends to infinity along $l$, and the ratio $f(x)/g(x)$ tends to a positive constant $a$ along $l$, then $f$ also tends to infinity along $l$.

Tendsto.den theorem

 {α K : Type*} [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 (𝓝 a)) : Tendsto g l atTop

Full source

/-- 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 {α K : Type*} [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 (𝓝 a)) :
    Tendsto g l atTop :=
  have hlim' : Tendsto (fun x => g x / f x) l (𝓝 a⁻¹) := by
    simp_rw [← inv_div (f _)]
    exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim
  (hlim'.pos_mul_atTop (inv_pos_of_pos ha) hf).congr' (.div_mul_cancel_atTop hf)

Limit Comparison Test for Denominator Tending to Infinity

Informal description

Let $K$ be a field with a linear order and strict ordered ring structure, equipped with the order topology and continuous inversion. Let $f, g : \alpha \to K$ be functions and $l$ a filter on $\alpha$. If $f$ tends to infinity along $l$, and the ratio $f(x)/g(x)$ tends to a positive constant $a$ along $l$, then $g$ also tends to infinity along $l$.

Tendsto.num_atTop_iff_den_atTop theorem

 {α K : Type*} [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 (𝓝 a)) :
  Tendsto f l atTop ↔ Tendsto g l atTop

Full source

/-- 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 `∞`. -/
theorem Tendsto.num_atTop_iff_den_atTop {α K : Type*}
    [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 (𝓝 a)) :
    TendstoTendsto f l atTop ↔ Tendsto g l atTop :=
  ⟨fun hf ↦ Tendsto.den hf ha hlim, fun hg ↦ Tendsto.num hg ha hlim⟩

Limit Comparison Test for Infinity: $f(x)/g(x) \to a > 0$ implies $f(x) \to \infty \leftrightarrow g(x) \to \infty$

Informal description

Let $K$ be a linearly ordered field with a strict ordered ring structure, equipped with the order topology and continuous inversion. Let $f, g : \alpha \to K$ be functions and $l$ a filter on $\alpha$. If the ratio $f(x)/g(x)$ tends to a positive constant $a$ along $l$, then $f$ tends to infinity along $l$ if and only if $g$ tends to infinity along $l$.

tendsto_add_one_pow_atTop_atTop_of_pos theorem

 [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α} (h : 0 < r) :
  Tendsto (fun n : ℕ ↦ (r + 1) ^ n) atTop atTop

Full source

theorem tendsto_add_one_pow_atTop_atTop_of_pos
    [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α}
    (h : 0 < r) : Tendsto (fun n : ℕ ↦ (r + 1) ^ n) atTop atTop :=
  tendsto_atTop_atTop_of_monotone' (pow_right_mono₀ <| le_add_of_nonneg_left h.le) <|
    not_bddAbove_iff.2 fun _ ↦ Set.exists_range_iff.2 <| add_one_pow_unbounded_of_pos _ h

Limit of $(r + 1)^n$ tends to infinity for $r > 0$ in an Archimedean ordered semiring

Informal description

Let $\alpha$ be a semiring with a linear order and strict ordered ring structure, and assume $\alpha$ is Archimedean. For any positive element $r \in \alpha$ (i.e., $0 < r$), the sequence $(r + 1)^n$ tends to infinity as $n$ tends to infinity.

tendsto_pow_atTop_atTop_of_one_lt theorem

 [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α} (h : 1 < r) :
  Tendsto (fun n : ℕ ↦ r ^ n) atTop atTop

Full source

theorem tendsto_pow_atTop_atTop_of_one_lt
    [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α}
    (h : 1 < r) : Tendsto (fun n : ℕ ↦ r ^ n) atTop atTop :=
  sub_add_cancel r 1 ▸ tendsto_add_one_pow_atTop_atTop_of_pos (sub_pos.2 h)

Exponential Growth: $r^n \to \infty$ for $r > 1$ in an Archimedean ordered ring

Informal description

Let $\alpha$ be a ring with a linear order and strict ordered ring structure, and assume $\alpha$ is Archimedean. For any element $r \in \alpha$ with $r > 1$, the sequence $r^n$ tends to infinity as $n$ tends to infinity.

Nat.tendsto_pow_atTop_atTop_of_one_lt theorem

{m : ℕ} (h : 1 < m) : Tendsto (fun n : ℕ ↦ m ^ n) atTop atTop

Full source

theorem Nat.tendsto_pow_atTop_atTop_of_one_lt {m : ℕ} (h : 1 < m) :
    Tendsto (fun n : ℕ ↦ m ^ n) atTop atTop :=
  tsub_add_cancel_of_le (le_of_lt h) ▸ tendsto_add_one_pow_atTop_atTop_of_pos (tsub_pos_of_lt h)

Exponential Growth of Natural Powers: $m^n \to \infty$ for $m > 1$

Informal description

For any natural number $m > 1$, the sequence $m^n$ tends to infinity as $n$ tends to infinity.

tendsto_pow_atTop_nhds_zero_of_lt_one theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜]
  {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0)

Full source

theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) :=
  h₁.eq_or_lt.elim
    (fun hr ↦ (tendsto_add_atTop_iff_nat 1).mp <| by
      simp [_root_.pow_succ, ← hr, tendsto_const_nhds])
    (fun hr ↦
      have := (one_lt_inv₀ hr).2 h₂ |> tendsto_pow_atTop_atTop_of_one_lt
      (tendsto_inv_atTop_zero.comp this).congr fun n ↦ by simp)

Geometric Decay: $r^n \to 0$ for $0 \leq r < 1$ in an Archimedean ordered field

Informal description

Let $\mathbb{K}$ be a field with a linear order and strict ordered ring structure, which is Archimedean and equipped with the order topology. For any $r \in \mathbb{K}$ satisfying $0 \leq r < 1$, the sequence $r^n$ tends to $0$ as $n$ tends to infinity.

tendsto_pow_atTop_nhds_zero_iff theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜]
  {r : 𝕜} : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1

Full source

@[simp] theorem tendsto_pow_atTop_nhds_zero_iff {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} :
    TendstoTendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) ↔ |r| < 1 := by
  rw [tendsto_zero_iff_abs_tendsto_zero]
  refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩
  · by_cases hr : 1 = |r|
    · replace h : Tendsto (fun n : ℕ ↦ |r|^n) atTop (𝓝 0) := by simpa only [← abs_pow, h]
      simp only [hr.symm, one_pow] at h
      exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds
    · apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
      · refine (pow_right_strictMono₀ <| lt_of_le_of_ne (le_of_not_lt hr_le)
          hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
        obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_lt hr_le) hr))
        exact ⟨n, le_of_lt hn⟩
      · simpa only [← abs_pow]
  · simpa only [← abs_pow] using (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h

Geometric Decay Criterion: $r^n \to 0 \iff |r| < 1$ in Archimedean Ordered Fields

Informal description

Let $\mathbb{K}$ be a linearly ordered field with a strict ordered ring structure, which is Archimedean and equipped with the order topology. For any $r \in \mathbb{K}$, the sequence $r^n$ tends to $0$ as $n$ tends to infinity if and only if the absolute value of $r$ is less than $1$, i.e., $|r| < 1$.

tendsto_pow_atTop_nhdsWithin_zero_of_lt_one theorem

 {𝕜 : Type*} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜]
  {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝[>] 0)

Full source

theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type*}
    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝[>] 0) :=
  tendsto_inf.2
    ⟨tendsto_pow_atTop_nhds_zero_of_lt_one h₁.le h₂,
      tendsto_principal.2 <| Eventually.of_forall fun _ ↦ pow_pos h₁ _⟩

Right-sided geometric decay: $r^n \searrow 0^+$ for $0 < r < 1$ in an Archimedean ordered field

Informal description

Let $\mathbb{K}$ be a field with a linear order and strict ordered ring structure, which is Archimedean and equipped with the order topology. For any $r \in \mathbb{K}$ satisfying $0 < r < 1$, the sequence $r^n$ tends to $0$ from above as $n$ tends to infinity. That is, for any neighborhood of $0$ in the right-sided topology (i.e., containing only positive elements), there exists $N \in \mathbb{N}$ such that for all $n \geq N$, $0 < r^n$ and $r^n$ lies in the neighborhood.

uniformity_basis_dist_pow_of_lt_one theorem

 {α : Type*} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r) (h₁ : r < 1) :
  (uniformity α).HasBasis (fun _ : ℕ ↦ True) fun k ↦ {p : α × α | dist p.1 p.2 < r ^ k}

Full source

theorem uniformity_basis_dist_pow_of_lt_one {α : Type*} [PseudoMetricSpace α] {r : ℝ} (h₀ : 0 < r)
    (h₁ : r < 1) :
    (uniformity α).HasBasis (fun _ : ℕ ↦ True) fun k ↦ { p : α × α | dist p.1 p.2 < r ^ k } :=
  Metric.mk_uniformity_basis (fun _ _ ↦ pow_pos h₀ _) fun _ ε0 ↦
    (exists_pow_lt_of_lt_one ε0 h₁).imp fun _ hk ↦ ⟨trivial, hk.le⟩

Uniformity Basis via Powers of $r$ in Pseudometric Spaces

Informal description

Let $α$ be a pseudometric space and $r$ a real number with $0 < r < 1$. Then the uniformity on $α$ has a basis consisting of all sets of pairs $(x,y)$ such that the distance between $x$ and $y$ is less than $r^k$ for some natural number $k$.

geom_lt theorem

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

Full 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 := by
  apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h
  · simp
  · simp [_root_.pow_succ', mul_assoc, le_refl]

Strict Geometric Lower Bound for Sequences: $c^n u_0 < u_n$

Informal description

Let $u : \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers and let $c \geq 0$ be a nonnegative real number. For any positive integer $n > 0$, if for every $k < n$ the inequality $c \cdot u(k) < u(k+1)$ holds, then $c^n \cdot u(0) < u(n)$.

geom_le theorem

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

Full 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 := by
  apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h <;>
    simp [_root_.pow_succ', mul_assoc, le_refl]

Geometric Lower Bound for Sequences: $c^n u_0 \leq u_n$

Informal description

Let $u : \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers and let $c \geq 0$ be a nonnegative real number. If for every natural number $k < n$, the inequality $c \cdot u(k) \leq u(k+1)$ holds, then $c^n \cdot u(0) \leq u(n)$.

lt_geom theorem

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

Full 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 := by
  apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _
  · simp
  · simp [_root_.pow_succ', mul_assoc, le_refl]

Strict Geometric Upper Bound for Sequences: $u_n < c^n u_0$

Informal description

Let $u : \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers, and let $c \geq 0$ be a nonnegative real number. For any positive natural number $n > 0$, if for every $k < n$ the inequality $u(k+1) < c \cdot u(k)$ holds, then $u(n) < c^n \cdot u(0)$.

le_geom theorem

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

Full 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 := by
  apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _ <;>
    simp [_root_.pow_succ', mul_assoc, le_refl]

Geometric Bound for Sequences: $u_n \leq c^n u_0$

Informal description

Let $u : \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers, and let $c \geq 0$ be a nonnegative real number. If for every natural number $k < n$, the inequality $u(k+1) \leq c \cdot u(k)$ holds, then $u(n) \leq c^n \cdot u(0)$.

tendsto_atTop_of_geom_le theorem

{v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (hc : 1 < c) (hu : ∀ n, c * v n ≤ v (n + 1)) : Tendsto v atTop atTop

Full source

/-- If a sequence `v` of real numbers satisfies `k * v n ≤ v (n+1)` with `1 < k`,
then it goes to +∞. -/
theorem tendsto_atTop_of_geom_le {v : ℕ → ℝ} {c : ℝ} (h₀ : 0 < v 0) (hc : 1 < c)
    (hu : ∀ n, c * v n ≤ v (n + 1)) : Tendsto v atTop atTop :=
  (tendsto_atTop_mono fun n ↦ geom_le (zero_le_one.trans hc.le) n fun k _ ↦ hu k) <|
    (tendsto_pow_atTop_atTop_of_one_lt hc).atTop_mul_const h₀

Divergence of Sequences with Geometric Lower Bound: $v(n) \to \infty$ when $c \cdot v(n) \leq v(n+1)$ for $c > 1$

Informal description

Let $v : \mathbb{N} \to \mathbb{R}$ be a sequence of real numbers with $v(0) > 0$, and let $c > 1$ be a real number. If for every natural number $n$, the inequality $c \cdot v(n) \leq v(n+1)$ holds, then the sequence $v(n)$ tends to infinity as $n$ tends to infinity.

NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one theorem

{r : ℝ≥0} (hr : r < 1) : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0)

Full source

theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) :=
  NNReal.tendsto_coe.1 <| by
    simp only [NNReal.coe_pow, NNReal.coe_zero,
      _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr]

Geometric Decay in Nonnegative Reals: $r^n \to 0$ for $0 \leq r < 1$

Informal description

For any nonnegative real number $r \in \mathbb{R}_{\geq 0}$ with $r < 1$, the sequence $r^n$ tends to $0$ as $n$ tends to infinity.

NNReal.tendsto_pow_atTop_nhds_zero_iff theorem

{r : ℝ≥0} : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1

Full source

@[simp]
protected theorem NNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0} :
    TendstoTendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 :=
  ⟨fun h => by simpa [coe_pow, coe_zero, abs_eq, coe_lt_one, val_eq_coe] using
    tendsto_pow_atTop_nhds_zero_iff.mp <| tendsto_coe.mpr h, tendsto_pow_atTop_nhds_zero_of_lt_one⟩

Geometric Decay Criterion in Nonnegative Reals: $r^n \to 0 \iff r < 1$

Informal description

For a nonnegative real number $r \in \mathbb{R}_{\geq 0}$, the sequence $r^n$ tends to $0$ as $n$ tends to infinity if and only if $r < 1$.

ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one theorem

{r : ℝ≥0∞} (hr : r < 1) : Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0)

Full source

theorem ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0∞} (hr : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) := by
  rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
  rw [← ENNReal.coe_zero]
  norm_cast at *
  apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

Geometric Decay in Extended Nonnegative Reals: $r^n \to 0$ for $0 \leq r < 1$

Informal description

For any extended non-negative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $r < 1$, the sequence of powers $(r^n)_{n \in \mathbb{N}}$ converges to $0$ as $n$ tends to infinity.

ENNReal.tendsto_pow_atTop_nhds_zero_iff theorem

{r : ℝ≥0∞} : Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1

Full source

@[simp]
protected theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} :
    TendstoTendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1 := by
  refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩
  lift r to NNReal
  · refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))
    exact eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩
  rw [← coe_zero] at h
  norm_cast at h ⊢
  exact NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h

Geometric Decay Criterion in Extended Nonnegative Reals: $r^n \to 0 \iff r < 1$

Informal description

For any extended non-negative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sequence of powers $(r^n)_{n \in \mathbb{N}}$ converges to $0$ as $n$ tends to infinity if and only if $r < 1$.

ENNReal.tendsto_pow_atTop_nhds_top_iff theorem

{r : ℝ≥0∞} : Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞) ↔ 1 < r

Full source

@[simp]
protected theorem ENNReal.tendsto_pow_atTop_nhds_top_iff {r : ℝ≥0∞} :
    TendstoTendsto (fun n ↦ r^n) atTop (𝓝 ∞) ↔ 1 < r := by
  refine ⟨?_, ?_⟩
  · contrapose!
    intro r_le_one h_tends
    specialize h_tends (Ioi_mem_nhds one_lt_top)
    simp only [Filter.mem_map, mem_atTop_sets, ge_iff_le, Set.mem_preimage, Set.mem_Ioi] at h_tends
    obtain ⟨n, hn⟩ := h_tends
    exact lt_irrefl _ <| lt_of_lt_of_le (hn n le_rfl) <| pow_le_one₀ (zero_le _) r_le_one
  · intro r_gt_one
    have obs := @Tendsto.inv ℝ≥0∞ ℕ _ _ _ (fun n ↦ (r⁻¹)^n) atTop 0
    simp only [ENNReal.tendsto_pow_atTop_nhds_zero_iff, inv_zero] at obs
    simpa [← ENNReal.inv_pow] using obs <| ENNReal.inv_lt_one.mpr r_gt_one

Limit Characterization: $(r^n) \to \infty$ iff $r > 1$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$

Informal description

For any extended non-negative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sequence of powers $(r^n)_{n \in \mathbb{N}}$ tends to $\infty$ in the order topology if and only if $r > 1$.

hasSum_geometric_of_lt_one theorem

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

Full source

theorem hasSum_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹ :=
  have : r ≠ 1 := ne_of_lt h₂
  have : Tendsto (fun n ↦ (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹)) :=
    ((tendsto_pow_atTop_nhds_zero_of_lt_one h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds
  (hasSum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr <| by
    simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]

Convergence of Geometric Series for $0 \leq r < 1$ to $(1 - r)^{-1}$

Informal description

For any real number $r$ satisfying $0 \leq r < 1$, the geometric series $\sum_{n=0}^\infty r^n$ converges to $(1 - r)^{-1}$.

summable_geometric_of_lt_one theorem

{r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : Summable fun n : ℕ ↦ r ^ n

Full source

theorem summable_geometric_of_lt_one {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    Summable fun n : ℕ ↦ r ^ n :=
  ⟨_, hasSum_geometric_of_lt_one h₁ h₂⟩

Summability of Geometric Series for $0 \leq r < 1$

Informal description

For any real number $r$ satisfying $0 \leq r < 1$, the geometric series $\sum_{n=0}^\infty r^n$ is summable.

tsum_geometric_of_lt_one theorem

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

Full source

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

Sum of Geometric Series: $\sum_{n=0}^\infty r^n = (1 - r)^{-1}$ for $0 \leq r < 1$

Informal description

For any real number $r$ with $0 \leq r < 1$, the sum of the geometric series $\sum_{n=0}^\infty r^n$ equals $(1 - r)^{-1}$.

hasSum_geometric_two theorem

: HasSum (fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n) 2

Full source

theorem hasSum_geometric_two : HasSum (fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n) 2 := by
  convert hasSum_geometric_of_lt_one _ _ <;> norm_num

Convergence of Geometric Series $\sum (1/2)^n = 2$

Informal description

The geometric series $\sum_{n=0}^\infty \left(\frac{1}{2}\right)^n$ converges to $2$.

summable_geometric_two theorem

: Summable fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n

Full source

theorem summable_geometric_two : Summable fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n :=
  ⟨_, hasSum_geometric_two⟩

Summability of Geometric Series $\sum (1/2)^n$

Informal description

The geometric series $\sum_{n=0}^\infty \left(\frac{1}{2}\right)^n$ is summable.

summable_geometric_two_encode theorem

{ι : Type*} [Encodable ι] : Summable fun i : ι ↦ (1 / 2 : ℝ) ^ Encodable.encode i

Full source

theorem summable_geometric_two_encode {ι : Type*} [Encodable ι] :
    Summable fun i : ι ↦ (1 / 2 : ℝ) ^ Encodable.encode i :=
  summable_geometric_two.comp_injective Encodable.encode_injective

Summability of Geometric Series $\sum (1/2)^{\text{encode}(i)}$ over Encodable Types

Informal description

For any encodable type $\iota$, the series $\sum_{i \in \iota} \left(\frac{1}{2}\right)^{\text{encode}(i)}$ is summable.

tsum_geometric_two theorem

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

Full source

theorem tsum_geometric_two : (∑' n : ℕ, ((1 : ℝ) / 2) ^ n) = 2 :=
  hasSum_geometric_two.tsum_eq

Sum of Geometric Series $\sum (1/2)^n = 2$

Informal description

The infinite series $\sum_{n=0}^\infty \left(\frac{1}{2}\right)^n$ converges to $2$.

sum_geometric_two_le theorem

(n : ℕ) : (∑ i ∈ range n, (1 / (2 : ℝ)) ^ i) ≤ 2

Full source

theorem sum_geometric_two_le (n : ℕ) : (∑ i ∈ range n, (1 / (2 : ℝ)) ^ i) ≤ 2 := by
  have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
    intro i
    apply pow_nonneg
    norm_num
  convert summable_geometric_two.sum_le_tsum (range n) (fun i _ ↦ this i)
  exact tsum_geometric_two.symm

Finite Geometric Series Bound: $\sum_{i=0}^{n-1} (1/2)^i \leq 2$

Informal description

For any natural number $n$, the finite sum $\sum_{i=0}^{n-1} \left(\frac{1}{2}\right)^i$ is less than or equal to 2.

tsum_geometric_inv_two theorem

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

Full source

theorem tsum_geometric_inv_two : (∑' n : ℕ, (2 : ℝ)⁻¹ ^ n) = 2 :=
  (inv_eq_one_div (2 : ℝ)).symm ▸ tsum_geometric_two

Sum of Geometric Series $\sum (1/2)^n = 2$

Informal description

The infinite series $\sum_{n=0}^\infty \left(\frac{1}{2}\right)^n$ converges to $2$.

tsum_geometric_inv_two_ge theorem

(n : ℕ) : (∑' i, ite (n ≤ i) ((2 : ℝ)⁻¹ ^ i) 0) = 2 * 2⁻¹ ^ n

Full source

/-- The sum of `2⁻¹ ^ i` for `n ≤ i` equals `2 * 2⁻¹ ^ n`. -/
theorem tsum_geometric_inv_two_ge (n : ℕ) :
    (∑' i, ite (n ≤ i) ((2 : ℝ)⁻¹ ^ i) 0) = 2 * 2⁻¹ ^ n := by
  have A : Summable fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0 := by
    simpa only [← piecewise_eq_indicator, one_div]
      using summable_geometric_two.indicator {i | n ≤ i}
  have B : ((Finset.range n).sum fun i : ℕ ↦ ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
    Finset.sum_eq_zero fun i hi ↦
      ite_eq_right_iff.2 fun h ↦ (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim
  simp only [← Summable.sum_add_tsum_nat_add n A, B, if_true, zero_add, zero_le',
    le_add_iff_nonneg_left, pow_add, _root_.tsum_mul_right, tsum_geometric_inv_two]

Sum of Tail of Geometric Series: $\sum_{i=n}^\infty (1/2)^i = 2 \cdot (1/2)^n$

Informal description

For any natural number $n$, the sum of the geometric series $\sum_{i=n}^\infty \left(\frac{1}{2}\right)^i$ equals $2 \cdot \left(\frac{1}{2}\right)^n$.

hasSum_geometric_two' theorem

(a : ℝ) : HasSum (fun n : ℕ ↦ a / 2 / 2 ^ n) a

Full source

theorem hasSum_geometric_two' (a : ℝ) : HasSum (fun n : ℕ ↦ a / 2 / 2 ^ n) a := by
  convert HasSum.mul_left (a / 2)
      (hasSum_geometric_of_lt_one (le_of_lt one_half_pos) one_half_lt_one) using 1
  · funext n
    simp only [one_div, inv_pow]
    rfl
  · norm_num

Convergence of the Series $\sum_{n=0}^\infty \frac{a}{2^{n+1}}$ to $a$

Informal description

For any real number $a$, the series $\sum_{n=0}^\infty \frac{a}{2^{n+1}}$ converges to $a$.

summable_geometric_two' theorem

(a : ℝ) : Summable fun n : ℕ ↦ a / 2 / 2 ^ n

Full source

theorem summable_geometric_two' (a : ℝ) : Summable fun n : ℕ ↦ a / 2 / 2 ^ n :=
  ⟨a, hasSum_geometric_two' a⟩

Summability of the Series $\sum_{n=0}^\infty \frac{a}{2^{n+1}}$

Informal description

For any real number $a$, the series $\sum_{n=0}^\infty \frac{a}{2^{n+1}}$ is summable.

tsum_geometric_two' theorem

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

Full source

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

Sum of Geometric Series $\sum_{n=0}^\infty \frac{a}{2^{n+1}} = a$

Informal description

For any real number $a$, the sum of the series $\sum_{n=0}^\infty \frac{a}{2^{n+1}}$ equals $a$.

NNReal.hasSum_geometric theorem

{r : ℝ≥0} (hr : r < 1) : HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹

Full source

/-- **Sum of a Geometric Series** -/
theorem NNReal.hasSum_geometric {r : ℝ≥0} (hr : r < 1) : HasSum (fun n : ℕ ↦ r ^ n) (1 - r)⁻¹ := by
  apply NNReal.hasSum_coe.1
  push_cast
  rw [NNReal.coe_sub (le_of_lt hr)]
  exact hasSum_geometric_of_lt_one r.coe_nonneg hr

Convergence of Geometric Series in Nonnegative Reals: $\sum_{n=0}^\infty r^n = (1 - r)^{-1}$ for $0 \leq r < 1$

Informal description

For any nonnegative real number $r < 1$, the geometric series $\sum_{n=0}^\infty r^n$ converges to $(1 - r)^{-1}$ in the space of nonnegative real numbers.

NNReal.summable_geometric theorem

{r : ℝ≥0} (hr : r < 1) : Summable fun n : ℕ ↦ r ^ n

Full source

theorem NNReal.summable_geometric {r : ℝ≥0} (hr : r < 1) : Summable fun n : ℕ ↦ r ^ n :=
  ⟨_, NNReal.hasSum_geometric hr⟩

Summability of Geometric Series in Nonnegative Reals for $0 \leq r < 1$

Informal description

For any nonnegative real number $r < 1$, the geometric series $\sum_{n=0}^\infty r^n$ is summable in the space of nonnegative real numbers.

tsum_geometric_nnreal theorem

{r : ℝ≥0} (hr : r < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹

Full source

theorem tsum_geometric_nnreal {r : ℝ≥0} (hr : r < 1) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ :=
  (NNReal.hasSum_geometric hr).tsum_eq

Geometric Series Sum Formula in Nonnegative Reals: $\sum_{n=0}^\infty r^n = (1 - r)^{-1}$ for $0 \leq r < 1$

Informal description

For any nonnegative real number $r < 1$, the sum of the geometric series $\sum_{n=0}^\infty r^n$ converges to $(1 - r)^{-1}$.

ENNReal.tsum_geometric theorem

(r : ℝ≥0∞) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹

Full source

/-- The series `pow r` converges to `(1-r)⁻¹`. For `r < 1` the RHS is a finite number,
and for `1 ≤ r` the RHS equals `∞`. -/
@[simp]
theorem ENNReal.tsum_geometric (r : ℝ≥0∞) : ∑' n : ℕ, r ^ n = (1 - r)⁻¹ := by
  rcases lt_or_le r 1 with hr | hr
  · rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
    norm_cast at *
    convert ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
    rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
  · rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
    refine fun a ha ↦
      (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn ↦ lt_of_lt_of_le hn ?_
    calc
      (n : ℝ≥0∞) = ∑ i ∈ range n, 1 := by rw [sum_const, nsmul_one, card_range]
      _ ≤ ∑ i ∈ range n, r ^ i := by gcongr; apply one_le_pow₀ hr

Sum of Geometric Series in Extended Non-Negative Reals: $\sum_{n=0}^\infty r^n = (1 - r)^{-1}$

Informal description

For any extended non-negative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sum of the geometric series $\sum_{n=0}^\infty r^n$ converges to $(1 - r)^{-1}$. When $r < 1$, the right-hand side is finite, and when $1 \leq r$, the right-hand side equals $\infty$.

ENNReal.tsum_geometric_add_one theorem

(r : ℝ≥0∞) : ∑' n : ℕ, r ^ (n + 1) = r * (1 - r)⁻¹

Full source

theorem ENNReal.tsum_geometric_add_one (r : ℝ≥0∞) : ∑' n : ℕ, r ^ (n + 1) = r * (1 - r)⁻¹ := by
  simp only [_root_.pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric]

Sum of Shifted Geometric Series in Extended Non-Negative Reals: $\sum_{n=0}^\infty r^{n+1} = r(1 - r)^{-1}$

Informal description

For any extended non-negative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sum of the shifted geometric series $\sum_{n=0}^\infty r^{n+1}$ converges to $r \cdot (1 - r)^{-1}$. When $r < 1$, the right-hand side is finite, and when $1 \leq r$, the right-hand side equals $\infty$.

cauchySeq_of_edist_le_geometric theorem

: CauchySeq f

Full source

/-- If `edist (f n) (f (n+1))` is bounded by `C * r^n`, `C ≠ ∞`, `r < 1`,
then `f` is a Cauchy sequence. -/
theorem cauchySeq_of_edist_le_geometric : CauchySeq f := by
  refine cauchySeq_of_edist_le_of_tsum_ne_top _ hu ?_
  rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
  refine ENNReal.mul_ne_top hC (ENNReal.inv_ne_top.2 ?_)
  exact (tsub_pos_iff_lt.2 hr).ne'

Cauchy Criterion for Sequences with Geometric Decay in Extended Distance

Informal description

Let $\{f(n)\}_{n \in \mathbb{N}}$ be a sequence in an extended metric space $\alpha$. If there exist constants $C \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $C \neq \infty$ and $r \in [0,1)$ such that for all $n \in \mathbb{N}$, the extended distance between consecutive terms satisfies $\text{edist}(f(n), f(n+1)) \leq C \cdot r^n$, then the sequence $\{f(n)\}$ is a Cauchy sequence.

edist_le_of_edist_le_geometric_of_tendsto theorem

{a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) : edist (f n) a ≤ C * r ^ n / (1 - r)

Full source

/-- 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 {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    edist (f n) a ≤ C * r ^ n / (1 - r) := by
  convert edist_le_tsum_of_edist_le_of_tendsto _ hu ha _
  simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]

Bound on limit distance for sequences with geometrically decaying consecutive differences: $\text{edist}(f_n, a) \leq \frac{C r^n}{1 - r}$

Informal description

Let $(f_n)_{n \in \mathbb{N}}$ be a sequence in an extended metric space $\alpha$ and let $C \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $C \neq \infty$ and $r \in [0,1)$. Suppose that for all $n \in \mathbb{N}$, the extended distance between consecutive terms satisfies $\text{edist}(f_n, f_{n+1}) \leq C r^n$. If the sequence $(f_n)$ converges to a limit $a \in \alpha$, then for any $n \in \mathbb{N}$, the distance from $f_n$ to $a$ is bounded by: \[ \text{edist}(f_n, a) \leq \frac{C r^n}{1 - r}. \]

edist_le_of_edist_le_geometric_of_tendsto₀ theorem

{a : α} (ha : Tendsto f atTop (𝓝 a)) : edist (f 0) a ≤ C / (1 - r)

Full source

/-- 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 edist_le_of_edist_le_geometric_of_tendsto₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) :
    edist (f 0) a ≤ C / (1 - r) := by
  simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0

Initial Term Distance Bound for Sequences with Geometric Decay: $\text{edist}(f_0, a) \leq \frac{C}{1 - r}$

Informal description

Let $(f_n)_{n \in \mathbb{N}}$ be a sequence in an extended metric space $\alpha$ and let $C \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $C \neq \infty$ and $r \in [0,1)$. Suppose that for all $n \in \mathbb{N}$, the extended distance between consecutive terms satisfies $\text{edist}(f_n, f_{n+1}) \leq C r^n$. If the sequence $(f_n)$ converges to a limit $a \in \alpha$, then the distance from the initial term $f_0$ to $a$ is bounded by: \[ \text{edist}(f_0, a) \leq \frac{C}{1 - r}. \]

cauchySeq_of_edist_le_geometric_two theorem

: CauchySeq f

Full source

/-- If `edist (f n) (f (n+1))` is bounded by `C * 2^-n`, then `f` is a Cauchy sequence. -/
theorem cauchySeq_of_edist_le_geometric_two : CauchySeq f := by
  simp only [div_eq_mul_inv, ENNReal.inv_pow] at hu
  refine cauchySeq_of_edist_le_geometric 2⁻¹ C ?_ hC hu
  simp [ENNReal.one_lt_two]

Cauchy Criterion for Sequences with Exponentially Decaying Distance (Base 2)

Informal description

Let $\{f(n)\}_{n \in \mathbb{N}}$ be a sequence in an extended metric space $\alpha$. If there exists a constant $C \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $C \neq \infty$ such that for all $n \in \mathbb{N}$, the extended distance between consecutive terms satisfies $\text{edist}(f(n), f(n+1)) \leq C \cdot 2^{-n}$, then the sequence $\{f(n)\}$ is a Cauchy sequence.

edist_le_of_edist_le_geometric_two_of_tendsto theorem

(n : ℕ) : edist (f n) a ≤ 2 * C / 2 ^ n

Full source

/-- 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 (n : ℕ) : edist (f n) a ≤ 2 * C / 2 ^ n := by
  simp only [div_eq_mul_inv, ENNReal.inv_pow] at *
  rw [mul_assoc, mul_comm]
  convert edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1
  rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]

Bound on limit distance for sequences with exponentially decaying consecutive differences (base 2): $\text{edist}(f_n, a) \leq 2C/2^n$

Informal description

Let $(f_n)_{n \in \mathbb{N}}$ be a sequence in an extended metric space $\alpha$ converging to a limit $a \in \alpha$. If there exists a constant $C \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $C \neq \infty$ such that for all $n \in \mathbb{N}$, the extended distance between consecutive terms satisfies $\text{edist}(f_n, f_{n+1}) \leq C \cdot 2^{-n}$, then for any $n \in \mathbb{N}$, the distance from $f_n$ to $a$ is bounded by: \[ \text{edist}(f_n, a) \leq \frac{2C}{2^n}. \]

edist_le_of_edist_le_geometric_two_of_tendsto₀ theorem

: edist (f 0) a ≤ 2 * C

Full source

/-- 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 edist_le_of_edist_le_geometric_two_of_tendsto₀ : edist (f 0) a ≤ 2 * C := by
  simpa only [_root_.pow_zero, div_eq_mul_inv, inv_one, mul_one] using
    edist_le_of_edist_le_geometric_two_of_tendsto C hu ha 0

Initial Term to Limit Distance Bound for Exponentially Decaying Sequences (Base 2): $\text{edist}(f_0, a) \leq 2C$

Informal description

Let $(f_n)_{n \in \mathbb{N}}$ be a sequence in an extended metric space $\alpha$ converging to a limit $a \in \alpha$. If there exists a constant $C \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $C \neq \infty$ such that for all $n \in \mathbb{N}$, the extended distance between consecutive terms satisfies $\text{edist}(f_n, f_{n+1}) \leq C \cdot 2^{-n}$, then the distance from the initial term $f_0$ to the limit $a$ is bounded by: \[ \text{edist}(f_0, a) \leq 2C. \]

aux_hasSum_of_le_geometric theorem

: HasSum (fun n : ℕ ↦ C * r ^ n) (C / (1 - r))

Full source

/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence. -/
theorem aux_hasSum_of_le_geometric : HasSum (fun n : ℕ ↦ C * r ^ n) (C / (1 - r)) := by
  rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)
  · simp [hasSum_zero]
  · refine HasSum.mul_left C ?_
    simpa using hasSum_geometric_of_lt_one r₀ hr

Sum of Geometric Series with Coefficient $C$: $\sum_{n=0}^\infty C r^n = C / (1 - r)$ for $0 \leq r < 1$

Informal description

For any real numbers $C$ and $r$ with $0 \leq r < 1$, the series $\sum_{n=0}^\infty C r^n$ converges to $C / (1 - r)$.

cauchySeq_of_le_geometric theorem

: CauchySeq f

Full source

/-- 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 cauchySeq_of_le_geometric : CauchySeq f :=
  cauchySeq_of_dist_le_of_summable _ hu ⟨_, aux_hasSum_of_le_geometric hr hu⟩

Cauchy Criterion for Sequences with Geometric Decay in Distance

Informal description

Let $(f(n))_{n \in \mathbb{N}}$ be a sequence in a metric space such that the distance between consecutive terms satisfies $\mathrm{dist}(f(n), f(n+1)) \leq C r^n$ for some constants $C$ and $r$ with $r < 1$. Then $f$ is a Cauchy sequence.

dist_le_of_le_geometric_of_tendsto₀ theorem

{a : α} (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ C / (1 - r)

Full source

/-- 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₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) :
    dist (f 0) a ≤ C / (1 - r) :=
  (aux_hasSum_of_le_geometric hr hu).tsum_eq ▸
    dist_le_tsum_of_dist_le_of_tendsto₀ _ hu ⟨_, aux_hasSum_of_le_geometric hr hu⟩ ha

Bound on Initial Distance to Limit for Geometric Decay Sequences

Informal description

Let $(f_n)$ be a sequence in a metric space $\alpha$ such that the distance between consecutive terms satisfies $\mathrm{dist}(f_n, f_{n+1}) \leq C r^n$ for some constants $C \geq 0$ and $0 \leq r < 1$. If the sequence converges to a limit $a \in \alpha$, then the distance from the first term to the limit is bounded by $\mathrm{dist}(f_0, a) \leq \frac{C}{1 - r}$.

dist_le_of_le_geometric_of_tendsto theorem

{a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) : dist (f n) a ≤ C * r ^ n / (1 - r)

Full source

/-- 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 dist_le_of_le_geometric_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ C * r ^ n / (1 - r) := by
  have := aux_hasSum_of_le_geometric hr hu
  convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n
  simp only [pow_add, mul_left_comm C, mul_div_right_comm]
  rw [mul_comm]
  exact (this.mul_left _).tsum_eq.symm

Distance Bound for Sequences with Geometric Decay: $\text{dist}(f_n, a) \leq \frac{C r^n}{1 - r}$

Informal description

Let $(f_n)$ be a sequence in a metric space $\alpha$ such that $\text{dist}(f_n, f_{n+1}) \leq C r^n$ for some constants $C \geq 0$ and $0 \leq r < 1$. If $f_n$ converges to a limit $a \in \alpha$, then for any $n \in \mathbb{N}$, the distance from $f_n$ to $a$ satisfies: \[ \text{dist}(f_n, a) \leq \frac{C r^n}{1 - r}. \]

cauchySeq_of_le_geometric_two theorem

: CauchySeq f

Full source

/-- If `dist (f n) (f (n+1))` is bounded by `(C / 2) / 2^n`, then `f` is a Cauchy sequence. -/
theorem cauchySeq_of_le_geometric_two : CauchySeq f :=
  cauchySeq_of_dist_le_of_summable _ hu₂ <| ⟨_, hasSum_geometric_two' C⟩

Cauchy Criterion for Sequences with Geometric Decay of Consecutive Distances

Informal description

Let $(f_n)$ be a sequence in a metric space such that the distance between consecutive terms satisfies $\mathrm{dist}(f_n, f_{n+1}) \leq \frac{C}{2^{n+1}}$ for some constant $C > 0$. Then $(f_n)$ is a Cauchy sequence.

dist_le_of_le_geometric_two_of_tendsto₀ theorem

{a : α} (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ C

Full source

/-- 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₀ {a : α} (ha : Tendsto f atTop (𝓝 a)) :
    dist (f 0) a ≤ C :=
  tsum_geometric_two' C ▸ dist_le_tsum_of_dist_le_of_tendsto₀ _ hu₂ (summable_geometric_two' C) ha

Distance Bound for Initial Term in Sequences with Geometric Decay: $\mathrm{dist}(f_0, a) \leq C$

Informal description

Let $(f_n)$ be a sequence in a metric space $\alpha$ such that $\mathrm{dist}(f_n, f_{n+1}) \leq \frac{C}{2^{n+1}}$ for some constant $C > 0$. If $f_n$ converges to a limit $a \in \alpha$, then the distance from the initial term $f_0$ to $a$ satisfies: \[ \mathrm{dist}(f_0, a) \leq C. \]

dist_le_of_le_geometric_two_of_tendsto theorem

{a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) : dist (f n) a ≤ C / 2 ^ n

Full source

/-- 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`. -/
theorem dist_le_of_le_geometric_two_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    dist (f n) a ≤ C / 2 ^ n := by
  convert dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n
  simp only [add_comm n, pow_add, ← div_div]
  symm
  exact ((hasSum_geometric_two' C).div_const _).tsum_eq

Distance Bound for Sequences with Geometric Decay of Consecutive Distances

Informal description

Let $(f_n)$ be a sequence in a metric space $\alpha$ converging to a limit $a \in \alpha$, and suppose there exists $C > 0$ such that for all $n \in \mathbb{N}$, the distance between consecutive terms satisfies $\mathrm{dist}(f_n, f_{n+1}) \leq \frac{C}{2^{n+1}}$. Then for any $n \in \mathbb{N}$, the distance from $f_n$ to the limit satisfies $\mathrm{dist}(f_n, a) \leq \frac{C}{2^n}$.

summable_one_div_pow_of_le theorem

{m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi : ∀ i, i ≤ f i) : Summable fun i ↦ 1 / m ^ f i

Full source

/-- A series whose terms are bounded by the terms of a converging geometric series converges. -/
theorem summable_one_div_pow_of_le {m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi : ∀ i, i ≤ f i) :
    Summable fun i ↦ 1 / m ^ f i := by
  refine .of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
      (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
        ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
  rw [div_pow, one_pow]
  refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a)) <;>
    exact pow_pos (zero_lt_one.trans hm) _

Summability of $\frac{1}{m^{f(i)}}$ for $m > 1$ and $i \leq f(i)$

Informal description

For any real number $m > 1$ and any function $f \colon \mathbb{N} \to \mathbb{N}$ satisfying $i \leq f(i)$ for all $i \in \mathbb{N}$, the series $\sum_{i=0}^\infty \frac{1}{m^{f(i)}}$ is summable.

posSumOfEncodable definition

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

Full source

/-- For any positive `ε`, define on an encodable type a positive sequence with sum less than `ε` -/
def posSumOfEncodable {ε : ℝ} (hε : 0 < ε) (ι) [Encodable ι] :
    { ε' : ι → ℝ // (∀ i, 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε } := by
  let f n := ε / 2 / 2 ^ n
  have hf : HasSum f ε := hasSum_geometric_two' _
  have f0 : ∀ n, 0 < f n := fun n ↦ div_pos (half_pos hε) (pow_pos zero_lt_two _)
  refine ⟨f ∘ Encodable.encode, fun i ↦ f0 _, ?_⟩
  rcases hf.summable.comp_injective (@Encodable.encode_injective ι _) with ⟨c, hg⟩
  refine ⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) ?_ ?_ hg hf⟩
  · intro i _
    exact le_of_lt (f0 _)
  · intro n
    exact le_rfl

Existence of positive summable sequence bounded by $\varepsilon$ on encodable types

Informal description

For any positive real number $\varepsilon > 0$ and any encodable type $\iota$, there exists a positive sequence $\varepsilon' \colon \iota \to \mathbb{R}$ such that $\varepsilon'(i) > 0$ for all $i \in \iota$, and the series $\sum_{i \in \iota} \varepsilon'(i)$ converges to some $c \leq \varepsilon$.

Set.Countable.exists_pos_hasSum_le theorem

 {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ} (hε : 0 < ε) :
  ∃ ε' : ι → ℝ, (∀ i, 0 < ε' i) ∧ ∃ c, HasSum (fun i : s ↦ ε' i) c ∧ c ≤ ε

Full source

theorem Set.Countable.exists_pos_hasSum_le {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ}
    (hε : 0 < ε) : ∃ ε' : ι → ℝ, (∀ i, 0 < ε' i) ∧ ∃ c, HasSum (fun i : s ↦ ε' i) c ∧ c ≤ ε := by
  classical
  haveI := hs.toEncodable
  rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
  refine ⟨fun i ↦ if h : i ∈ s then f ⟨i, h⟩ else 1, fun i ↦ ?_, ⟨c, ?_, hcε⟩⟩
  · conv_rhs => simp
    split_ifs
    exacts [hf0 _, zero_lt_one]
  · simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]

Existence of positive summable sequence on countable sets with sum bounded by $\varepsilon$

Informal description

For any countable set $s \subseteq \iota$ and any positive real number $\varepsilon > 0$, there exists a positive function $\varepsilon' \colon \iota \to \mathbb{R}$ such that $\varepsilon'(i) > 0$ for all $i \in \iota$, and the series $\sum_{i \in s} \varepsilon'(i)$ converges to some $c \leq \varepsilon$.

Set.Countable.exists_pos_forall_sum_le theorem

 {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ} (hε : 0 < ε) :
  ∃ ε' : ι → ℝ, (∀ i, 0 < ε' i) ∧ ∀ t : Finset ι, ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε

Full source

theorem Set.Countable.exists_pos_forall_sum_le {ι : Type*} {s : Set ι} (hs : s.Countable) {ε : ℝ}
    (hε : 0 < ε) : ∃ ε' : ι → ℝ,
    (∀ i, 0 < ε' i) ∧ ∀ t : Finset ι, ↑t ⊆ s → ∑ i ∈ t, ε' i ≤ ε := by
  classical
  rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
  refine ⟨ε', hpos, fun t ht ↦ ?_⟩
  rw [← sum_subtype_of_mem _ ht]
  refine (sum_le_hasSum _ ?_ hε'c).trans hcε
  exact fun _ _ ↦ (hpos _).le

Existence of Positive Function with Finite Sums Bounded by $\varepsilon$ on Countable Sets

Informal description

For any countable set $s \subseteq \iota$ and any positive real number $\varepsilon > 0$, there exists a positive function $\varepsilon' \colon \iota \to \mathbb{R}$ such that $\varepsilon'(i) > 0$ for all $i \in \iota$, and for any finite subset $t \subseteq s$, the sum $\sum_{i \in t} \varepsilon'(i)$ is bounded above by $\varepsilon$.

NNReal.exists_pos_sum_of_countable theorem

 {ε : ℝ≥0} (hε : ε ≠ 0) (ι) [Countable ι] : ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε

Full source

theorem exists_pos_sum_of_countable {ε : ℝ≥0} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε := by
  cases nonempty_encodable ι
  obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)
  obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι
  exact
    ⟨fun i ↦ ⟨ε' i, (hε' i).le⟩, fun i ↦ NNReal.coe_lt_coe.1 <| hε' i,
      ⟨c, hasSum_le (fun i ↦ (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
      aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩

Existence of Positive Summable Sequence Bounded by $\varepsilon$ on Countable Types in $\mathbb{R}_{\geq 0}$

Informal description

For any positive real number $\varepsilon > 0$ in $\mathbb{R}_{\geq 0}$ and any countable type $\iota$, there exists a positive sequence $\varepsilon' \colon \iota \to \mathbb{R}_{\geq 0}$ such that $\varepsilon'(i) > 0$ for all $i \in \iota$, and the series $\sum_{i \in \iota} \varepsilon'(i)$ converges to some $c < \varepsilon$.

ENNReal.exists_pos_sum_of_countable theorem

 {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] : ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ (∑' i, (ε' i : ℝ≥0∞)) < ε

Full source

theorem exists_pos_sum_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ (∑' i, (ε' i : ℝ≥0∞)) < ε := by
  rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩
  rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩
  rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩
  exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩

Existence of Positive Summable Sequence Bounded by $\varepsilon$ on Countable Types in Extended Non-Negative Reals

Informal description

For any nonzero extended non-negative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any countable type $\iota$, there exists a positive sequence $\varepsilon' \colon \iota \to \mathbb{R}_{\geq 0}$ such that $\varepsilon'(i) > 0$ for all $i \in \iota$, and the extended non-negative real-valued series $\sum_{i \in \iota} \varepsilon'(i)$ is less than $\varepsilon$.

ENNReal.exists_pos_sum_of_countable' theorem

 {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] : ∃ ε' : ι → ℝ≥0∞, (∀ i, 0 < ε' i) ∧ ∑' i, ε' i < ε

Full source

theorem exists_pos_sum_of_countable' {ε : ℝ≥0∞} (hε : ε ≠ 0) (ι) [Countable ι] :
    ∃ ε' : ι → ℝ≥0∞, (∀ i, 0 < ε' i) ∧ ∑' i, ε' i < ε :=
  let ⟨δ, δpos, hδ⟩ := exists_pos_sum_of_countable hε ι
  ⟨fun i ↦ δ i, fun i ↦ ENNReal.coe_pos.2 (δpos i), hδ⟩

Existence of Positive Summable Sequence Bounded by $\varepsilon$ on Countable Types in Extended Non-Negative Reals (Extended Version)

Informal description

For any nonzero extended non-negative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any countable type $\iota$, there exists a positive sequence $\varepsilon' \colon \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $\varepsilon'(i) > 0$ for all $i \in \iota$, and the extended non-negative real-valued series $\sum_{i \in \iota} \varepsilon'(i)$ is less than $\varepsilon$.

ENNReal.exists_pos_tsum_mul_lt_of_countable theorem

 {ε : ℝ≥0∞} (hε : ε ≠ 0) {ι} [Countable ι] (w : ι → ℝ≥0∞) (hw : ∀ i, w i ≠ ∞) :
  ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, (w i * δ i : ℝ≥0∞)) < ε

Full source

theorem exists_pos_tsum_mul_lt_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) {ι} [Countable ι] (w : ι → ℝ≥0∞)
    (hw : ∀ i, w i ≠ ∞) : ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, (w i * δ i : ℝ≥0∞)) < ε := by
  lift w to ι → ℝ≥0 using hw
  rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
  have : ∀ i, 0 < max 1 (w i) := fun i ↦ zero_lt_one.trans_le (le_max_left _ _)
  refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩
  refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum
  rw [coe_div (this i).ne']
  refine mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 ?_) _)
  exact coe_le_coe.2 (le_max_right _ _)

Existence of Positive Multiplicative Sequence with Summable Product Bounded by $\varepsilon$ in Extended Non-Negative Reals

Informal description

For any nonzero extended non-negative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, any countable type $\iota$, and any sequence $w \colon \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $w(i) \neq \infty$ for all $i \in \iota$, there exists a positive sequence $\delta \colon \iota \to \mathbb{R}_{\geq 0}$ with $\delta(i) > 0$ for all $i \in \iota$, such that the sum $\sum_{i \in \iota} (w(i) \cdot \delta(i))$ is less than $\varepsilon$.

factorial_tendsto_atTop theorem

: Tendsto Nat.factorial atTop atTop

Full source

theorem factorial_tendsto_atTop : Tendsto Nat.factorial atTop atTop :=
  tendsto_atTop_atTop_of_monotone (fun _ _ ↦ Nat.factorial_le) fun n ↦ ⟨n, n.self_le_factorial⟩

Factorial Tends to Infinity at Infinity

Informal description

The factorial function $n!$ tends to infinity as $n$ tends to infinity.

tendsto_factorial_div_pow_self_atTop theorem

: Tendsto (fun n ↦ n ! / (n : ℝ) ^ n : ℕ → ℝ) atTop (𝓝 0)

Full source

theorem tendsto_factorial_div_pow_self_atTop :
    Tendsto (fun n ↦ n ! / (n : ℝ) ^ n : ℕ → ℝ) atTop (𝓝 0) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (tendsto_const_div_atTop_nhds_zero_nat 1)
    (Eventually.of_forall fun n ↦
      div_nonneg (mod_cast n.factorial_pos.le)
        (pow_nonneg (mod_cast n.zero_le) _))
    (by
      refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_
      rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
      rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
        Finset.prod_range_succ']
      simp only [prod_range_succ', one_mul, Nat.cast_add, zero_add, Nat.cast_one]
      refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;>
          intro x hx <;>
        rw [Finset.mem_range] at hx
      · positivity
      · refine (div_le_one <| mod_cast hn).mpr ?_
        norm_cast
        omega)

Limit of Factorial Over Power: $\lim_{n \to \infty} \frac{n!}{n^n} = 0$

Informal description

The sequence defined by $a_n = \frac{n!}{n^n}$ for natural numbers $n$ converges to $0$ as $n$ tends to infinity, i.e., $\lim_{n \to \infty} \frac{n!}{n^n} = 0$.

tendsto_nat_floor_atTop theorem

 {α : Type*} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
  Tendsto (fun x : α ↦ ⌊x⌋₊) atTop atTop

Full source

theorem tendsto_nat_floor_atTop {α : Type*}
    [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
    Tendsto (fun x : α ↦ ⌊x⌋₊) atTop atTop :=
  Nat.floor_mono.tendsto_atTop_atTop fun x ↦ ⟨max 0 (x + 1), by simp [Nat.le_floor_iff]⟩

Floor Function Tends to Infinity at Infinity

Informal description

For any ordered semiring $\alpha$ with a strictly ordered ring structure and a floor function, the sequence of floor functions $\lfloor x \rfloor$ tends to infinity as $x$ tends to infinity. In other words, the function $\lfloor \cdot \rfloor : \alpha \to \mathbb{N}$ satisfies $\lim_{x \to \infty} \lfloor x \rfloor = \infty$.

tendsto_nat_ceil_atTop theorem

 {α : Type*} [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
  Tendsto (fun x : α ↦ ⌈x⌉₊) atTop atTop

Full source

lemma tendsto_nat_ceil_atTop {α : Type*}
    [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] :
    Tendsto (fun x : α ↦ ⌈x⌉₊) atTop atTop := by
  refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)
  simp only [Nat.ceil_natCast, le_refl]

Ceiling Function Tends to Infinity at Infinity

Informal description

For any ordered semiring $\alpha$ with a strictly ordered ring structure and a floor function, the sequence of ceiling functions $\lceil x \rceil$ tends to infinity as $x$ tends to infinity. In other words, the function $\lceil \cdot \rceil : \alpha \to \mathbb{N}$ satisfies $\lim_{x \to \infty} \lceil x \rceil = \infty$.

tendsto_nat_floor_mul_atTop theorem

 {α : Type _} [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α] [Archimedean α] (a : α)
  (ha : 0 < a) : Tendsto (fun (x : ℕ) => ⌊a * x⌋₊) atTop atTop

Full source

lemma tendsto_nat_floor_mul_atTop {α : Type _}
    [Semifield α] [LinearOrder α] [IsStrictOrderedRing α] [FloorSemiring α]
    [Archimedean α] (a : α) (ha : 0 < a) : Tendsto (fun (x : ℕ) => ⌊a * x⌋₊) atTop atTop :=
  Tendsto.comp tendsto_nat_floor_atTop
    <| Tendsto.const_mul_atTop ha tendsto_natCast_atTop_atTop

Floor of Scaled Natural Numbers Tends to Infinity at Infinity

Informal description

Let $\alpha$ be a semifield with a linear order and a strictly ordered ring structure, equipped with a floor function and satisfying the Archimedean property. For any positive element $a \in \alpha$ (i.e., $0 < a$), the sequence defined by $x \mapsto \lfloor a \cdot x \rfloor$ tends to infinity as $x$ tends to infinity. In other words, $\lim_{x \to \infty} \lfloor a \cdot x \rfloor = \infty$.

tendsto_nat_floor_mul_div_atTop theorem

{a : R} (ha : 0 ≤ a) : Tendsto (fun x ↦ (⌊a * x⌋₊ : R) / x) atTop (𝓝 a)

Full source

theorem tendsto_nat_floor_mul_div_atTop {a : R} (ha : 0 ≤ a) :
    Tendsto (fun x ↦ (⌊a * x⌋₊ : R) / x) atTop (𝓝 a) := by
  have A : Tendsto (fun x : R ↦ a - x⁻¹) atTop (𝓝 (a - 0)) :=
    tendsto_const_nhds.sub tendsto_inv_atTop_zero
  rw [sub_zero] at A
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds
  · refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul,
      inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']
    have := Nat.lt_floor_add_one (a * x)
    linarith
  · refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    rw [div_le_iff₀ (zero_lt_one.trans_le hx)]
    simp [Nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))]

Limit of Scaled Floor Function Ratio: $\lim_{x \to \infty} \frac{\lfloor a x \rfloor}{x} = a$ for $a \geq 0$

Informal description

For any real number $a \geq 0$, the sequence defined by $x \mapsto \frac{\lfloor a x \rfloor}{x}$ converges to $a$ as $x$ tends to infinity, i.e., \[ \lim_{x \to \infty} \frac{\lfloor a x \rfloor}{x} = a. \]

tendsto_nat_floor_div_atTop theorem

: Tendsto (fun x ↦ (⌊x⌋₊ : R) / x) atTop (𝓝 1)

Full source

theorem tendsto_nat_floor_div_atTop : Tendsto (fun x ↦ (⌊x⌋₊ : R) / x) atTop (𝓝 1) := by
  simpa using tendsto_nat_floor_mul_div_atTop (zero_le_one' R)

Limit of Floor Function Ratio: $\lim_{x \to \infty} \frac{\lfloor x \rfloor}{x} = 1$

Informal description

The sequence defined by $x \mapsto \frac{\lfloor x \rfloor}{x}$ converges to $1$ as $x$ tends to infinity, i.e., \[ \lim_{x \to \infty} \frac{\lfloor x \rfloor}{x} = 1. \]

tendsto_nat_ceil_mul_div_atTop theorem

{a : R} (ha : 0 ≤ a) : Tendsto (fun x ↦ (⌈a * x⌉₊ : R) / x) atTop (𝓝 a)

Full source

theorem tendsto_nat_ceil_mul_div_atTop {a : R} (ha : 0 ≤ a) :
    Tendsto (fun x ↦ (⌈a * x⌉₊ : R) / x) atTop (𝓝 a) := by
  have A : Tendsto (fun x : R ↦ a + x⁻¹) atTop (𝓝 (a + 0)) :=
    tendsto_const_nhds.add tendsto_inv_atTop_zero
  rw [add_zero] at A
  apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A
  · refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    rw [le_div_iff₀ (zero_lt_one.trans_le hx)]
    exact Nat.le_ceil _
  · refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩
    simp [div_le_iff₀ (zero_lt_one.trans_le hx), inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne',
      (Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]

Limit of Ceiling Function: $\lim_{x \to \infty} \frac{\lceil a x \rceil}{x} = a$ for $a \geq 0$

Informal description

For any nonnegative real number $a \geq 0$, the sequence of functions defined by $x \mapsto \frac{\lceil a x \rceil}{x}$ converges to $a$ as $x$ tends to infinity, i.e., \[ \lim_{x \to \infty} \frac{\lceil a x \rceil}{x} = a. \]

tendsto_nat_ceil_div_atTop theorem

: Tendsto (fun x ↦ (⌈x⌉₊ : R) / x) atTop (𝓝 1)

Full source

theorem tendsto_nat_ceil_div_atTop : Tendsto (fun x ↦ (⌈x⌉₊ : R) / x) atTop (𝓝 1) := by
  simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)

Limit of Ceiling Function: $\lim_{x \to \infty} \frac{\lceil x \rceil}{x} = 1$

Informal description

The sequence of functions defined by $x \mapsto \frac{\lceil x \rceil}{x}$ converges to $1$ as $x$ tends to infinity, i.e., \[ \lim_{x \to \infty} \frac{\lceil x \rceil}{x} = 1. \]

Nat.tendsto_div_const_atTop theorem

{n : ℕ} (hn : n ≠ 0) : Tendsto (· / n) atTop atTop

Full source

lemma Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (· / n) atTop atTop := by
  rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]

Divergence of Division by Nonzero Natural Number: $\lim_{x \to \infty} \frac{x}{n} = \infty$ for $n \neq 0$

Informal description

For any nonzero natural number $n$, the function $x \mapsto x / n$ tends to infinity as $x$ tends to infinity, i.e., $\lim_{x \to \infty} \frac{x}{n} = \infty$.