CH2.first_contour_integrand_holomorphicOn

lemma first_contour_integrand_holomorphicOn (ν ε x : ℝ) (z' w' z₀ : ℂ)    (hz₀ : z₀ = -(I * ν) / (2 * π))    (h_rect_re : Set.uIcc z'.re w'.re = Set.Icc (-1 / 2 : ℝ) (1 / 2)) :    HolomorphicOn (fun z ↦ Phi_circ ν ε z * E (-z * x)) (Rectangle z' w' \ {z₀}) := by  intro z hz  apply DifferentiableAt.differentiableWithinAt  apply DifferentiableAt.mul  · apply AnalyticAt.differentiableAt    apply Phi_circ.analyticAt_of_not_pole ν ε z    intro n hn    by_cases hn0 : n = 0    · subst hn0; have : z = z₀ := by rw [hn, hz₀]; ring      exact hz.2 this    · have hz_re : z.re ∈ Set.Icc (-1 / 2 : ℝ) (1 / 2) := h_rect_re ▸ hz.1.1      rw [hn, Complex.sub_re, pole_re ν, sub_zero, Complex.intCast_re] at hz_re      exact hn0 (unique_int_in_Icc n 0 hz_re (by norm_num) (by norm_num))  · apply DifferentiableAt.comp    · exact analyticAt_cexp.differentiableAt    · fun_prop