CH2.Phi_star.continuousAt_imag

theorem Phi_star.continuousAt_imag (ν ε t : ℝ) (ht : 0 ≤ t) (hν : ν > 0) :    ContinuousAt (fun s : ℝ ↦ Phi_star ν ε (I * ↑s)) t := by  simp only [Phi_star]  have h_eq (s : ℝ) : -2 * π * I * (I * s) + ν = ↑(2 * π * s + ν) := by    ring_nf; simp  simp_rw [h_eq]  apply ContinuousAt.div_const  apply ContinuousAt.sub  · let f : ℝ → ℝ := fun x ↦ 2 * π * x + ν    have hf : ContinuousAt f t := by fun_prop    have hg : ContinuousAt (fun x : ℝ ↦ B ε ↑x) (f t) :=      B.continuousAt_ofReal_ne_zero ε (f t) (by nlinarith [Real.pi_pos])    exact hg.comp hf  · exact continuousAt_const