continuous_laplaceIntegral_verticalLine_of_integrable

theorem continuous_laplaceIntegral_verticalLine_of_integrable    {f : ℝ → ℂ} {sigma : ℝ} (hf_cont : Continuous f)    (hf_int : Integrable (fun y : ℝ => exp (-((sigma : ℂ) * (y : ℂ))) * f y)) :    Continuous (fun t : ℝ => laplaceIntegral f ((sigma : ℂ) - (t : ℂ) * I)) := by  rw [continuous_iff_continuousAt]  intro t0  let bound : ℝ → ℝ := fun y => ‖exp (-((sigma : ℂ) * (y : ℂ))) * f y‖  let F : ℝ → ℝ → ℂ := fun t y =>    f y * exp ((((t : ℂ) * I - (sigma : ℂ)) * (y : ℂ)))  have hbound_int : Integrable bound := by    simpa [bound, mul_comm] using hf_int.norm  have hF_meas : ∀ᶠ t in 𝓝 t0, AEStronglyMeasurable (F t) volume := by    refine Eventually.of_forall ?_    intro t    dsimp [F]    exact (hf_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 : (-(↑sigma * ↑y) : ℂ).re = -sigma * y := by      norm_num [Complex.mul_re]    have ht : (((↑t * I - ↑sigma) * ↑y) : ℂ).re = -sigma * 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 : ℝ => f y * exp ((((t : ℂ) * I - (sigma : ℂ)) * (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 laplaceIntegral  simpa [F, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using h_tendsto