Kadiri.kadiri_laplace_full_strip_exp_interval_moment_integrable_of_continuous

theorem kadiri_laplace_full_strip_exp_interval_moment_integrable_of_continuous    {ψ : ℝ → ℂ} (hψ : Continuous ψ) {b lo hi : ℝ}    (hlo : -b < lo) (hhi : hi < 1 + b) (hlohi : lo ≤ hi)    (hψ_decay : (fun x : ℝ ↦ ψ x * exp ((x : ℂ) / 2))        =O[Filter.cocompact ℝ] fun x : ℝ ↦ Real.exp (-(1/2 + b) * |x|)) :    Integrable (fun y : ℝ =>      ‖(y : ℂ)‖ * ‖ψ y‖ * (Real.exp (lo * y) + Real.exp (hi * y))) := by  let F : ℝ → ℝ := fun y =>    ‖(y : ℂ)‖ * ‖ψ y‖ * (Real.exp (lo * y) + Real.exp (hi * 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 =        ‖(x : ℂ)‖ *          (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *            ‖ψ x * exp ((x : ℂ) / 2)‖ := by    intro x    dsimp [F]    have hxre : ((x : ℂ) / 2).re = x / 2 := by norm_num    have hψexp : ‖ψ x * exp ((x : ℂ) / 2)‖ = ‖ψ x‖ * Real.exp (x / 2) := by      rw [norm_mul, Complex.norm_exp, hxre]    have hloexp :        Real.exp ((lo - 1 / 2) * x) * Real.exp (x / 2) = Real.exp (lo * x) := by      rw [← Real.exp_add]      ring_nf    have hhiexp :        Real.exp ((hi - 1 / 2) * x) * Real.exp (x / 2) = Real.exp (hi * x) := by      rw [← Real.exp_add]      ring_nf    rw [hψexp]    rw [← hloexp, ← hhiexp]    ring  let topBound : ℝ → ℝ := fun x =>    x * Real.exp (-(1 + b - lo) * x) +      x * Real.exp (-(1 + b - hi) * x)  let botBound : ℝ → ℝ := fun x =>    (-x) * Real.exp ((b + lo) * x) +      (-x) * Real.exp ((b + hi) * x)  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] topBound := 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    have hxnorm : ‖(x : ℂ)‖ = x := by      rw [Complex.norm_real, Real.norm_eq_abs, abs_of_pos hxpos]    have hdecay :        ‖Real.exp (-(1 / 2 + b) * |x|)‖ = Real.exp (-(1 / 2 + b) * x) := by      rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), abs_of_pos hxpos]    rw [hshape, hxnorm]    rw [Real.norm_eq_abs, abs_of_nonneg      (by positivity :        0 ≤ x * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *          ‖ψ x * exp ((x : ℂ) / 2)‖)]    calc      x * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *          ‖ψ x * exp ((x : ℂ) / 2)‖          ≤ x * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *              (C * ‖Real.exp (-(1 / 2 + b) * |x|)‖) := by            gcongr      _ = C * ‖topBound x‖ := by            rw [hdecay]            have hlo_prod :                Real.exp ((lo - 1 / 2) * x) * Real.exp (-(1 / 2 + b) * x) =                  Real.exp (-(1 + b - lo) * x) := by              rw [← Real.exp_add]              ring_nf            have hhi_prod :                Real.exp ((hi - 1 / 2) * x) * Real.exp (-(1 / 2 + b) * x) =                  Real.exp (-(1 + b - hi) * x) := by              rw [← Real.exp_add]              ring_nf            have htopNorm :                ‖topBound x‖ =                  x * Real.exp (-(1 + b - lo) * x) +                    x * Real.exp (-(1 + b - hi) * x) := by              dsimp [topBound]              rw [abs_of_nonneg]              · positivity            rw [htopNorm]            calc              x * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *                    (C * Real.exp (-(1 / 2 + b) * x))                  = C * (x * (Real.exp ((lo - 1 / 2) * x) *                        Real.exp (-(1 / 2 + b) * x)) +                      x * (Real.exp ((hi - 1 / 2) * x) *                        Real.exp (-(1 / 2 + b) * x))) := by ring              _ = C * (x * Real.exp (-(1 + b - lo) * x) +                    x * Real.exp (-(1 + b - hi) * x)) := by                    rw [hlo_prod, hhi_prod]  have hbot : F =O[Filter.atBot] botBound := 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    have hxnorm : ‖(x : ℂ)‖ = -x := by      rw [Complex.norm_real, Real.norm_eq_abs, abs_of_neg hxneg]    have hdecay :        ‖Real.exp (-(1 / 2 + b) * |x|)‖ =          Real.exp (-(1 / 2 + b) * (-x)) := by      rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), abs_of_neg hxneg]    have hxneg_nonneg : 0 ≤ -x := by linarith    have hsum_nonneg :        0 ≤ Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x) :=      add_nonneg (Real.exp_nonneg _) (Real.exp_nonneg _)    have hpref_nonneg :        0 ≤ (-x) * (Real.exp ((lo - 1 / 2) * x) +          Real.exp ((hi - 1 / 2) * x)) :=      mul_nonneg hxneg_nonneg hsum_nonneg    rw [hshape, hxnorm]    rw [Real.norm_eq_abs, abs_of_nonneg      (mul_nonneg hpref_nonneg (norm_nonneg _))]    calc      (-x) * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *          ‖ψ x * exp ((x : ℂ) / 2)‖          ≤ (-x) * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *              (C * ‖Real.exp (-(1 / 2 + b) * |x|)‖) := by            exact mul_le_mul_of_nonneg_left hxC hpref_nonneg      _ = C * ‖botBound x‖ := by            rw [hdecay]            have hlo_prod :                Real.exp ((lo - 1 / 2) * x) * Real.exp (-(1 / 2 + b) * (-x)) =                  Real.exp ((b + lo) * x) := by              rw [← Real.exp_add]              ring_nf            have hhi_prod :                Real.exp ((hi - 1 / 2) * x) * Real.exp (-(1 / 2 + b) * (-x)) =                  Real.exp ((b + hi) * x) := by              rw [← Real.exp_add]              ring_nf            have hbotNorm :                ‖botBound x‖ =                  (-x) * Real.exp ((b + lo) * x) +                    (-x) * Real.exp ((b + hi) * x) := by              dsimp [botBound]              rw [abs_of_nonneg]              · exact add_nonneg                  (mul_nonneg hxneg_nonneg (Real.exp_nonneg _))                  (mul_nonneg hxneg_nonneg (Real.exp_nonneg _))            rw [hbotNorm]            calc              (-x) * (Real.exp ((lo - 1 / 2) * x) + Real.exp ((hi - 1 / 2) * x)) *                    (C * Real.exp (-(1 / 2 + b) * (-x)))                  = C * ((-x) * (Real.exp ((lo - 1 / 2) * x) *                        Real.exp (-(1 / 2 + b) * (-x))) +                      (-x) * (Real.exp ((hi - 1 / 2) * x) *                        Real.exp (-(1 / 2 + b) * (-x)))) := by ring              _ = C * ((-x) * Real.exp ((b + lo) * x) +                    (-x) * Real.exp ((b + hi) * x)) := by                    rw [hlo_prod, hhi_prod]  have htop_int : IntegrableAtFilter topBound Filter.atTop volume := by    have h1 : IntegrableAtFilter        (fun x : ℝ => x ^ (1 : ℝ) * Real.exp (-(1 + b - lo) * x))        Filter.atTop volume := by      refine ⟨Set.Ioi 0, Filter.Ioi_mem_atTop 0, ?_⟩      simpa [Real.rpow_one] using        integrableOn_rpow_mul_exp_neg_mul_rpow          (s := 1) (p := 1) (b := 1 + b - lo) (by norm_num) (by norm_num)          (by linarith)    have h2 : IntegrableAtFilter        (fun x : ℝ => x ^ (1 : ℝ) * Real.exp (-(1 + b - hi) * x))        Filter.atTop volume := by      refine ⟨Set.Ioi 0, Filter.Ioi_mem_atTop 0, ?_⟩      simpa [Real.rpow_one] using        integrableOn_rpow_mul_exp_neg_mul_rpow          (s := 1) (p := 1) (b := 1 + b - hi) (by norm_num) (by norm_num)          (by linarith)    have hfun : topBound = fun x : ℝ =>        x ^ (1 : ℝ) * Real.exp (-(1 + b - lo) * x) +          x ^ (1 : ℝ) * Real.exp (-(1 + b - hi) * x) := by      funext x      simp [topBound, Real.rpow_one, mul_comm]    rw [hfun]    exact h1.add h2  have hbot_int : IntegrableAtFilter botBound 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]    have h1 : IntegrableAtFilter        (fun x : ℝ => x ^ (1 : ℝ) * Real.exp (-(b + lo) * x))        Filter.atTop volume := by      refine ⟨Set.Ioi 0, Filter.Ioi_mem_atTop 0, ?_⟩      simpa [Real.rpow_one] using        integrableOn_rpow_mul_exp_neg_mul_rpow          (s := 1) (p := 1) (b := b + lo) (by norm_num) (by norm_num)          (by linarith)    have h2 : IntegrableAtFilter        (fun x : ℝ => x ^ (1 : ℝ) * Real.exp (-(b + hi) * x))        Filter.atTop volume := by      refine ⟨Set.Ioi 0, Filter.Ioi_mem_atTop 0, ?_⟩      simpa [Real.rpow_one] using        integrableOn_rpow_mul_exp_neg_mul_rpow          (s := 1) (p := 1) (b := b + hi) (by norm_num) (by norm_num)          (by linarith)    have hfun : (fun x : ℝ => botBound (-x)) = fun x : ℝ =>        x ^ (1 : ℝ) * Real.exp (-(b + lo) * x) +          x ^ (1 : ℝ) * Real.exp (-(b + hi) * x) := by      funext x      simp [botBound, Real.rpow_one, mul_comm]      ring_nf    rw [hfun]    exact h1.add h2  exact hF_loc.integrable_of_isBigO_atBot_atTop hbot hbot_int htop htop_int