exp_neg_integrableOn_Ioi
theorem exp_neg_integrableOn_Ioi :
∀ (a : ℝ) {b : ℝ}, 0 < b → MeasureTheory.IntegrableOn (fun x => (-b * x).exp) (Set.Ioi a) MeasureTheory.volume := by
sorry
The theorem `exp_neg_integrableOn_Ioi` states that for all real numbers `a` and any positive real number `b`, the function `exp (-b * x)` is integrable over the interval `(a, ∞)`. In mathematical terms, for every real number `a` and any `b` greater than zero, the integral of `e^(-b * x)` from `a` to infinity is finite. This is determined using the Lebesgue measure (`MeasureTheory.volume`) to define integrability.
More concisely: For any real numbers `a` and positive `b`, the function `exp (-b * x)` is integrable with respect to Lebesgue measure over the interval `(a, ∞)`.
|
integrable_of_isBigO_exp_neg
theorem integrable_of_isBigO_exp_neg :
∀ {f : ℝ → ℝ} {a b : ℝ},
0 < b →
ContinuousOn f (Set.Ici a) →
(f =O[Filter.atTop] fun x => (-b * x).exp) → MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume
The theorem `integrable_of_isBigO_exp_neg` states that for a real-valued function `f` which is continuous on the interval `[a, ∞)` and is asymptotically bounded by `exp(-b * x)` as `x` goes to infinity, where `b` is a real number greater than 0, then `f` is integrable over the interval `(a, ∞)`. Here, integrability is defined in the sense of Lebesgue measure, meaning the integral of its absolute value is finite. The condition `f =O[Filter.atTop] fun x => (-b * x).exp` is a formal way of saying that `f` is of order `exp(-b * x)` at infinity.
More concisely: If a real-valued function `f` is continuous on `[a, ∞)` and has exponential decay `exp(-b * x)` as `x` approaches infinity, then `f` is integrable over `(a, ∞)` with respect to Lebesgue measure.
|