Limit_Comparison_Test
Provedconvergence-testsproofwikiseries
If a_n/b_n converges to a positive limit l and sum b_n converges, then sum a_n converges.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_Comparison_Test (a b : ℕ → ℝ) (ha : ∀ n, 0 < a n) (hb : ∀ n, 0 < b n) (l : ℝ) (hl : 0 < l) (hlim : Filter.Tendsto (fun n => a n / b n) Filter.atTop (nhds l)) (hbs : Summable b) : Summable a := by sorry
Source