[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): add more pnat tsum lemmas

Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

@@ -216,10 +216,9 @@ theorem 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 h1 := cot_series_rep' hz
-  simp only [one_div, Nat.cast_add, Nat.cast_one] at *
-  rw [h0, ← h1]
+  have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))
+  rw [one_div] at *
+  rw [h0, ← cot_series_rep' hz]
   ring
 
 end MittagLeffler

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -529,17 +529,46 @@ lemma multipliable_int_iff_multipliable_nat_and_neg {f : ℤ → G} :
 
 end IsUniformGroup
 
+theorem tsum_int_eq_tsum_neg {α : Type*} [AddCommMonoid α] [TopologicalSpace α] (f : ℤ → α) :
+    ∑' d, f (-d) = ∑' d, f d := by
+  rw [show (fun d => f (-d)) = (fun d => f d) ∘ (Equiv.neg ℤ) by ext; simp]
+  apply (Equiv.neg ℤ).tsum_eq
+
 end Int
 
 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) :=
-  Equiv.pnatEquivNat.symm.multipliable_iff.symm
+variable {α R : Type*} [TopologicalSpace α] [CommMonoid α] [AddMonoidWithOne R]
+
+
+@[to_additive (dont_translate := R)]
+theorem pnat_multipliable_iff_multipliable_succ {f : R → α} :
+    Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) := by
+  convert Equiv.pnatEquivNat.symm.multipliable_iff.symm
+  simp
+
+@[to_additive (dont_translate := R)]
+theorem tprod_pnat_eq_tprod_succ {f : R → α} : ∏' n : ℕ+, f n = ∏' (n : ℕ), f (n + 1) := by
+  convert (Equiv.pnatEquivNat.symm.tprod_eq _).symm
+  simp
 
 @[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
+lemma tprod_zero_pnat_eq_tprod_nat {α : Type*} [TopologicalSpace α] [CommGroup α]
+    [IsTopologicalGroup α] [T2Space α] (f : ℕ → α) (hf : Multipliable f) :
+    f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n := by
+  simpa [Multipliable.tprod_eq_zero_mul hf] using tprod_pnat_eq_tprod_succ (f := f)
+
+theorem tsum_nat_eq_zero_two_pnat {α : Type*} [UniformSpace α] [Ring α] [IsUniformAddGroup α]
+    [CompleteSpace α] [T2Space α] {f : ℤ → α} (hf : ∀ n : ℤ, f n = f (-n)) (hf2 : Summable f) :
+    ∑' n, f n = f 0 + 2 * ∑' n : ℕ+, f n := by
+  rw [tsum_of_add_one_of_neg_add_one]
+  · conv =>
+      enter [1,2,1,n]
+      rw [hf]
+    simp only [neg_add_rev, Int.reduceNeg, neg_neg, tsum_pnat_eq_tsum_succ, two_mul]
+    abel
+  · simpa using ((summable_nat_add_iff (k := 1)).mpr
+      (summable_int_iff_summable_nat_and_neg.mp hf2).1)
+  · exact (summable_nat_add_iff (k := 1)).mpr (summable_int_iff_summable_nat_and_neg.mp hf2).2
 
 end pnat