feat(analysis/complex/basic): a complex-valued function has_sum iff…

… its real part and imaginary part `has_sum` (#9648)

src/analysis/complex/basic.lean

@@ -193,6 +193,35 @@ noncomputable instance : is_R_or_C ℂ :=
     complex.of_real_eq_coe, complex.norm_eq_abs],
   div_I_ax := complex.div_I }
 
+section
+
+variables {α β γ : Type*}
+  [add_comm_monoid α] [topological_space α] [add_comm_monoid γ] [topological_space γ]
+
+/-- The natural `add_equiv` from `ℂ` to `ℝ × ℝ`. -/
+def equiv_real_prod_add_hom : ℂ ≃+ ℝ × ℝ :=
+{ map_add' := by simp, .. equiv_real_prod }
+
+/-- The natural `linear_equiv` from `ℂ` to `ℝ × ℝ`. -/
+def equiv_real_prod_add_hom_lm : ℂ ≃ₗ[ℝ] ℝ × ℝ :=
+{ map_smul' := by simp [equiv_real_prod_add_hom], .. equiv_real_prod_add_hom }
+
+/-- The natural `continuous_linear_equiv` from `ℂ` to `ℝ × ℝ`. -/
+def equiv_real_prodₗ : ℂ ≃L[ℝ] ℝ × ℝ :=
+equiv_real_prod_add_hom_lm.to_continuous_linear_equiv
+
+end
+
+lemma has_sum_iff {α} (f : α → ℂ) (c : ℂ) :
+  has_sum f c ↔ has_sum (λ x, (f x).re) c.re ∧ has_sum (λ x, (f x).im) c.im :=
+begin
+  refine ⟨λ h, ⟨h.mapL re_clm, h.mapL im_clm⟩, _⟩,
+  rintro ⟨h₁, h₂⟩,
+  convert (h₁.prod_mk h₂).mapL equiv_real_prodₗ.symm.to_continuous_linear_map,
+  { ext x; refl },
+  { cases c, refl }
+end
+
 end complex
 
 namespace is_R_or_C

src/topology/algebra/infinite_sum.lean

@@ -536,6 +536,17 @@ lemma tsum_even_add_odd {f : ℕ → α} (he : summable (λ k, f (2 * k)))
 
 end tsum
 
+section prod
+
+variables [add_comm_monoid α] [topological_space α] [add_comm_monoid γ] [topological_space γ]
+
+lemma has_sum.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ}
+  (hf : has_sum f a) (hg : has_sum g b) :
+  has_sum (λ x, (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩ :=
+by simp [has_sum, ← prod_mk_sum, filter.tendsto.prod_mk_nhds hf hg]
+
+end prod
+
 section pi
 variables {ι : Type*} {π : α → Type*} [∀ x, add_comm_monoid (π x)] [∀ x, topological_space (π x)]