Improper integrals

TheoremConditional convergence of the Dirichlet integral on \((1, \infty)\)#●ready to prove

The function \(x \mapsto \sin x / x\) is interval integrable on \([1, b]\) for every real \(b \ge 1\), the integrals \(\int_1^b \frac{\sin x}{x}\,dx\) converge to a real limit as \(b \to \infty\), and \(\sin x / x\) is not Lebesgue integrable on \((1, \infty)\).

public theorem_wanted dirichlet_integral_conditionally_convergent :
    (∀ b : ℝ, 1 ≤ b → IntervalIntegrable (fun x ↦ Real.sin x / x) volume 1 b) ∧
      (∃ L : ℝ, Tendsto (fun b ↦ ∫ x in (1 : ℝ)..b, Real.sin x / x) atTop (nhds L)) ∧
      ¬ Integrable (fun x ↦ Real.sin x / x) (volume.restrict (Ioi 1))

Sources

• W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 11, Exercise 15 (conditional convergence of the sine integral).

TheoremComparison test for improper integrals#●ready to prove

Let \(a \in \mathbb{R}\) and let \(f, g : \mathbb{R} \to \mathbb{R}\) be interval integrable on \([a, b]\) for every \(b \ge a\), with \(0 \le f(x) \le g(x)\) for all \(x \ge a\). If \(\int_a^b g(x)\,dx\) converges to a real limit as \(b \to \infty\), then \(\int_a^b f(x)\,dx\) also converges to a real limit as \(b \to \infty\).

public theorem_wanted improper_integral_comparison_test {f g : ℝ → ℝ} {a : ℝ}
    (hfg : ∀ x : ℝ, a ≤ x → 0 ≤ f x ∧ f x ≤ g x)
    (hfi : ∀ b : ℝ, a ≤ b → IntervalIntegrable f volume a b)
    (hgi : ∀ b : ℝ, a ≤ b → IntervalIntegrable g volume a b)
    (hg : ∃ L : ℝ, Tendsto (fun b ↦ ∫ x in a..b, g x) atTop (nhds L)) :
    ∃ L : ℝ, Tendsto (fun b ↦ ∫ x in a..b, f x) atTop (nhds L)

Sources

• https://mathbooks.unl.edu/Calculus/sec-5-11-comparison.html

TheoremLimit comparison test for improper integrals#●ready to prove

Let \(a, L \in \mathbb{R}\) with \(L \ne 0\), and let \(f, g : \mathbb{R} \to \mathbb{R}\) be interval integrable on \([a, b]\) for every \(b \ge a\), with \(f(x) > 0\) and \(g(x) > 0\) for all \(x \ge a\). If \(f(x) / g(x) \to L\) as \(x \to \infty\), then \(\int_a^b f(x)\,dx\) converges to a real limit as \(b \to \infty\) if and only if \(\int_a^b g(x)\,dx\) converges to a real limit as \(b \to \infty\).

public theorem_wanted improper_integral_limit_comparison_test
    {f g : ℝ → ℝ} {a : ℝ} {L : ℝ}
    (hf : ∀ x : ℝ, a ≤ x → 0 < f x)
    (hg : ∀ x : ℝ, a ≤ x → 0 < g x)
    (hfi : ∀ b : ℝ, a ≤ b → IntervalIntegrable f volume a b)
    (hgi : ∀ b : ℝ, a ≤ b → IntervalIntegrable g volume a b)
    (hL : L ≠ 0)
    (hlim : Tendsto (fun x ↦ f x / g x) atTop (nhds L)) :
    (∃ L' : ℝ, Tendsto (fun b ↦ ∫ x in a..b, f x) atTop (nhds L')) ↔
      ∃ L' : ℝ, Tendsto (fun b ↦ ∫ x in a..b, g x) atTop (nhds L')

Sources

• T. Apostol, Mathematical Analysis, 2nd ed., §10.23 (limit comparison test).

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.