CH2.Phi_fourier_holo_left

lemma Phi_fourier_holo_left (ν ε x : ℝ) (hν : ν > 0) :    ∃ g : ℂ → ℂ, (∀ U : ℝ, U ≥ 0 → HolomorphicOn g (Rectangle (-1 : ℂ) (-1 / 2 - I * U))) ∧    Set.EqOn g (fun z ↦ (Phi_circ ν ε z - Phi_star ν ε z) * E (-z * x)) {z | z ≠ z₀_pole ν} := by  let z₀ := z₀_pole ν  let f_base (z : ℂ) := (Phi_circ ν ε z - Phi_star ν ε z)  let f (z : ℂ) := f_base z * E (-z * x)  obtain ⟨c_base, h_tendsto_base⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg    ((Phi_circ.meromorphic ν ε z₀).sub (Phi_star.meromorphic ν ε z₀))    (meromorphicOrderAt_phi_diff_nonneg ν ε hν)  let c := c_base * E (-z₀ * x)  let g (z : ℂ) := if z = z₀ then c else f z  use g  constructor  · intro U hU z hz    by_cases hz₀ : z = z₀    · have h_anal_z₀ : AnalyticAt ℂ g z₀ :=        analyticAt_removable_sing_mul_E x          ((Phi_circ.meromorphic ν ε z₀).sub (Phi_star.meromorphic ν ε z₀))          h_tendsto_base      exact (hz₀ ▸ h_anal_z₀).differentiableAt.differentiableWithinAt    · have h_not_pole : ∀ n : ℤ, z ≠ ↑n - I * ↑ν / (2 * ↑π) := by        intro n hn; have h_re : z.re = n := by          rw [hn, Complex.sub_re, Complex.intCast_re, mul_div_assoc, Complex.I_mul_re]          simp; field_simp; norm_cast        have h_im : z.im = -ν / (2 * π) := by          rw [hn, Complex.sub_im, Complex.intCast_im, mul_div_assoc, Complex.I_mul_im]          norm_cast; ring        have h_rect := hz; rw [Rectangle, Complex.mem_reProdIm] at h_rect        simp only [neg_re, one_re, sub_re, div_ofNat_re, mul_re, I_re, ofReal_re, zero_mul, I_im,          ofReal_im, mul_zero, sub_self, sub_zero, neg_im, one_im, neg_zero, sub_im, div_ofNat_im,          zero_div, mul_im, one_mul, zero_add, zero_sub] at h_rect        rw [Set.uIcc_of_le (by norm_num), Set.uIcc_of_ge (by linarith)] at h_rect        have h_n : n = -1 := unique_int_in_Icc n (-1) (h_re ▸ h_rect.1) (by norm_num) (by norm_num)        subst h_n        exact hz₀ (Complex.ext          (by            rw [h_re]            dsimp [z₀, z₀_pole]            simp [Complex.div_im, Complex.ofReal_re, Complex.ofReal_im]          )          (by rw [h_im]; dsimp [z₀, z₀_pole]; simp; norm_cast; ring))      have h_anal_z : AnalyticAt ℂ g z := by        have h_eq : g =ᶠ[nhds z] f := by          filter_upwards [eventually_ne_nhds hz₀] with w hw          dsimp [g]; rw [if_neg hw]        rw [analyticAt_congr h_eq]        apply AnalyticAt.mul        · exact (Phi_circ.analyticAt_of_not_pole ν ε z h_not_pole).sub            (Phi_star.analyticAt_of_not_pole ν ε z h_not_pole)        · unfold E; fun_prop      exact h_anal_z.differentiableAt.differentiableWithinAt  · intro z hz; dsimp [g]; rw [if_neg hz]