CH2.integrableOn_Phi_star_m12

lemma integrableOn_Phi_star_m12 (ν ε x T : ℝ) :    IntegrableOn (fun a : ℝ ↦ Phi_star ν ε (-1 / 2 - I * ↑a) * cexp (2 * ↑π * I * (-(-1 / 2 - I * ↑a) * ↑x))) (Set.Icc 0 T) := by  apply ContinuousOn.integrableOn_Icc  apply ContinuousOn.mul  · intro a _    apply ContinuousAt.continuousWithinAt    have h_ana : AnalyticAt ℂ (Phi_star ν ε) (-1 / 2 - I * ↑a) := by      apply Phi_star.analyticAt_of_re_ne_int      intro ⟨n, hn⟩; replace hn := congr_arg (· * 2) hn; norm_num at hn; norm_cast at hn; omega    exact ContinuousAt.comp (f := fun a : ℝ ↦ (-1 / 2 : ℂ) - I * ↑a) h_ana.continuousAt (by fun_prop)  · exact Continuous.continuousOn (by fun_prop)