Trigonometric form of the AGM integral

For nonzero a and b, the integral of (a² cos² θ + b² sin² θ)^(-1/2) over a quarter period equals the integral of 1 / √((x² + a²)(x² + b²)) over the positive half-line. This identifies the trigonometric complete elliptic integral with the improper integral used to evaluate it by the arithmetic-geometric mean.

For b > 0, the substitution is θ = arctan (x / b); invariance under sign changes covers b < 0. The open-interval change of variables handles the endpoint at infinity without assigning a value to the integrand there.

References

• J. M. Borwein and P. B. Borwein, Pi and the AGM, Wiley, 1987, Chapter 1.

theorem TauCeti.continuous_rpow_cos_sq_add_sin_sq {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) : Continuous fun (θ : ℝ) => (a ^ 2 * Real.cos θ ^ 2 + b ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

The first-kind trigonometric integrand is continuous when both axes are nonzero.

theorem TauCeti.intervalIntegrable_rpow_cos_sq_add_sin_sq {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) (u v : ℝ) : IntervalIntegrable (fun (θ : ℝ) => (a ^ 2 * Real.cos θ ^ 2 + b ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)) MeasureTheory.volume u v

The trigonometric AGM integrand is integrable on every bounded interval.

theorem TauCeti.integral_rpow_cos_sq_add_sin_sq_eq_integral_Ioi {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) : ∫ (θ : ℝ) in 0..Real.pi / 2, (a ^ 2 * Real.cos θ ^ 2 + b ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) = ∫ (x : ℝ) in Set.Ioi 0, (√((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)))⁻¹

The trigonometric complete elliptic integral equals the improper AGM integral. Both sides converge for nonzero a and b.