Source indexedtheorem · leanprover/lean4:v4.32.0

ZetaAppendix.tsum_even_add_odd'

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3600 to 3610

Mathematical statement

Exact Lean statement

theorem tsum_even_add_odd' {M : Type*} [AddCommMonoid M] [TopologicalSpace M]
    [T2Space M] [ContinuousAdd M] {f : ℕ+ → M}
    (he : Summable fun (k : ℕ+) ↦ f (2 * k))
    (ho : Summable fun (k : ℕ+) ↦ f (2 * k - 1)) :
    ∑' (k : ℕ+), f (2 * k - 1) + ∑' (k : ℕ+), f (2 * k) = ∑' (k : ℕ+), f k

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tsum_even_add_odd' {M : Type*} [AddCommMonoid M] [TopologicalSpace M]    [T2Space M] [ContinuousAdd M] {f : ℕ+ → M}    (he : Summable fun (k : ℕ+) ↦ f (2 * k))    (ho : Summable fun (k : ℕ+) ↦ f (2 * k - 1)) :    ∑' (k : ℕ+), f (2 * k - 1) + ∑' (k : ℕ+), f (2 * k) = ∑' (k : ℕ+), f k := by  symm  rw [← Equiv.tsum_eq (Equiv.pnatEquivNat.symm), ← tsum_even_add_odd,    ← Equiv.tsum_eq (Equiv.pnatEquivNat.symm), ← Equiv.tsum_eq (Equiv.pnatEquivNat.symm)]  · congr  · simpa [← Equiv.summable_iff (Equiv.pnatEquivNat.symm)] using! ho  · simpa [← Equiv.summable_iff (Equiv.pnatEquivNat.symm)] using! he