Legendre's relation

The complete elliptic integrals at complementary moduli satisfy E(k) K(k′) + E(k′) K(k) - K(k) K(k′) = π / 2, where k′ = √(1 - k²). This identity relates the first and second kinds and determines the second kind at the self-complementary modulus 1 / √2.

The left side has derivative zero on (0, 1). Its constant is evaluated at k → 0⁺: the derivatives of E and K at zero give E(k) - K(k) = o(k), while the elementary bound on K gives k K(k′) ≤ π / 2. Thus no logarithmic expansion at modulus one is needed.

References

• NIST Digital Library of Mathematical Functions, §19.7(i), equation 19.7.1, https://dlmf.nist.gov/19.7.E1.

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

Legendre's relation between the complete first and second elliptic integrals at complementary moduli (DLMF 19.7.1).

theorem TauCeti.Real.legendreEc_one_div_sqrt_two : legendreEc (1 / √2) = legendreK (1 / √2) / 2 + Real.pi / (4 * legendreK (1 / √2))

The complete second kind at the self-complementary modulus, expressed in terms of the complete first kind.