Alternating_Series_Test
Disprovedconvergence-testsproofwikiseries
If a_n is a decreasing sequence of non-negative reals converging to 0, then the alternating series sum (-1)^n a_n converges.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Alternating_Series_Test (a : ℕ → ℝ) (ha_pos : ∀ n, 0 ≤ a n) (ha_dec : Antitone a) (ha_lim : Filter.Tendsto a Filter.atTop (nhds 0)) : Summable (fun n => (-1) ^ n * a n) := by sorry
Source