Landen's transformation of the complete integral of the second kind

The ascending transformation sends k to 2√k / (1 + k) and expresses the second-kind integral at the new modulus in terms of E(k) and K(k). The descending transformation uses k₁ = (1 - k') / (1 + k'), where k' = √(1 - k²), and reads E(k) = (1 + k') E(k₁) - k' K(k).

Together with the first-kind transformations in Gauss, these identities allow simultaneous evaluation of the two complete elliptic integrals by arithmetic-geometric mean iteration. We obtain the second-kind transformation by differentiating the first-kind one in the modulus.

References

• NIST Digital Library of Mathematical Functions, §19.8(ii), https://dlmf.nist.gov/19.8.
• B. C. Carlson, Special Functions of Applied Mathematics, §9.5.

The corresponding Carlson-form transformation is Carlson.carlsonRE_sq_eq in Bastiaan J Braams' lean-codes, Carlson/Elliptic/LandenExercises.lean (commit 2b8cba1, Apache-2.0). The proof here uses the real Legendre modulus derivatives instead of Carlson's general quadratic transformation.

theorem TauCeti.Real.legendreEc_two_mul_sqrt_div_one_add {k : ℝ} (hk₀ : 0 ≤ k) (hk₁ : k < 1) : legendreEc (2 * √k / (1 + k)) = (2 * legendreEc k - (1 - k ^ 2) * legendreK k) / (1 + k)

Landen's transformation of the complete integral of the second kind, ascending form: for 0 ≤ k < 1, E(2√k / (1 + k)) = (2 E(k) - (1 - k²) K(k)) / (1 + k).

theorem TauCeti.Real.legendreEc_eq_one_add_mul_legendreEc {k : ℝ} (hk : k ^ 2 < 1) : legendreEc k = (1 + √(1 - k ^ 2)) * legendreEc ((1 - √(1 - k ^ 2)) / (1 + √(1 - k ^ 2))) - √(1 - k ^ 2) * legendreK k

Landen's transformation of the complete integral of the second kind, descending form: for k² < 1, with k' = √(1 - k²) and k₁ = (1 - k') / (1 + k'), E(k) = (1 + k') E(k₁) - k' K(k).