A rational integral on the half-line

For a, c ≥ 0, not both zero,

∫_{y > 0} y² / ((y² + a²) (y² + c²)) dy = π / (2 (a + c)).

The integrand is the product of the two functions y / (y² + a²) and y / (y² + c²), and integrals of this shape arise when two Lorentzian line shapes are paired on the half-line. For a ≠ c partial fractions give the antiderivative (c arctan (y / c) - a arctan (y / a)) / (c² - a²), and for a = c > 0 the antiderivative is arctan (y / a) / (2 a) - y / (2 (y² + a²)). The integrand is nonnegative, so integrability comes for free from the limits of these antiderivatives at infinity.

Main results

• TauCeti.hasDerivAt_mul_arctan_div: a arctan (y / a) is an antiderivative of a² / (y² + a²) for every real a;
• TauCeti.integrableOn_sq_div_sq_add_sq_mul_sq_add_sq: the integrand is integrable on (0, ∞);
• TauCeti.integral_Ioi_sq_div_sq_add_sq_mul_sq_add_sq: the value of the integral.

theorem TauCeti.hasDerivAt_mul_arctan_div (a y : ℝ) : HasDerivAt (fun (y : ℝ) => a * Real.arctan (y / a)) (a ^ 2 / (y ^ 2 + a ^ 2)) y

a arctan (y / a) is an antiderivative of a² / (y² + a²), for every real a; both sides vanish when a = 0.

theorem TauCeti.tendsto_mul_arctan_div {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (y : ℝ) => a * Real.arctan (y / a)) Filter.atTop (nhds (a * (Real.pi / 2)))

For a ≥ 0, a arctan (y / a) tends to a π / 2 as y → ∞.

theorem TauCeti.integrableOn_sq_div_sq_add_sq_mul_sq_add_sq {a c : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hac : 0 < a + c) : MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ 2 / ((y ^ 2 + a ^ 2) * (y ^ 2 + c ^ 2))) (Set.Ioi 0) MeasureTheory.volume

The function y² / ((y² + a²) (y² + c²)) is integrable on (0, ∞) for a, c ≥ 0 not both zero.

theorem TauCeti.integral_Ioi_sq_div_sq_add_sq_mul_sq_add_sq {a c : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hac : 0 < a + c) : ∫ (y : ℝ) in Set.Ioi 0, y ^ 2 / ((y ^ 2 + a ^ 2) * (y ^ 2 + c ^ 2)) = Real.pi / (2 * (a + c))

For a, c ≥ 0 not both zero, ∫_{y > 0} y² / ((y² + a²) (y² + c²)) dy = π / (2 (a + c)).