Kadiri.kadiri_laplace_shifted_vertical_segment_continuousOn

lemma kadiri_laplace_shifted_vertical_segment_continuousOn    {φ : ℝ → ℂ} (hφ : ContDiff ℝ 1 φ)    {b : ℝ} (_hb : 0 < b)    (hφ_decay : (fun x : ℝ ↦ φ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|))    {a T : ℝ} (ha : 0 < a) (hab : a < b) (_ha1 : a < 1) :    ContinuousOn      (fun t : ℝ =>        let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume        let s : ℂ := ((-a : ℝ) : ℂ) + (t : ℂ) * I        Φ (-s))      (Set.Icc (-T) T) := by  have h_weighted :      Integrable (fun y : ℝ => exp (-((a : ℂ) * (y : ℂ))) * φ y) :=    kadiri_laplace_positive_line_weight_integrable hφ hφ_decay ha hab  have hcont :=    continuous_laplaceIntegral_verticalLine_of_integrable      (f := φ) (sigma := a) hφ.continuous h_weighted  refine hcont.continuousOn.congr ?_  intro t _ht  dsimp [laplaceIntegral]  apply integral_congr_ae  filter_upwards with y  apply congrArg (fun z : ℂ => φ y * exp (-z * (y : ℂ)))  simp [sub_eq_add_neg, add_comm]