Definition 5.5.1. For a function f : [a, b) → ℝ that is Riemann integrable
on every [a, c] with c < b, we define ∫ a^b f as the limit
lim_{c → b⁻} ∫ a^c f when it exists. For f : [a, ∞) → ℝ, integrable on
every [a, c], we define ∫ a^∞ f as lim_{c → ∞} ∫ a^c f. The improper
integral converges if the relevant limit exists and diverges otherwise. The
analogous definitions for a left-hand endpoint are similar.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Improper integral over [a, ∞) converging to l.
Equations
- ImproperIntegralAtTop f a l = ((∀ (c : ℝ), MeasureTheory.IntegrableOn f (Set.Icc a c) MeasureTheory.volume) ∧ Filter.Tendsto (fun (c : ℝ) => ∫ (x : ℝ) in a..c, f x) Filter.atTop (nhds l))
Instances For
Convergence of an improper integral on [a, b).
Equations
- ImproperIntegralRightConverges f a b = ∃ (l : ℝ), ImproperIntegralRight f a b l
Instances For
Convergence of an improper integral on [a, ∞).
Equations
- ImproperIntegralAtTopConverges f a = ∃ (l : ℝ), ImproperIntegralAtTop f a l
Instances For
Helper: x ↦ 1 / x^p is integrable on any interval [1, c].
Proposition 5.5.2 (p-test for integrals). The improper integral
∫₁^∞ x^{-p} converges to 1 / (p - 1) for p > 1 and diverges for
0 < p ≤ 1. The improper integral ∫₀^1 x^{-p} converges to
1 / (1 - p) for 0 < p < 1 and diverges for p ≥ 1.
Proposition 5.5.3. If f : [a, ∞) → ℝ is Riemann integrable on every
[a, c] with c > a, then for any b > a the improper integral ∫ b^∞ f
converges if and only if ∫ a^∞ f converges, and in the convergent case
∫ a^∞ f = ∫ a..b, f + ∫ b^∞ f.
Proposition 5.5.3 (value identity). Under the same hypotheses as
improperIntegral_tail_convergence, if the improper integrals from a and
from b both converge, then the value from a splits as the sum of the
integral over [a, b] and the improper integral from b to ∞.
Proposition 5.5.4. Let f : [a, ∞) → ℝ be nonnegative and Riemann
integrable on every interval [a, b] with b > a.
(i) If the improper integral ∫ a^∞ f converges to l, then
l = sup {∫ a..x, f x | x ≥ a}.
(ii) For any sequence xₙ → ∞, the improper integral converges if and only if
lim_{n → ∞} ∫ a^{xₙ} f exists, and in that case the two limits agree.
Proposition 5.5.5 (comparison test for improper integrals). Let
f g : [a, ∞) → ℝ be Riemann integrable on every [a, b] with b > a and
assume |f x| ≤ g x for all x ≥ a.
(i) If ∫ a^∞ g converges, then ∫ a^∞ f converges and
|∫ a^∞ f| ≤ ∫ a^∞ g.
(ii) If ∫ a^∞ f diverges, then ∫ a^∞ g diverges.
Example 5.5.6. The improper integral
∫₀^∞ (sin (x^2) * (x + 2)) / (x^3 + 1) converges, for instance by comparing
its tail to 3 / x^2 on [1, ∞) and using the tail test.
Example 5.5.7. The improper integral ∫₂^∞ 2 / (x^2 - 1) converges (in
fact to log 3), but writing 2 / (x^2 - 1) = 1 / (x - 1) - 1 / (x + 1) does
not allow splitting the improper integral, since both pieces diverge
separately.
Definition 5.5.8. For a function f : (a, b) → ℝ that is Riemann
integrable on every closed subinterval [c, d] with a < c < d < b, the
improper integral ∫ a^b f is defined as the iterated limit
lim_{c → a⁺} lim_{d → b⁻} ∫_{c}^{d} f when this limit exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Definition 5.5.8 (whole line). If f : ℝ → ℝ is Riemann integrable on
every bounded interval [a, b], then the improper integral ∫_{-∞}^{∞} f is
defined as lim_{c → -∞} lim_{d → ∞} ∫_{c}^{d} f, when this limit exists.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Example 5.5.9. The improper integral of 1 / (1 + x^2) over the entire real
line converges and has value π, computed via the antiderivative x ↦ arctan x
and the limits at ±∞.
Helper: integrability on all closed intervals implies interval integrability.
Helper: convergence of base integrals at -∞ gives left partial limits.
Helper: base limits at ±∞ yield the two-variable limit.
Proposition 5.5.10. If f : ℝ → ℝ is Riemann integrable on every bounded
interval [a, b], then the iterated limits
lim_{a → -∞} lim_{b → ∞} ∫_{a}^{b} f and
lim_{b → ∞} lim_{a → -∞} ∫_{a}^{b} f converge together and have the same
value. If either iterated limit exists, then the improper integral over the
whole line converges to the same value and agrees with the limit of the
symmetric integrals ∫_{-a}^{a} f as a → ∞.
Example 5.5.11. For the function f(x) = x / |x| with f(0) = 0,
integrable on every bounded interval, the improper integral over the whole
line does not converge because for any fixed a < 0 the limit
lim_{b → ∞} ∫_{a}^{b} f diverges. However, the symmetric partial integrals
∫_{-a}^{a} f are all zero for a > 0, so
lim_{a → ∞} ∫_{-a}^{a} f = 0.
The primitive t ↦ ∫_0^t sinc has a finite limit at +∞.
Equations
- muA a = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (x : ℝ) => ENNReal.ofReal (Real.exp (-a * x))
Instances For
Example 5.5.12. The improper integral of the sinc function over the real
line converges and equals π, but the integral of its absolute value diverges,
so the convergence is not absolute.
Proposition 5.5.13 (integral test for series). If f : [k, ∞) → ℝ is
nonnegative and decreasing for some integer k, then the series
∑_{n = k}^{∞} f n converges if and only if the improper integral ∫ k^∞ f
converges. In the convergent case,
∫ k^∞ f ≤ ∑_{n = k}^{∞} f n ≤ f k + ∫ k^∞ f.
Telescoping sum for successive differences.
Example 5.5.14. Using the integral test with f x = 1 / x^2 gives explicit
bounds on the Basel series. For any integer k ≥ 1,
∑_{n=1}^{k-1} 1 / n^2 + 1 / k ≤ ∑_{n=1}^{∞} 1 / n^2 ≤ ∑_{n=1}^{k-1} 1 / n^2 + 1 / k + 1 / k^2. Numerically, taking k = 10
shows the sum lies between 1.6397… and 1.6497…, while the exact value is
π^2 / 6 ≈ 1.6449….