continuous_laplaceIntegral_verticalLine_add_of_integrable

theorem continuous_laplaceIntegral_verticalLine_add_of_integrable    {φ : ℝ → ℂ} {σ : ℝ} (hφ_cont : Continuous φ)    (hφ_int : Integrable (fun y : ℝ => exp (-((σ : ℂ) * (y : ℂ))) * φ y)) :    Continuous      (fun t : ℝ => ∫ y : ℝ, φ y * exp (-(((σ : ℂ) + (t : ℂ) * I) * (y : ℂ)))) := by  rw [continuous_iff_continuousAt]  intro t0  let bound : ℝ → ℝ := fun y => ‖exp (-((σ : ℂ) * (y : ℂ))) * φ y‖  let F : ℝ → ℝ → ℂ := fun t y =>    φ y * exp (-(((σ : ℂ) + (t : ℂ) * I) * (y : ℂ)))  have hbound_int : Integrable bound := by    simpa [bound, mul_comm] using hφ_int.norm  have hF_meas : ∀ᶠ t in 𝓝 t0, AEStronglyMeasurable (F t) volume := by    refine Eventually.of_forall ?_    intro t    dsimp [F]    exact (hφ_cont.mul (continuous_exp.comp (by fun_prop))).aestronglyMeasurable  have h_bound : ∀ᶠ t in 𝓝 t0, ∀ᵐ y ∂volume, ‖F t y‖ ≤ bound y := by    refine Eventually.of_forall ?_    intro t    filter_upwards with y    dsimp [F, bound]    rw [norm_mul, norm_mul, norm_exp, norm_exp]    have hsig : (-(↑σ * ↑y) : ℂ).re = -σ * y := by      norm_num [Complex.mul_re]    have ht : (-((↑σ + ↑t * I) * ↑y) : ℂ).re = -σ * y := by      norm_num [Complex.mul_re, Complex.I_re, Complex.I_im]    rw [hsig, ht]    rw [mul_comm]  have h_lim : ∀ᵐ y ∂volume, Tendsto (fun t => F t y) (𝓝 t0) (𝓝 (F t0 y)) := by    filter_upwards with y    dsimp [F]    have hcont : Continuous        (fun t : ℝ => φ y * exp (-(((σ : ℂ) + (t : ℂ) * I) * (y : ℂ)))) := by      fun_prop    exact hcont.continuousAt  have h_tendsto :=    tendsto_integral_filter_of_dominated_convergence      (μ := volume) bound hF_meas h_bound hbound_int h_lim  unfold ContinuousAt  simpa [F] using h_tendsto