feat(topology/algebra/infinite_sum): add tsum_star (#13999)

These lemmas names are copied from `tsum_neg` and friends.

As a result, `star_exp` can be golfed and generalized.

src/analysis/normed_space/exponential.lean

@@ -125,6 +125,10 @@ begin
   simp [h]
 end
 
+lemma star_exp [t2_space 𝔸] [star_ring 𝔸] [has_continuous_star 𝔸] (x : 𝔸) :
+  star (exp 𝕂 x) = exp 𝕂 (star x) :=
+by simp_rw [exp_eq_tsum, ←star_pow, ←star_inv_nat_cast_smul, ←tsum_star]
+
 variables (𝕂)
 
 lemma commute.exp_right [t2_space 𝔸] {x y : 𝔸} (h : commute x y) : commute x (exp 𝕂 y) :=
@@ -599,17 +603,3 @@ lemma exp_ℝ_ℂ_eq_exp_ℂ_ℂ : (exp ℝ : ℂ → ℂ) = exp ℂ :=
 exp_eq_exp ℝ ℂ ℂ
 
 end scalar_tower
-
-lemma star_exp {𝕜 A : Type*} [is_R_or_C 𝕜] [normed_ring A] [normed_algebra 𝕜 A]
-  [star_ring A] [normed_star_group A] [complete_space A]
-  [star_module 𝕜 A] (a : A) : star (exp 𝕜 a) = exp 𝕜 (star a) :=
-begin
-  rw exp_eq_tsum,
-  have := continuous_linear_map.map_tsum
-    (starₗᵢ 𝕜 : A ≃ₗᵢ⋆[𝕜] A).to_linear_isometry.to_continuous_linear_map
-    (exp_series_summable' a),
-  dsimp at this,
-  convert this,
-  funext,
-  simp only [star_smul, star_pow, one_div, star_inv', star_nat_cast],
-end

src/analysis/normed_space/star/exponential.lean

@@ -23,7 +23,7 @@ subtypes `self_adjoint A` and `unitary A`.
 section star
 
 variables {A : Type*}
-[normed_ring A] [normed_algebra ℂ A] [star_ring A] [cstar_ring A] [complete_space A]
+[normed_ring A] [normed_algebra ℂ A] [star_ring A] [has_continuous_star A] [complete_space A]
 [star_module ℂ A]
 
 open complex

src/topology/algebra/infinite_sum.lean

@@ -246,6 +246,26 @@ lemma function.surjective.summable_iff_of_has_sum_iff {α' : Type*} [add_comm_mo
   summable f ↔ summable g :=
 hes.exists.trans $ exists_congr $ @he
 
+section has_continuous_star
+variables [star_add_monoid α] [has_continuous_star α]
+
+lemma has_sum.star (h : has_sum f a) : has_sum (λ b, star (f b)) (star a) :=
+by simpa only using h.map (star_add_equiv : α ≃+ α) continuous_star
+
+lemma summable.star (hf : summable f) : summable (λ b, star (f b)) :=
+hf.has_sum.star.summable
+
+lemma summable.of_star (hf : summable (λ b, star (f b))) : summable f :=
+by simpa only [star_star] using hf.star
+
+@[simp] lemma summable_star_iff : summable (λ b, star (f b)) ↔ summable f :=
+⟨summable.of_star, summable.star⟩
+
+@[simp] lemma summable_star_iff' : summable (star f) ↔ summable f :=
+summable_star_iff
+
+end has_continuous_star
+
 variable [has_continuous_add α]
 
 lemma has_sum.add (hf : has_sum f a) (hg : has_sum g b) : has_sum (λb, f b + g b) (a + b) :=
@@ -474,6 +494,19 @@ end
 
 end has_continuous_add
 
+section has_continuous_star
+variables [star_add_monoid α] [has_continuous_star α]
+
+lemma tsum_star : star (∑' b, f b) = ∑' b, star (f b) :=
+begin
+  by_cases hf : summable f,
+  { exact hf.has_sum.star.tsum_eq.symm, },
+  { rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt summable.of_star hf),
+        star_zero] },
+end
+
+end has_continuous_star
+
 section encodable
 open encodable
 variable [encodable γ]