Integrals with exponential decay at ∞

As easy special cases of general theorems in the library, we prove the following test for integrability:

• integrable_of_isBigO_exp_neg: If f is continuous on [a,∞), for some a ∈ ℝ, and there exists b > 0 such that f(x) = O(exp(-b x)) as x → ∞, then f is integrable on (a, ∞).
• integrableOn_exp_neg_smul_of_isBigO_exp: exponential decay dominates a locally integrable function of strictly smaller exponential order, with integrableOn_exp_neg_mul_of_isBigO_exp as the real-valued specialization.

theorem exp_neg_integrableOn_Ioi (a : ℝ) {b : ℝ} (h : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-b * x)) (Set.Ioi a) MeasureTheory.volume

exp (-b * x) is integrable on (a, ∞).

theorem integrable_of_isBigO_exp_neg {f : ℝ → ℝ} {a b : ℝ} (h0 : 0 < b) (hf : ContinuousOn f (Set.Ici a)) (ho : f =O[Filter.atTop] fun (x : ℝ) => Real.exp (-b * x)) : MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume

If f is continuous on [a, ∞), and is O (exp (-b * x)) at ∞ for some b > 0, then f is integrable on (a, ∞).

theorem integrableOn_exp_neg_smul_of_isBigO_exp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b c : ℝ} {f : ℝ → E} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ici c) MeasureTheory.volume) (hf : f =O[Filter.atTop] fun (x : ℝ) => Real.exp (a * x)) (hab : a < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-b * x) • f x) (Set.Ici c) MeasureTheory.volume

If f is locally integrable on [c, ∞) and f x = O(exp (a * x)) at ∞, then exp (-b * x) • f x is integrable on [c, ∞) for every a < b.

theorem integrableOn_exp_neg_mul_of_isBigO_exp {a b c : ℝ} {f : ℝ → ℝ} (hfc : MeasureTheory.LocallyIntegrableOn f (Set.Ici c) MeasureTheory.volume) (hf : f =O[Filter.atTop] fun (x : ℝ) => Real.exp (a * x)) (hab : a < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-b * x) * f x) (Set.Ici c) MeasureTheory.volume

Real-valued specialization of integrableOn_exp_neg_smul_of_isBigO_exp.