feat(NumberTheory/LSeries/RiemannZeta): add tsum over ints lemma.

Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

@@ -226,7 +226,7 @@ lemma cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x =
 /-- The cotangent infinite sum representation. -/
 theorem cot_series_rep (hz : x ∈ ℂ_ℤ) :
     π * cot (π * x) = 1 / x + ∑' n : ℕ+, (1 / (x - n) + 1 / (x + n)) := by
-  have h0 := tsum_pnat_eq_tsum_succ fun n ↦ 1 / (x - n) + 1 / (x + n)
+  have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))
   have h1 := cot_series_rep' hz
   simp only [one_div, Nat.cast_add, Nat.cast_one] at *
   rw [h0, ← h1]

Mathlib/NumberTheory/LSeries/RiemannZeta.lean

@@ -197,6 +197,17 @@ theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) :
       (by rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt] : 1 < re k),
     cpow_natCast]
 
+lemma two_riemannZeta_eq_tsum_int_inv_even_pow {k : ℕ} (hk : 2 ≤ k) (hk2 : Even k) :
+    2 * riemannZeta k = ∑' (n : ℤ), ((n : ℂ) ^ k)⁻¹ := by
+  have hkk : 1 < k := by linarith
+  rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]
+  · have h0 : (0 ^ k : ℂ)⁻¹ = 0 := by simp; omega
+    norm_cast
+    simp [h0, zeta_eq_tsum_one_div_nat_add_one_cpow (s := k) (by simp [hkk]),
+      tsum_pnat_eq_tsum_succ (f := fun n => ((n : ℂ) ^ k)⁻¹)]
+  · simp [Even.neg_pow hk2]
+  · exact (Summable.of_nat_of_neg (by simp [hkk]) (by simp [hkk])).of_norm
+
 /-- The residue of `ζ(s)` at `s = 1` is equal to 1. -/
 lemma riemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1) := by
   exact hurwitzZetaEven_residue_one 0

Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

@@ -113,7 +113,7 @@ lemma tsum_pow_div_one_sub_eq_tsum_sigma {r : 𝕜} (hr : ‖r‖ < 1) (k : ℕ)
   have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
     (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
   simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
-    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (fun m ↦ n ^ k * (r ^ n) ^ m)]
+    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]
   have h00 := tsum_prod_pow_eq_tsum_sigma k hr
   rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
   rw [← h00]

Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

@@ -461,6 +461,11 @@ theorem Function.Injective.tprod_eq {g : γ → β} (hg : Injective g) {f : β 
 theorem Equiv.tprod_eq (e : γ ≃ β) (f : β → α) : ∏' c, f (e c) = ∏' b, f b :=
   e.injective.tprod_eq <| by simp
 
+@[to_additive (attr := simp)]
+theorem tprod_comp_neg {β : Type*} [InvolutiveNeg β] (f : β → α) :
+    ∏' d, f (-d) = ∏' d, f d :=
+  (Equiv.neg β).tprod_eq f
+
 /-! ### `tprod` on subsets - part 1 -/
 
 @[to_additive]

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -545,15 +545,38 @@ end IsUniformGroup
 
 end Int
 
-section pnat
+section PNat
 
 @[to_additive]
-theorem pnat_multipliable_iff_multipliable_succ {α : Type*} [TopologicalSpace α] [CommMonoid α]
-    {f : ℕ → α} : Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) :=
+theorem multipliable_pnat_iff_multipliable_succ {f : ℕ → M} :
+    Multipliable (fun x : ℕ+ ↦ f x) ↔ Multipliable fun x ↦ f (x + 1) :=
   Equiv.pnatEquivNat.symm.multipliable_iff.symm
 
+@[deprecated (since := "2025-09-31")]
+alias pnat_multipliable_iff_multipliable_succ := multipliable_pnat_iff_multipliable_succ
+
 @[to_additive]
-theorem tprod_pnat_eq_tprod_succ {α : Type*} [TopologicalSpace α] [CommMonoid α] (f : ℕ → α) :
-    ∏' n : ℕ+, f n = ∏' n, f (n + 1) := (Equiv.pnatEquivNat.symm.tprod_eq _).symm
+theorem tprod_pnat_eq_tprod_succ {f : ℕ → M} : ∏' n : ℕ+, f n = ∏' n, f (n + 1) :=
+  (Equiv.pnatEquivNat.symm.tprod_eq _).symm
 
-end pnat
+@[to_additive]
+lemma tprod_zero_pnat_eq_tprod_nat [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G]
+    {f : ℕ → G} (hf : Multipliable f) :
+    f 0 * ∏' n : ℕ+, f ↑n = ∏' n, f n := by
+  simpa [hf.tprod_eq_zero_mul] using tprod_pnat_eq_tprod_succ
+
+@[to_additive tsum_int_eq_zero_add_two_mul_tsum_pnat]
+theorem tprod_int_eq_zero_mul_tprod_pnat_sq [UniformSpace G] [IsUniformGroup G] [CompleteSpace G]
+    [T2Space G] {f : ℤ → G} (hf : ∀ n : ℤ, f (-n) = f n) (hf2 : Multipliable f) :
+    ∏' n, f n = f 0 * (∏' n : ℕ+, f n) ^ 2 := by
+  have hf3 : Multipliable fun n : ℕ ↦ f n :=
+    (multipliable_int_iff_multipliable_nat_and_neg.mp hf2).1
+  have hf4 : Multipliable fun n : ℕ+ ↦ f n := by
+    rwa [multipliable_pnat_iff_multipliable_succ (f := (f ·)),
+      multipliable_nat_add_iff 1 (f := (f ·))]
+  have := tprod_nat_mul_neg hf2
+  rw [← tprod_zero_pnat_eq_tprod_nat (by simpa [hf] using hf3.mul hf3), mul_comm _ (f 0)] at this
+  simp only [hf, Nat.cast_zero, mul_assoc, mul_right_inj] at this
+  rw [← this, mul_right_inj, hf4.tprod_mul hf4, sq]
+
+end PNat