laplace_integrand_integrable

theorem laplace_integrand_integrable {φ : ℝ → ℂ} {b σ : ℝ} (hφ : Continuous φ)    (hφ_decay : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[cocompact ℝ]      fun x ↦ Real.exp (-(1/2+b)*|x|))    (hσ_top : -(1+b) < σ) (hσ_bot : σ < b) :    Integrable (fun y : ℝ ↦ φ y * Complex.exp (-(σ:ℂ)*y)) := by  have h_loc : LocallyIntegrable (fun y : ℝ ↦ φ y * Complex.exp (-(σ:ℂ)*y)) :=    (hφ.mul (by fun_prop)).locallyIntegrable  have hbig_top : (fun y : ℝ ↦ φ y * Complex.exp (-(σ:ℂ)*y)) =O[atTop]      (fun y ↦ Real.exp (-(1+b+σ)*y)) := by    have hφ_top : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[atTop]        fun x ↦ Real.exp (-(1/2+b)*|x|) :=      hφ_decay.mono (by rw [cocompact_eq_atBot_atTop]; exact le_sup_right)    rw [isBigO_iff] at hφ_top ⊢    obtain ⟨C, hC⟩ := hφ_top    refine ⟨C, ?_⟩    filter_upwards [hC, eventually_ge_atTop 0] with y hy hy0    rw [show ‖φ y * Complex.exp (-(σ:ℂ)*y)‖ = ‖φ y‖ * Real.exp (-σ*y) by          rw [norm_mul, Complex.norm_exp]; congr 1; simp, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]    rw [show ‖φ y * Complex.exp ((y:ℂ)/2)‖ = ‖φ y‖ * Real.exp (y/2) by          rw [norm_mul, Complex.norm_exp]; congr 1; simp,        Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), abs_of_nonneg hy0] at hy    rw [show -σ*y = y/2 + -(σ+1/2)*y by ring, show -(1+b+σ)*y = -(1/2+b)*y + -(σ+1/2)*y by ring,        Real.exp_add, Real.exp_add, ← mul_assoc, ← mul_assoc]    exact mul_le_mul_of_nonneg_right hy (le_of_lt (Real.exp_pos _))  have hbig_bot : (fun y : ℝ ↦ φ y * Complex.exp (-(σ:ℂ)*y)) =O[atBot]      (fun y ↦ Real.exp ((b-σ)*y)) := by    have hφ_bot : (fun x : ℝ ↦ φ x * Complex.exp ((x:ℂ)/2)) =O[atBot]        fun x ↦ Real.exp (-(1/2+b)*|x|) :=      hφ_decay.mono (by rw [cocompact_eq_atBot_atTop]; exact le_sup_left)    rw [isBigO_iff] at hφ_bot ⊢    obtain ⟨C, hC⟩ := hφ_bot    refine ⟨C, ?_⟩    filter_upwards [hC, eventually_le_atBot 0] with y hy hy0    rw [show ‖φ y * Complex.exp (-(σ:ℂ)*y)‖ = ‖φ y‖ * Real.exp (-σ*y) by          rw [norm_mul, Complex.norm_exp]; congr 1; simp, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]    rw [show ‖φ y * Complex.exp ((y:ℂ)/2)‖ = ‖φ y‖ * Real.exp (y/2) by          rw [norm_mul, Complex.norm_exp]; congr 1; simp,        Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), abs_of_nonpos hy0] at hy    rw [show -σ*y = y/2 + (-σ-1/2)*y by ring, show (b-σ)*y = -(1/2+b)*(-y) + (-σ-1/2)*y by ring,        Real.exp_add, Real.exp_add, ← mul_assoc, ← mul_assoc]    exact mul_le_mul_of_nonneg_right hy (le_of_lt (Real.exp_pos _))  have hint_top : IntegrableAtFilter (fun y : ℝ ↦ Real.exp (-(1+b+σ)*y)) atTop volume :=    ⟨Ioi 0, Ioi_mem_atTop 0, exp_neg_integrableOn_Ioi 0 (by linarith)⟩  have hint_bot : IntegrableAtFilter (fun y : ℝ ↦ Real.exp ((b-σ)*y)) atBot volume := by    have hα : 0 < b - σ := by linarith    have h_top : IntegrableAtFilter (fun y : ℝ ↦ Real.exp (-((b-σ)*y))) atTop volume :=      ⟨Ioi 0, Ioi_mem_atTop 0, by simpa only [neg_mul] using exp_neg_integrableOn_Ioi 0 hα⟩    rw [← Filter.map_neg_atTop, measurableEmbedding_neg.integrableAtFilter_iff_comap]    have hvol : (volume : Measure ℝ).comap Neg.neg = volume := by      convert! (MeasurableEquiv.neg ℝ).map_symm.symm using 1; simp    rw [hvol, Function.comp_def]; simp only [mul_neg]; exact h_top  exact h_loc.integrable_of_isBigO_atBot_atTop hbig_bot hint_bot hbig_top hint_top