English
If f is summable in a complete uniform ring, then the alternating sum ∑ (-1)^n f(n) is summable.
Русский
Если f суммируема в полном единообразном кольце, то чередующаяся сумма ∑(-1)^n f(n) суммируема.
LaTeX
$$$\\displaystyle \\text{Summable}(f) \\implies \\text{Summable}\\bigl(n \\mapsto (-1)^n \\cdot f(n)\\bigr)$$$
Lean4
theorem alternating {α} [Ring α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ℕ → α}
(hf : Summable f) : Summable (fun n => (-1) ^ n * f n) :=
by
apply Summable.even_add_odd
· simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]
exact hf.comp_injective (mul_right_injective₀ (two_ne_zero' ℕ))
· simp only [pow_add, even_two, Even.mul_right, Even.neg_pow, one_pow, pow_one, mul_neg, mul_one, neg_mul, one_mul]
apply Summable.neg
apply hf.comp_injective
exact (add_left_injective 1).comp (mul_right_injective₀ (two_ne_zero' ℕ))
