CH2.third_contour_integrand_holomorphicOn

lemma third_contour_integrand_holomorphicOn (ν ε x : ℝ) (U : ℝ) (_hU : U ≥ 0) :    HolomorphicOn (fun z ↦ Phi_star ν ε z * E (-z * x)) (Rectangle (0 : ℂ) (1/2 - I * U)) := 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, pole_re, sub_zero] at h_eq      exact h_eq    have h_re := hz.1    simp only [Set.mem_preimage, Complex.zero_re, Complex.sub_re, Complex.mul_re,      Complex.I_re, Complex.I_im, Complex.ofReal_re, Complex.ofReal_im] at h_re    rw [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