Ratio_Test
Provedconvergence-testsproofwikiseries
If a_n > 0 and lim a_{n+1}/a_n = l < 1, then sum a_n converges.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Ratio_Test (a : ℕ → ℝ) (ha : ∀ n, 0 < a n) (l : ℝ) (hl : l < 1) (hlim : Filter.Tendsto (fun n => a (n + 1) / a n) Filter.atTop (nhds l)) : Summable a := by sorry
Source