English
If f is continuous on [a, ∞) and f(x) = O(e^{−b x}) as x → ∞ for some b > 0, then f is integrable on (a, ∞).
Русский
Если f непрерывна на [a, ∞) и f(x) = O(e^{−b x}) при x→∞ для некоторого b > 0, то f интегрируема на (a, ∞).
LaTeX
$$$f\ \text{continuous on }[a,\infty) \land f=O\left(e^{-b x}\right)\text{ at }\infty\Rightarrow\int_a^{\infty} f(x)dx<\infty$$$
Lean4
/-- If `f` is continuous on `[a, ∞)`, and is `O (exp (-b * x))` at `∞` for some `b > 0`, then
`f` is integrable on `(a, ∞)`. -/
theorem integrable_of_isBigO_exp_neg {f : ℝ → ℝ} {a b : ℝ} (h0 : 0 < b) (hf : ContinuousOn f (Ici a))
(ho : f =O[atTop] fun x => exp (-b * x)) : IntegrableOn f (Ioi a) :=
integrableOn_Ici_iff_integrableOn_Ioi (by finiteness) |>.mp <|
(hf.locallyIntegrableOn measurableSet_Ici).integrableOn_of_isBigO_atTop ho
⟨Ioi b, Ioi_mem_atTop b, exp_neg_integrableOn_Ioi b h0⟩
