Documentation

Mathlib.Analysis.SpecificLimits.Normed

A collection of specific limit computations #

This file contains important specific limit computations in (semi-)normed groups/rings/spaces, as well as such computations in when the natural proof passes through a fact about normed spaces.

theorem tendsto_norm_atTop_atTop :
Filter.Tendsto norm Filter.atTop Filter.atTop
theorem summable_of_absolute_convergence_real {f : } :
(∃ (r : ), Filter.Tendsto (fun (n : ) => iFinset.range n, |f i|) Filter.atTop (nhds r))Summable f

Powers #

theorem NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop {𝕜 : Type u_4} [NormedDivisionRing 𝕜] {m : } (hm : m < 0) :
Filter.Tendsto (fun (x : 𝕜) => x ^ m) (nhdsWithin 0 {0}) Filter.atTop
theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded {ι : Type u_4} {𝕜 : Type u_5} {𝔸 : Type u_6} [NormedDivisionRing 𝕜] [NormedAddCommGroup 𝔸] [Module 𝕜 𝔸] [BoundedSMul 𝕜 𝔸] {l : Filter ι} {ε : ι𝕜} {f : ι𝔸} (hε : Filter.Tendsto ε l (nhds 0)) (hf : Filter.IsBoundedUnder (fun (x1 x2 : ) => x1 x2) l (norm f)) :
Filter.Tendsto (ε f) l (nhds 0)

The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero.

@[simp]
theorem NormedField.continuousAt_zpow {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {m : } {x : 𝕜} :
ContinuousAt (fun (x : 𝕜) => x ^ m) x x 0 0 m
@[simp]
theorem NormedField.continuousAt_inv {𝕜 : Type u_4} [NontriviallyNormedField 𝕜] {x : 𝕜} :
ContinuousAt Inv.inv x x 0
theorem isLittleO_pow_pow_of_lt_left {r₁ : } {r₂ : } (h₁ : 0 r₁) (h₂ : r₁ < r₂) :
(fun (n : ) => r₁ ^ n) =o[Filter.atTop] fun (n : ) => r₂ ^ n
theorem isBigO_pow_pow_of_le_left {r₁ : } {r₂ : } (h₁ : 0 r₁) (h₂ : r₁ r₂) :
(fun (n : ) => r₁ ^ n) =O[Filter.atTop] fun (n : ) => r₂ ^ n
theorem isLittleO_pow_pow_of_abs_lt_left {r₁ : } {r₂ : } (h : |r₁| < |r₂|) :
(fun (n : ) => r₁ ^ n) =o[Filter.atTop] fun (n : ) => r₂ ^ n
theorem TFAE_exists_lt_isLittleO_pow (f : ) (R : ) :
[aSet.Ioo (-R) R, f =o[Filter.atTop] fun (x : ) => a ^ x, aSet.Ioo 0 R, f =o[Filter.atTop] fun (x : ) => a ^ x, aSet.Ioo (-R) R, f =O[Filter.atTop] fun (x : ) => a ^ x, aSet.Ioo 0 R, f =O[Filter.atTop] fun (x : ) => a ^ x, a < R, ∃ (C : ), (0 < C 0 < R) ∀ (n : ), |f n| C * a ^ n, aSet.Ioo 0 R, C > 0, ∀ (n : ), |f n| C * a ^ n, a < R, ∀ᶠ (n : ) in Filter.atTop, |f n| a ^ n, aSet.Ioo 0 R, ∀ᶠ (n : ) in Filter.atTop, |f n| a ^ n].TFAE

Various statements equivalent to the fact that f n grows exponentially slower than R ^ n.

  • 0: $f n = o(a ^ n)$ for some $-R < a < R$;
  • 1: $f n = o(a ^ n)$ for some $0 < a < R$;
  • 2: $f n = O(a ^ n)$ for some $-R < a < R$;
  • 3: $f n = O(a ^ n)$ for some $0 < a < R$;
  • 4: there exist a < R and C such that one of C and R is positive and $|f n| ≤ Ca^n$ for all n;
  • 5: there exists 0 < a < R and a positive C such that $|f n| ≤ Ca^n$ for all n;
  • 6: there exists a < R such that $|f n| ≤ a ^ n$ for sufficiently large n;
  • 7: there exists 0 < a < R such that $|f n| ≤ a ^ n$ for sufficiently large n.

NB: For backwards compatibility, if you add more items to the list, please append them at the end of the list.

theorem isLittleO_pow_const_const_pow_of_one_lt {R : Type u_4} [NormedRing R] (k : ) {r : } (hr : 1 < r) :
(fun (n : ) => n ^ k) =o[Filter.atTop] fun (n : ) => r ^ n

For any natural k and a real r > 1 we have n ^ k = o(r ^ n) as n → ∞.

theorem isLittleO_coe_const_pow_of_one_lt {R : Type u_4} [NormedRing R] {r : } (hr : 1 < r) :
Nat.cast =o[Filter.atTop] fun (n : ) => r ^ n

For a real r > 1 we have n = o(r ^ n) as n → ∞.

theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type u_4} [NormedRing R] (k : ) {r₁ : R} {r₂ : } (h : r₁ < r₂) :
(fun (n : ) => n ^ k * r₁ ^ n) =o[Filter.atTop] fun (n : ) => r₂ ^ n

If ‖r₁‖ < r₂, then for any natural k we have n ^ k r₁ ^ n = o (r₂ ^ n) as n → ∞.

theorem tendsto_pow_const_div_const_pow_of_one_lt (k : ) {r : } (hr : 1 < r) :
Filter.Tendsto (fun (n : ) => n ^ k / r ^ n) Filter.atTop (nhds 0)
theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ) {r : } (hr : |r| < 1) :
Filter.Tendsto (fun (n : ) => n ^ k * r ^ n) Filter.atTop (nhds 0)

If |r| < 1, then n ^ k r ^ n tends to zero for any natural k.

theorem tendsto_pow_const_mul_const_pow_of_lt_one (k : ) {r : } (hr : 0 r) (h'r : r < 1) :
Filter.Tendsto (fun (n : ) => n ^ k * r ^ n) Filter.atTop (nhds 0)

If 0 ≤ r < 1, then n ^ k r ^ n tends to zero for any natural k. This is a specialized version of tendsto_pow_const_mul_const_pow_of_abs_lt_one, singled out for ease of application.

theorem tendsto_self_mul_const_pow_of_abs_lt_one {r : } (hr : |r| < 1) :
Filter.Tendsto (fun (n : ) => n * r ^ n) Filter.atTop (nhds 0)

If |r| < 1, then n * r ^ n tends to zero.

theorem tendsto_self_mul_const_pow_of_lt_one {r : } (hr : 0 r) (h'r : r < 1) :
Filter.Tendsto (fun (n : ) => n * r ^ n) Filter.atTop (nhds 0)

If 0 ≤ r < 1, then n * r ^ n tends to zero. This is a specialized version of tendsto_self_mul_const_pow_of_abs_lt_one, singled out for ease of application.

theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one {R : Type u_4} [NormedRing R] {x : R} (h : x < 1) :
Filter.Tendsto (fun (n : ) => x ^ n) Filter.atTop (nhds 0)

In a normed ring, the powers of an element x with ‖x‖ < 1 tend to zero.

@[deprecated tendsto_pow_atTop_nhds_zero_of_norm_lt_one]
theorem tendsto_pow_atTop_nhds_0_of_norm_lt_1 {R : Type u_4} [NormedRing R] {x : R} (h : x < 1) :
Filter.Tendsto (fun (n : ) => x ^ n) Filter.atTop (nhds 0)

Alias of tendsto_pow_atTop_nhds_zero_of_norm_lt_one.


In a normed ring, the powers of an element x with ‖x‖ < 1 tend to zero.

theorem tendsto_pow_atTop_nhds_zero_of_abs_lt_one {r : } (h : |r| < 1) :
Filter.Tendsto (fun (n : ) => r ^ n) Filter.atTop (nhds 0)
@[deprecated tendsto_pow_atTop_nhds_zero_of_abs_lt_one]
theorem tendsto_pow_atTop_nhds_0_of_abs_lt_1 {r : } (h : |r| < 1) :
Filter.Tendsto (fun (n : ) => r ^ n) Filter.atTop (nhds 0)

Alias of tendsto_pow_atTop_nhds_zero_of_abs_lt_one.

Geometric series #

A normed ring has summable geometric series if, for all ξ of norm < 1, the geometric series ∑ ξ ^ n converges. This holds both in complete normed rings and in normed fields, providing a convenient abstraction of these two classes to avoid repeating the same proofs.

  • summable_geometric_of_norm_lt_one : ∀ (ξ : K), ξ < 1Summable fun (n : ) => ξ ^ n
Instances
    theorem HasSummableGeomSeries.summable_geometric_of_norm_lt_one {K : Type u_4} :
    ∀ {inst : NormedRing K} [self : HasSummableGeomSeries K] (ξ : K), ξ < 1Summable fun (n : ) => ξ ^ n
    theorem summable_geometric_of_norm_lt_one {K : Type u_4} [NormedRing K] [HasSummableGeomSeries K] {x : K} (h : x < 1) :
    Summable fun (n : ) => x ^ n
    theorem tsum_geometric_le_of_norm_lt_one {R : Type u_4} [NormedRing R] (x : R) (h : x < 1) :
    ∑' (n : ), x ^ n 1 - 1 + (1 - x)⁻¹

    Bound for the sum of a geometric series in a normed ring. This formula does not assume that the normed ring satisfies the axiom ‖1‖ = 1.

    @[deprecated tsum_geometric_le_of_norm_lt_one]
    theorem NormedRing.tsum_geometric_of_norm_lt_1 {R : Type u_4} [NormedRing R] (x : R) (h : x < 1) :
    ∑' (n : ), x ^ n 1 - 1 + (1 - x)⁻¹

    Alias of tsum_geometric_le_of_norm_lt_one.


    Bound for the sum of a geometric series in a normed ring. This formula does not assume that the normed ring satisfies the axiom ‖1‖ = 1.

    @[deprecated tsum_geometric_le_of_norm_lt_one]
    theorem NormedRing.tsum_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] (x : R) (h : x < 1) :
    ∑' (n : ), x ^ n 1 - 1 + (1 - x)⁻¹

    Alias of tsum_geometric_le_of_norm_lt_one.


    Bound for the sum of a geometric series in a normed ring. This formula does not assume that the normed ring satisfies the axiom ‖1‖ = 1.

    theorem geom_series_mul_neg {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
    (∑' (i : ), x ^ i) * (1 - x) = 1
    theorem mul_neg_geom_series {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
    (1 - x) * ∑' (i : ), x ^ i = 1
    theorem geom_series_succ {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
    ∑' (i : ), x ^ (i + 1) = ∑' (i : ), x ^ i - 1
    theorem geom_series_mul_shift {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
    x * ∑' (i : ), x ^ i = ∑' (i : ), x ^ (i + 1)
    theorem geom_series_mul_one_add {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
    (1 + x) * ∑' (i : ), x ^ i = 2 * ∑' (i : ), x ^ i - 1
    @[simp]
    theorem Units.val_oneSub {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (t : R) (h : t < 1) :
    (Units.oneSub t h) = 1 - t
    def Units.oneSub {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (t : R) (h : t < 1) :

    In a normed ring with summable geometric series, a perturbation of 1 by an element t of distance less than 1 from 1 is a unit. Here we construct its Units structure.

    Equations
    • Units.oneSub t h = { val := 1 - t, inv := ∑' (n : ), t ^ n, val_inv := , inv_val := }
    Instances For
      theorem geom_series_eq_inverse {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
      ∑' (i : ), x ^ i = Ring.inverse (1 - x)
      theorem hasSum_geom_series_inverse {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (x : R) (h : x < 1) :
      HasSum (fun (i : ) => x ^ i) (Ring.inverse (1 - x))
      theorem isUnit_one_sub_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {x : R} (h : x < 1) :
      IsUnit (1 - x)
      @[deprecated summable_geometric_of_norm_lt_one]
      theorem NormedRing.summable_geometric_of_norm_lt_1 {K : Type u_4} [NormedRing K] [HasSummableGeomSeries K] {x : K} (h : x < 1) :
      Summable fun (n : ) => x ^ n

      Alias of summable_geometric_of_norm_lt_one.

      @[deprecated summable_geometric_of_norm_lt_one]
      theorem NormedRing.summable_geometric_of_norm_lt_one {K : Type u_4} [NormedRing K] [HasSummableGeomSeries K] {x : K} (h : x < 1) :
      Summable fun (n : ) => x ^ n

      Alias of summable_geometric_of_norm_lt_one.

      theorem hasSum_geometric_of_norm_lt_one {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ξ < 1) :
      HasSum (fun (n : ) => ξ ^ n) (1 - ξ)⁻¹
      @[deprecated hasSum_geometric_of_norm_lt_one]
      theorem hasSum_geometric_of_norm_lt_1 {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ξ < 1) :
      HasSum (fun (n : ) => ξ ^ n) (1 - ξ)⁻¹

      Alias of hasSum_geometric_of_norm_lt_one.

      @[deprecated summable_geometric_of_norm_lt_one]
      theorem summable_geometric_of_norm_lt_1 {K : Type u_4} [NormedRing K] [HasSummableGeomSeries K] {x : K} (h : x < 1) :
      Summable fun (n : ) => x ^ n

      Alias of summable_geometric_of_norm_lt_one.

      theorem tsum_geometric_of_norm_lt_one {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ξ < 1) :
      ∑' (n : ), ξ ^ n = (1 - ξ)⁻¹
      @[deprecated tsum_geometric_of_norm_lt_one]
      theorem tsum_geometric_of_norm_lt_1 {K : Type u_4} [NormedDivisionRing K] {ξ : K} (h : ξ < 1) :
      ∑' (n : ), ξ ^ n = (1 - ξ)⁻¹

      Alias of tsum_geometric_of_norm_lt_one.

      theorem hasSum_geometric_of_abs_lt_one {r : } (h : |r| < 1) :
      HasSum (fun (n : ) => r ^ n) (1 - r)⁻¹
      @[deprecated hasSum_geometric_of_abs_lt_one]
      theorem hasSum_geometric_of_abs_lt_1 {r : } (h : |r| < 1) :
      HasSum (fun (n : ) => r ^ n) (1 - r)⁻¹

      Alias of hasSum_geometric_of_abs_lt_one.

      theorem summable_geometric_of_abs_lt_one {r : } (h : |r| < 1) :
      Summable fun (n : ) => r ^ n
      @[deprecated summable_geometric_of_abs_lt_one]
      theorem summable_geometric_of_abs_lt_1 {r : } (h : |r| < 1) :
      Summable fun (n : ) => r ^ n

      Alias of summable_geometric_of_abs_lt_one.

      theorem tsum_geometric_of_abs_lt_one {r : } (h : |r| < 1) :
      ∑' (n : ), r ^ n = (1 - r)⁻¹
      @[deprecated tsum_geometric_of_abs_lt_one]
      theorem tsum_geometric_of_abs_lt_1 {r : } (h : |r| < 1) :
      ∑' (n : ), r ^ n = (1 - r)⁻¹

      Alias of tsum_geometric_of_abs_lt_one.

      @[simp]
      theorem summable_geometric_iff_norm_lt_one {K : Type u_4} [NormedDivisionRing K] {ξ : K} :
      (Summable fun (n : ) => ξ ^ n) ξ < 1

      A geometric series in a normed field is summable iff the norm of the common ratio is less than one.

      @[deprecated summable_geometric_iff_norm_lt_one]
      theorem summable_geometric_iff_norm_lt_1 {K : Type u_4} [NormedDivisionRing K] {ξ : K} :
      (Summable fun (n : ) => ξ ^ n) ξ < 1

      Alias of summable_geometric_iff_norm_lt_one.


      A geometric series in a normed field is summable iff the norm of the common ratio is less than one.

      theorem summable_norm_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] {k : } {r : R} (hr : r < 1) {u : } (hu : (fun (n : ) => (u n)) =O[Filter.atTop] fun (n : ) => (n ^ k)) :
      Summable fun (n : ) => (u n) * r ^ n
      theorem summable_norm_pow_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] (k : ) {r : R} (hr : r < 1) :
      Summable fun (n : ) => n ^ k * r ^ n
      theorem summable_norm_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] {r : R} (hr : r < 1) :
      Summable fun (n : ) => r ^ n
      theorem hasSum_choose_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ) {r : R} (hr : r < 1) :
      HasSum (fun (n : ) => ((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
      theorem summable_choose_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ) {r : R} (hr : r < 1) :
      Summable fun (n : ) => ((n + k).choose k) * r ^ n
      theorem tsum_choose_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ) {r : R} (hr : r < 1) :
      ∑' (n : ), ((n + k).choose k) * r ^ n = Ring.inverse (1 - r) ^ (k + 1)
      theorem hasSum_choose_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ) {r : 𝕜} (hr : r < 1) :
      HasSum (fun (n : ) => ((n + k).choose k) * r ^ n) (1 / (1 - r) ^ (k + 1))
      theorem tsum_choose_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] (k : ) {r : 𝕜} (hr : r < 1) :
      ∑' (n : ), ((n + k).choose k) * r ^ n = 1 / (1 - r) ^ (k + 1)
      theorem summable_descFactorial_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ) {r : R} (hr : r < 1) :
      Summable fun (n : ) => ((n + k).descFactorial k) * r ^ n
      theorem summable_pow_mul_geometric_of_norm_lt_one {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ) {r : R} (hr : r < 1) :
      Summable fun (n : ) => n ^ k * r ^ n
      @[deprecated summable_norm_pow_mul_geometric_of_norm_lt_one]
      theorem summable_norm_pow_mul_geometric_of_norm_lt_1 {R : Type u_4} [NormedRing R] (k : ) {r : R} (hr : r < 1) :
      Summable fun (n : ) => n ^ k * r ^ n

      Alias of summable_norm_pow_mul_geometric_of_norm_lt_one.

      @[deprecated summable_pow_mul_geometric_of_norm_lt_one]
      theorem summable_pow_mul_geometric_of_norm_lt_1 {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] (k : ) {r : R} (hr : r < 1) :
      Summable fun (n : ) => n ^ k * r ^ n

      Alias of summable_pow_mul_geometric_of_norm_lt_one.

      theorem hasSum_coe_mul_geometric_of_norm_lt_one' {R : Type u_4} [NormedRing R] [HasSummableGeomSeries R] {x : R} (h : x < 1) :
      HasSum (fun (n : ) => n * x ^ n) (x * Ring.inverse (1 - x) ^ 2)

      If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, HasSum version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see hasSum_coe_mul_geometric_of_norm_lt_one.

      theorem tsum_coe_mul_geometric_of_norm_lt_one' {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : r < 1) :
      ∑' (n : ), n * r ^ n = r * Ring.inverse (1 - r) ^ 2

      If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, version in a general ring with summable geometric series. For a version in a field, using division instead of Ring.inverse, see tsum_coe_mul_geometric_of_norm_lt_one.

      theorem hasSum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : r < 1) :
      HasSum (fun (n : ) => n * r ^ n) (r / (1 - r) ^ 2)

      If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, HasSum version.

      @[deprecated hasSum_coe_mul_geometric_of_norm_lt_one]
      theorem hasSum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : r < 1) :
      HasSum (fun (n : ) => n * r ^ n) (r / (1 - r) ^ 2)

      Alias of hasSum_coe_mul_geometric_of_norm_lt_one.


      If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2, HasSum version.

      theorem tsum_coe_mul_geometric_of_norm_lt_one {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : r < 1) :
      ∑' (n : ), n * r ^ n = r / (1 - r) ^ 2

      If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2.

      @[deprecated tsum_coe_mul_geometric_of_norm_lt_one]
      theorem tsum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type u_5} [NormedDivisionRing 𝕜] {r : 𝕜} (hr : r < 1) :
      ∑' (n : ), n * r ^ n = r / (1 - r) ^ 2

      Alias of tsum_coe_mul_geometric_of_norm_lt_one.


      If ‖r‖ < 1, then ∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2.

      theorem SeminormedAddCommGroup.cauchySeq_of_le_geometric {α : Type u_1} [SeminormedAddCommGroup α] {C : } {r : } (hr : r < 1) {u : α} (h : ∀ (n : ), u n - u (n + 1) C * r ^ n) :
      theorem dist_partial_sum_le_of_le_geometric {α : Type u_1} [SeminormedAddCommGroup α] {r : } {C : } {f : α} (hf : ∀ (n : ), f n C * r ^ n) (n : ) :
      dist (∑ iFinset.range n, f i) (∑ iFinset.range (n + 1), f i) C * r ^ n
      theorem cauchySeq_finset_of_geometric_bound {α : Type u_1} [SeminormedAddCommGroup α] {r : } {C : } {f : α} (hr : r < 1) (hf : ∀ (n : ), f n C * r ^ n) :
      CauchySeq fun (s : Finset ) => xs, f x

      If ‖f n‖ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f form a Cauchy sequence. This lemma does not assume 0 ≤ r or 0 ≤ C.

      theorem norm_sub_le_of_geometric_bound_of_hasSum {α : Type u_1} [SeminormedAddCommGroup α] {r : } {C : } {f : α} (hr : r < 1) (hf : ∀ (n : ), f n C * r ^ n) {a : α} (ha : HasSum f a) (n : ) :
      xFinset.range n, f x - a C * r ^ n / (1 - r)

      If ‖f n‖ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f are within distance C * r ^ n / (1 - r) of the sum of the series. This lemma does not assume 0 ≤ r or 0 ≤ C.

      @[simp]
      theorem dist_partial_sum {α : Type u_1} [SeminormedAddCommGroup α] (u : α) (n : ) :
      dist (∑ kFinset.range (n + 1), u k) (∑ kFinset.range n, u k) = u n
      @[simp]
      theorem dist_partial_sum' {α : Type u_1} [SeminormedAddCommGroup α] (u : α) (n : ) :
      dist (∑ kFinset.range n, u k) (∑ kFinset.range (n + 1), u k) = u n
      theorem cauchy_series_of_le_geometric {α : Type u_1} [SeminormedAddCommGroup α] {C : } {u : α} {r : } (hr : r < 1) (h : ∀ (n : ), u n C * r ^ n) :
      CauchySeq fun (n : ) => kFinset.range n, u k
      theorem NormedAddCommGroup.cauchy_series_of_le_geometric' {α : Type u_1} [SeminormedAddCommGroup α] {C : } {u : α} {r : } (hr : r < 1) (h : ∀ (n : ), u n C * r ^ n) :
      CauchySeq fun (n : ) => kFinset.range (n + 1), u k
      theorem NormedAddCommGroup.cauchy_series_of_le_geometric'' {α : Type u_1} [SeminormedAddCommGroup α] {C : } {u : α} {N : } {r : } (hr₀ : 0 < r) (hr₁ : r < 1) (h : nN, u n C * r ^ n) :
      CauchySeq fun (n : ) => kFinset.range (n + 1), u k
      theorem exists_norm_le_of_cauchySeq {α : Type u_1} [SeminormedAddCommGroup α] {f : α} (h : CauchySeq fun (n : ) => kFinset.range n, f k) :
      ∃ (C : ), ∀ (n : ), f n C

      The term norms of any convergent series are bounded by a constant.

      Summability tests based on comparison with geometric series #

      theorem summable_of_ratio_norm_eventually_le {α : Type u_4} [SeminormedAddCommGroup α] [CompleteSpace α] {f : α} {r : } (hr₁ : r < 1) (h : ∀ᶠ (n : ) in Filter.atTop, f (n + 1) r * f n) :
      theorem summable_of_ratio_test_tendsto_lt_one {α : Type u_4} [NormedAddCommGroup α] [CompleteSpace α] {f : α} {l : } (hl₁ : l < 1) (hf : ∀ᶠ (n : ) in Filter.atTop, f n 0) (h : Filter.Tendsto (fun (n : ) => f (n + 1) / f n) Filter.atTop (nhds l)) :
      theorem not_summable_of_ratio_norm_eventually_ge {α : Type u_4} [SeminormedAddCommGroup α] {f : α} {r : } (hr : 1 < r) (hf : ∃ᶠ (n : ) in Filter.atTop, f n 0) (h : ∀ᶠ (n : ) in Filter.atTop, r * f n f (n + 1)) :
      theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type u_4} [SeminormedAddCommGroup α] {f : α} {l : } (hl : 1 < l) (h : Filter.Tendsto (fun (n : ) => f (n + 1) / f n) Filter.atTop (nhds l)) :
      theorem summable_powerSeries_of_norm_lt {α : Type u_1} [NormedDivisionRing α] [CompleteSpace α] {f : α} {w : α} {z : α} (h : CauchySeq fun (n : ) => iFinset.range n, f i * w ^ i) (hz : z < w) :
      Summable fun (n : ) => f n * z ^ n

      If a power series converges at w, it converges absolutely at all z of smaller norm.

      theorem summable_powerSeries_of_norm_lt_one {α : Type u_1} [NormedDivisionRing α] [CompleteSpace α] {f : α} {z : α} (h : CauchySeq fun (n : ) => iFinset.range n, f i) (hz : z < 1) :
      Summable fun (n : ) => f n * z ^ n

      If a power series converges at 1, it converges absolutely at all z of smaller norm.

      Dirichlet and alternating series tests #

      theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {b : } {f : } {z : E} (hfa : Monotone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) (hgb : ∀ (n : ), iFinset.range n, z i b) :
      CauchySeq fun (n : ) => iFinset.range n, f i z i

      Dirichlet's test for monotone sequences.

      theorem Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded {E : Type u_4} [NormedAddCommGroup E] [NormedSpace E] {b : } {f : } {z : E} (hfa : Antitone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) (hzb : ∀ (n : ), iFinset.range n, z i b) :
      CauchySeq fun (n : ) => iFinset.range n, f i z i

      Dirichlet's test for antitone sequences.

      theorem norm_sum_neg_one_pow_le (n : ) :
      iFinset.range n, (-1) ^ i 1
      theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero {f : } (hfa : Monotone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) :
      CauchySeq fun (n : ) => iFinset.range n, (-1) ^ i * f i

      The alternating series test for monotone sequences. See also Monotone.tendsto_alternating_series_of_tendsto_zero.

      theorem Monotone.tendsto_alternating_series_of_tendsto_zero {f : } (hfa : Monotone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) :
      ∃ (l : ), Filter.Tendsto (fun (n : ) => iFinset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)

      The alternating series test for monotone sequences.

      theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero {f : } (hfa : Antitone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) :
      CauchySeq fun (n : ) => iFinset.range n, (-1) ^ i * f i

      The alternating series test for antitone sequences. See also Antitone.tendsto_alternating_series_of_tendsto_zero.

      theorem Antitone.tendsto_alternating_series_of_tendsto_zero {f : } (hfa : Antitone f) (hf0 : Filter.Tendsto f Filter.atTop (nhds 0)) :
      ∃ (l : ), Filter.Tendsto (fun (n : ) => iFinset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)

      The alternating series test for antitone sequences.

      Partial sum bounds on alternating convergent series #

      theorem Monotone.tendsto_le_alternating_series {E : Type u_4} [OrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : E} (hfl : Filter.Tendsto (fun (n : ) => iFinset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfm : Monotone f) (k : ) :
      l iFinset.range (2 * k), (-1) ^ i * f i

      Partial sums of an alternating monotone series with an even number of terms provide upper bounds on the limit.

      theorem Monotone.alternating_series_le_tendsto {E : Type u_4} [OrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : E} (hfl : Filter.Tendsto (fun (n : ) => iFinset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfm : Monotone f) (k : ) :
      iFinset.range (2 * k + 1), (-1) ^ i * f i l

      Partial sums of an alternating monotone series with an odd number of terms provide lower bounds on the limit.

      theorem Antitone.alternating_series_le_tendsto {E : Type u_4} [OrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : E} (hfl : Filter.Tendsto (fun (n : ) => iFinset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfa : Antitone f) (k : ) :
      iFinset.range (2 * k), (-1) ^ i * f i l

      Partial sums of an alternating antitone series with an even number of terms provide lower bounds on the limit.

      theorem Antitone.tendsto_le_alternating_series {E : Type u_4} [OrderedRing E] [TopologicalSpace E] [OrderClosedTopology E] {l : E} {f : E} (hfl : Filter.Tendsto (fun (n : ) => iFinset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)) (hfa : Antitone f) (k : ) :
      l iFinset.range (2 * k + 1), (-1) ^ i * f i

      Partial sums of an alternating antitone series with an odd number of terms provide upper bounds on the limit.

      Factorial #

      theorem Real.summable_pow_div_factorial (x : ) :
      Summable fun (n : ) => x ^ n / n.factorial

      The series ∑' n, x ^ n / n! is summable of any x : ℝ. See also expSeries_div_summable for a version that also works in , and NormedSpace.expSeries_summable' for a version that works in any normed algebra over or .

      theorem Real.tendsto_pow_div_factorial_atTop (x : ) :
      Filter.Tendsto (fun (n : ) => x ^ n / n.factorial) Filter.atTop (nhds 0)