CH2.second_contour_integrand_holomorphicOn

lemma second_contour_integrand_holomorphicOn (ν ε x : ℝ) (T : ℝ) (_hT : T ≥ 0) :    HolomorphicOn (fun z ↦ Phi_star ν ε z * E (-z * x))      (Rectangle (↑(-1/2 : ℝ)) (↑(0 : ℝ) - I * ↑T)) := by  intro z hz  apply DifferentiableWithinAt.mul  · apply AnalyticAt.differentiableWithinAt    apply Phi_star.analyticAt_of_not_pole_nz    intro n hn h_eq    have h_z_re : z.re = n := by      replace h_eq := congr_arg Complex.re h_eq      simp only [sub_re, intCast_re] at h_eq      rw [pole_re] at h_eq      simp only [sub_zero] at h_eq      exact h_eq    have h_re := hz.1    simp only [Set.mem_preimage, ofReal_re, sub_re, mul_re, I_re, I_im, ofReal_im,      zero_mul, mul_zero, sub_zero] at h_re    rw [Set.uIcc_of_le (by norm_num), Set.mem_Icc, h_z_re] at h_re    exact hn (unique_int_in_Icc n 0 h_re (by norm_num) (by norm_num))  · dsimp [E]; apply DifferentiableAt.differentiableWithinAt; fun_prop