Kadiri.kadiri_laplace_full_strip_weight_integrable_of_continuous

theorem kadiri_laplace_full_strip_weight_integrable_of_continuous {ψ : ℝ → ℂ}    (hψ : Continuous ψ) {b σ : ℝ}    (hσlo : -b < σ) (hσhi : σ < 1 + b)    (hψ_decay : (fun x : ℝ ↦ ψ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :    Integrable (fun y : ℝ => exp ((σ : ℂ) * (y : ℂ)) * ψ y) := by  let F : ℝ → ℂ := fun y => exp ((σ : ℂ) * (y : ℂ)) * ψ y  have hF_cont : Continuous F := by    dsimp [F]    fun_prop  have hF_loc : LocallyIntegrable F volume := hF_cont.locallyIntegrable  have hshape : ∀ x : ℝ,      ‖F x‖ = Real.exp ((σ - 1 / 2) * x) * ‖ψ x * exp ((x : ℂ) / 2)‖ := by    intro x    dsimp [F]    rw [norm_mul, norm_mul, Complex.norm_exp, Complex.norm_exp]    have h1 : ((↑σ * ↑x) : ℂ).re = σ * x := by      norm_num [Complex.mul_re]    have h2 : ((x : ℂ) / 2).re = x / 2 := by      norm_num    rw [h1, h2]    calc      Real.exp (σ * x) * ‖ψ x‖          = (Real.exp ((σ - 1 / 2) * x) * Real.exp (x / 2)) * ‖ψ x‖ := by            rw [← Real.exp_add]            congr 1            ring_nf      _ = Real.exp ((σ - 1 / 2) * x) * (‖ψ x‖ * Real.exp (x / 2)) := by            ring_nf  have htop_decay := hψ_decay.mono (show Filter.atTop ≤ Filter.cocompact ℝ from    atTop_le_cocompact)  have hbot_decay := hψ_decay.mono (show Filter.atBot ≤ Filter.cocompact ℝ from    atBot_le_cocompact)  have htop : F =O[Filter.atTop] fun x : ℝ => Real.exp ((σ - 1 - b) * x) := by    rw [Asymptotics.isBigO_iff] at htop_decay ⊢    obtain ⟨C, hC⟩ := htop_decay    refine ⟨C, ?_⟩    filter_upwards [hC, Filter.eventually_gt_atTop (0 : ℝ)] with x hxC hxpos    rw [hshape]    calc      Real.exp ((σ - 1 / 2) * x) * ‖ψ x * exp ((x : ℂ) / 2)‖          ≤ Real.exp ((σ - 1 / 2) * x) *              (C * ‖Real.exp (-(1 / 2 + b) * |x|)‖) := by            exact mul_le_mul_of_nonneg_left hxC (Real.exp_nonneg _)      _ = C * ‖Real.exp ((σ - 1 - b) * x)‖ := by            rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _),              abs_of_pos (Real.exp_pos _), abs_of_pos hxpos]            calc              Real.exp ((σ - 1 / 2) * x) * (C * Real.exp (-(1 / 2 + b) * x))                  = C * (Real.exp ((σ - 1 / 2) * x) *                      Real.exp (-(1 / 2 + b) * x)) := by ring_nf              _ = C * Real.exp ((σ - 1 / 2) * x + (-(1 / 2 + b) * x)) := by                    rw [Real.exp_add]              _ = C * Real.exp ((σ - 1 - b) * x) := by ring_nf  have hbot : F =O[Filter.atBot] fun x : ℝ => Real.exp ((σ + b) * x) := by    rw [Asymptotics.isBigO_iff] at hbot_decay ⊢    obtain ⟨C, hC⟩ := hbot_decay    refine ⟨C, ?_⟩    filter_upwards [hC, Filter.eventually_lt_atBot (0 : ℝ)] with x hxC hxneg    rw [hshape]    calc      Real.exp ((σ - 1 / 2) * x) * ‖ψ x * exp ((x : ℂ) / 2)‖          ≤ Real.exp ((σ - 1 / 2) * x) *              (C * ‖Real.exp (-(1 / 2 + b) * |x|)‖) := by            exact mul_le_mul_of_nonneg_left hxC (Real.exp_nonneg _)      _ = C * ‖Real.exp ((σ + b) * x)‖ := by            rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.exp_pos _),              abs_of_pos (Real.exp_pos _), abs_of_neg hxneg]            calc              Real.exp ((σ - 1 / 2) * x) * (C * Real.exp (-(1 / 2 + b) * -x))                  = C * (Real.exp ((σ - 1 / 2) * x) *                      Real.exp (-(1 / 2 + b) * -x)) := by ring_nf              _ = C * Real.exp ((σ - 1 / 2) * x + (-(1 / 2 + b) * -x)) := by                    rw [Real.exp_add]              _ = C * Real.exp ((σ + b) * x) := by ring_nf  have htop_int : IntegrableAtFilter (fun x : ℝ => Real.exp ((σ - 1 - b) * x))      Filter.atTop volume := by    refine ⟨Set.Ioi 0, Filter.Ioi_mem_atTop 0, ?_⟩    convert exp_neg_integrableOn_Ioi 0 (show 0 < 1 + b - σ by linarith) using 1    ext x    ring_nf  have hbot_int : IntegrableAtFilter (fun x : ℝ => Real.exp ((σ + b) * x))      Filter.atBot volume := by    rw [← Filter.map_neg_atTop, measurableEmbedding_neg.integrableAtFilter_iff_comap]    have hvol : (volume : Measure ℝ).comap Neg.neg = volume := by      have he : ((MeasurableEquiv.neg ℝ).symm : ℝ → ℝ) = Neg.neg := rfl      rw [← he, (MeasurableEquiv.neg ℝ).comap_symm]      simp    rw [hvol, Function.comp_def]    refine ⟨Set.Ioi 0, Filter.Ioi_mem_atTop 0, ?_⟩    convert exp_neg_integrableOn_Ioi 0 (show 0 < σ + b by linarith) using 1    ext x    ring_nf  exact hF_loc.integrable_of_isBigO_atBot_atTop hbot hbot_int htop htop_int