Comparison_Test

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

convergence-testsnamed-theoremsproofwikiseries

Let $\displaystyle \sum_{n \mathop = 1}^\infty b_n$ be a convergent series of positive real numbers. Let $\sequence {a_n}$ be a sequence $\R$ or sequence in $\C$ . Let $\forall n \in \N_{>0}: \cmod {a_n} \le b_n$ . Then the series $\displaystyle \sum_{n \mathop = 1}^\infty a_n$ converges absolutely.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

theorem Comparison_Test (a b : ℕ → ℝ) (hb : Summable b) (hb_pos : ∀ n, 0 ≤ b n) (hab : ∀ n, |a n| ≤ b n) : Summable a := by sorry

Source

https://proofwiki.org/wiki/Comparison_Test

View graph