The imaginary-modulus transformation

The real integral with radicand 1 + c² sin² θ reduces to the complete integral legendreK at the real modulus c / √(1 + c²). This modulus always has square less than one, so the transformation evaluates a convergent integral without introducing a complex-valued extension of legendreK.

The proof uses symmetry and homogeneity of the AGM integral. This is the real-integral counterpart of Bastiaan J Braams' Carlson.legendreK_imaginary_modulus in Carlson/Elliptic/CompleteK.lean of bjbraams/lean-codes (Apache-2.0), which instead uses the symmetric integral R_K.

References

• NIST Digital Library of Mathematical Functions, §19.7.5, https://dlmf.nist.gov/19.7.E5.
• B. C. Carlson, Special Functions of Applied Mathematics, Academic Press, 1977, Exercise 6.10-5.

theorem TauCeti.Real.intervalIntegrable_one_add_mul_sin_sq_rpow_neg_half (c a b : ℝ) : IntervalIntegrable (fun (θ : ℝ) => (1 + c ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)) MeasureTheory.volume a b

The first-kind integral at an imaginary modulus, expressed entirely over the reals, is integrable on every bounded interval.

theorem TauCeti.Real.integral_one_add_mul_sin_sq_rpow_neg_half_eq_legendreK_div_sqrt (c : ℝ) : ∫ (θ : ℝ) in 0..Real.pi / 2, (1 + c ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) = legendreK (c / √(1 + c ^ 2)) / √(1 + c ^ 2)

Imaginary-modulus transformation (DLMF 19.7.5): the complete first-kind integral with radicand 1 + c² sin² θ is K(c / √(1 + c²)) / √(1 + c²). The integral converges for every real c.