CH2.Phi_fourier_holo_right

lemma Phi_fourier_holo_right (ν ε x : ℝ) (hν : ν > 0) :    ∃ g : ℂ → ℂ, (∀ U : ℝ, U ≥ 0 → HolomorphicOn g (Rectangle (1/2 : ℂ) (1 - 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)  have h_mero : MeromorphicAt f_base z₁ := (Phi_circ.meromorphic ν ε z₁).add (Phi_star.meromorphic ν ε z₁)  have h_order : meromorphicOrderAt f_base z₁ ≥ 0 := meromorphicOrderAt_phi_add_nonneg ν ε hν  obtain ⟨c_base, h_tendsto_base⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg h_mero h_order  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 h_mero h_tendsto_base      rw [hz₁]      exact 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]          simp [Complex.sub_re, Complex.mul_re, Complex.div_re, Complex.I_re, Complex.I_im, Complex.ofReal_re, Complex.ofReal_im]        have h_im : z.im = -ν / (2 * π) := by          rw [hn]          simp [Complex.sub_im, Complex.mul_im, Complex.div_im, Complex.I_im, Complex.I_re]          field_simp        have h_rect := hz        rw [Rectangle, Complex.mem_reProdIm] at h_rect        simp only [one_re, div_ofNat_re, sub_re, mul_re, I_re, ofReal_re, zero_mul, I_im,          ofReal_im, mul_zero, sub_self, sub_zero, sub_im, div_ofNat_im,          mul_im, one_mul, zero_add] at h_rect        rw [Set.uIcc_of_le (by norm_num), Set.uIcc_of_ge (by simp; 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        have : z = z₁ := by          apply Complex.ext <;> dsimp [z₁, z₁_pole]          · rw [h_re]; simp; norm_cast          · rw [h_im]            simp [Complex.div_re, Complex.div_im, Complex.ofReal_re, Complex.ofReal_im]            field_simp [Real.pi_ne_zero]        exact hz₁ this      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]        exact ((Phi_circ.analyticAt_of_not_pole ν ε z h_not_pole).add          (Phi_star.analyticAt_of_not_pole ν ε z h_not_pole)).mul (by unfold E; fun_prop)      exact h_anal_z.differentiableAt.differentiableWithinAt  · intro z hz; dsimp [g]; rw [if_neg hz]