Convergence of sequences and series

Convergence tests (root test, rearrangement theorem, Stolz–Cesàro), normal and uniform convergence of series of functions, and specific limits of sequences and partial sums.

TheoremConvergence of an alternating weighted series in the plane#●ready to prove

Let \(\alpha\) and \(\beta\) be real numbers. For \(k \in \mathbb{N}\) let \(x_k = (\alpha, \beta) \in \mathbb{R} \times \mathbb{R}\) if \(k\) is even and \(x_k = (\beta, \alpha)\) if \(k\) is odd. For \(n \in \mathbb{N}\) let \(s_n = \sum_{k=1}^{n} k^{-2} x_k\) (so \(s_0 = 0\)). Then the sequence \((s_n)\) converges in \(\mathbb{R} \times \mathbb{R}\).

public theorem_wanted exists_tendsto_sum_inv_sq_smul_alternating_pair
    (α β : ℝ) (x s : ℕ → (ℝ × ℝ))
    (hx : ∀ k : ℕ, x k = if Even k then (α, β) else (β, α))
    (hs : ∀ n : ℕ, s n = ∑ k ∈ Finset.Icc (1 : ℕ) n,
        (1 / ((k : ℝ) ^ 2)) • x k) :
    ∃ L : (ℝ × ℝ), Tendsto s atTop (𝓝 L)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Sequences, series, summability; Convergence and divergence of infinite limiting processes), problem ma_proofbench_l1_46.

TheoremMonotone functions on a closed interval with a continuous pointwise limit converge uniformly#●ready to prove

Monotone functions on a closed interval with a continuous pointwise limit converge uniformly. Let \(a < b\) be real numbers, let \(f_n : [a, b] \to \mathbb{R}\), \(n \in \mathbb{N}\), be nondecreasing functions, and let \(g : [a, b] \to \mathbb{R}\) be continuous with \(f_n(x) \to g(x)\) for every \(x \in [a, b]\). Then \(g\) is nondecreasing and \(f_n \to g\) uniformly on \([a, b]\).

public theorem_wanted monotone_and_tendstoUniformly_of_monotone_tendsto_continuous
    (a b : ℝ) (hab : a < b) (f : ℕ → (Set.Icc a b) → ℝ) (g : (Set.Icc a b) → ℝ)
    (hmono : ∀ n : ℕ, Monotone (f n))
    (hpt : ∀ x : Set.Icc a b, Tendsto (fun n => f n x) atTop (𝓝 (g x)))
    (hgcont : Continuous g) :
    Monotone g ∧
      TendstoUniformly (fun n x => f n x) g atTop
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_07.

TheoremPower series agreeing at \(1/2, 1/3, 1/4, \dots\) have equal coefficients#●ready to prove

Let \((a_k)\) and \((b_k)\) be real sequences such that the series \(\sum_{k=0}^{\infty} a_k x^k\) and \(\sum_{k=0}^{\infty} b_k x^k\) converge absolutely for every real \(x\) with \(|x| < 1\). If \(\sum_{k=0}^{\infty} a_k x^k = \sum_{k=0}^{\infty} b_k x^k\) for \(x = 1/2, 1/3, 1/4, \dots\), then \(a_k = b_k\) for all \(k \ge 0\).

public theorem_wanted coeff_eq_of_tsum_eq_on_inv_nat_add_two
    (a b : ℕ → ℝ) (ha : ∀ x : ℝ, |x| < 1 → Summable (fun k : ℕ => a k * x ^ k))
    (hb : ∀ x : ℝ, |x| < 1 → Summable (fun k : ℕ => b k * x ^ k))
    (hEq : ∀ n : ℕ, (∑' k : ℕ, a k * ((1 : ℝ) / (n + 2)) ^ k) =
      (∑' k : ℕ, b k * ((1 : ℝ) / (n + 2)) ^ k)) :
    ∀ k : ℕ, a k = b k
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_24.

TheoremStolz–Cesàro theorem#✓fully proved

Let \((a_n)_{n \ge 0}\) and \((b_n)_{n \ge 0}\) be sequences of real numbers such that \((b_n)\) is strictly increasing and \(b_n \to +\infty\) as \(n \to \infty\), and let \(L\) be a real number. If \(\frac{a_{n+1} - a_n}{b_{n+1} - b_n} \to L\) as \(n \to \infty\), then \(\frac{a_n}{b_n} \to L\) as \(n \to \infty\).

theorem stolz_cesaro {a b : ℕ → ℝ} {L : ℝ}
    (hb_mono : StrictMono b)
    (hb_unbounded : Filter.Tendsto b Filter.atTop Filter.atTop)
    (hlim : Filter.Tendsto (fun n => (a (n + 1) - a n) / (b (n + 1) - b n))
      Filter.atTop (nhds L)) :
    Filter.Tendsto (fun n => a n / b n) Filter.atTop (nhds L)
Sources
  • https://en.wikipedia.org/wiki/Stolz%E2%80%93Ces%C3%A0ro_theorem.

TheoremSummability of a rising-product series#✓fully proved

Let \(b\), \(c\) and \(x\) be complex numbers such that \(c + kb \neq 0\) for every integer \(k \ge 1\). Then the series \(\sum_{j=0}^{\infty} \frac{(-b)^j x^{j+1}}{\prod_{k=1}^{j+1} (c + kb)}\) is summable.

theorem summable_neg_pow_mul_pow_div_prod_add_mul {b c : ℂ} (x : ℂ)
    (hc : ∀ r : ℕ, c + b * ((r + 1 : ℕ) : ℂ) ≠ 0) :
    Summable (fun j : ℕ =>
      (-b) ^ j * x ^ (j + 1) / ∏ r ∈ Finset.range (j + 1), (c + b * ((r + 1 : ℕ) : ℂ)))
Used by 2
Used bySummability of Ramanujan's factorial series in a sector, for every \(x\) · Convergence of Ramanujan's product series in a sector

TheoremUniform convergence of \(\sum (1 - \cos(x/n))\) on compact intervals#●ready to prove

For all real numbers \(a < b\) there is a function \(g : \mathbb{R} \to \mathbb{R}\) such that the partial sums \(\sum_{n=1}^{N} \bigl(1 - \cos(x/n)\bigr)\) converge to \(g(x)\) uniformly for \(x \in [a, b]\) as \(N \to \infty\).

public theorem_wanted tendstoUniformlyOn_sum_one_sub_cos_div
    (f : ℕ → ℝ → ℝ) (hf : ∀ n x, f n x = 1 - Real.cos (x / (n + 1))) :
    ∀ a b : ℝ, a < b → ∃ g : ℝ → ℝ,
        TendstoUniformlyOn
          (fun N x => ∑ n ∈ Finset.range N, f n x) g Filter.atTop (Set.Icc a b)
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Sequences, series, summability; Convergence and divergence of infinite limiting processes), problem ma_proofbench_l1_05.

TheoremŚleszyński–Pringsheim convergence criterion#●ready to prove

Let \(a_0, a_1, a_2, \dots\) and \(b_0, b_1, b_2, \dots\) be complex numbers with \(1 + |a_k| \le |b_k|\) for every \(k\). For \(n \ge 0\) let \(f_n\) be the \(n\)-th approximant of the continued fraction \(a_0 / (b_0 + a_1 / (b_1 + \cdots))\), that is \(f_0 = 0\) and \(f_n = a_0 / (b_0 + a_1 / (b_1 + \cdots + a_{n-1} / b_{n-1}))\) for \(n \ge 1\). Then there is a complex number \(v\) with \(|v| \le 1\) such that \(f_n \to v\) as \(n \to \infty\).

Zero partial numerators are admitted.

public theorem_wanted contFract_tendsto_of_pringsheim (a b : ℕ → ℂ)
    (h : ∀ k, 1 + ‖a k‖ ≤ ‖b k‖) :
    ∃ v : ℂ, ‖v‖ ≤ 1 ∧
      Tendsto
        (fun n ↦ (⟨0, Stream'.Seq.ofStream fun k ↦ ⟨a k, b k⟩⟩ : GenContFract ℂ).convs' n)
        atTop (𝓝 v)
Sources
  • Carminda M. Mennen, Möbius Maps and Continued Fractions, INTEGERS 24 (2024), Article A52, Theorem 1.
2 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.