Gauss's AGM formula for the complete elliptic integral of the first kind

Writing 1 - k² sin² θ = cos² θ + k'² sin² θ with the complementary modulus k' = √(1 - k²) identifies legendreK k with the trigonometric AGM integral of the axes 1 and k'. The evaluation of that integral by the arithmetic-geometric mean then gives Gauss's theorem

legendreK k = π / (2 * agm 1 √(1 - k²)) for k ^ 2 < 1.

Rescaling the axes, agmIntegral_eq_legendreK_div expresses the AGM integral of any axes 0 < a ≤ b as K(k) / b with k = √(1 - (a / b)²).

Since the AGM is unchanged by replacing its arguments with their geometric and arithmetic means, the same identification gives Landen's transformation of K (DLMF 19.8.12):

• legendreK_two_mul_sqrt_div_one_add, the ascending form: for 0 ≤ k < 1, legendreK (2 √k / (1 + k)) = (1 + k) * legendreK k;
• legendreK_eq_one_add_mul_legendreK, the descending form: for k ^ 2 < 1, with k' = √(1 - k²) and k₁ = (1 - k') / (1 + k'), legendreK k = (1 + k₁) * legendreK k₁.

References

• NIST Digital Library of Mathematical Functions, §19.8, https://dlmf.nist.gov/19.8.
• J. M. Borwein and P. B. Borwein, Pi and the AGM, Wiley, 1987, Chapter 1.

theorem TauCeti.Real.legendreK_eq_agmIntegral {k : ℝ} (hk : k ^ 2 < 1) : legendreK k = agmIntegral 1 √(1 - k ^ 2)

For k ^ 2 < 1, the complete elliptic integral of the first kind is the AGM integral of the axes 1 and the complementary modulus √(1 - k²).

theorem TauCeti.Real.legendreK_eq_pi_div_two_mul_agm {k : ℝ} (hk : k ^ 2 < 1) : legendreK k = Real.pi / (2 * ↑(NNReal.agm 1 (√(1 - k ^ 2)).toNNReal))

Gauss's theorem: for k ^ 2 < 1, the complete elliptic integral of the first kind is K(k) = π / (2 M(1, k')), where M is the arithmetic-geometric mean and k' = √(1 - k²) is the complementary modulus.

theorem TauCeti.Real.agmIntegral_eq_legendreK_div {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : agmIntegral a b = legendreK √(1 - (a / b) ^ 2) / b

For axes 0 < a ≤ b, the AGM integral is K(k) / b, where the modulus k = √(1 - (a / b)²) has complementary modulus a / b.

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

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

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

Landen's transformation of the complete integral of the first kind, descending form (DLMF 19.8.12): for k ^ 2 < 1, with k' = √(1 - k²) and k₁ = (1 - k') / (1 + k'), we have K(k) = (1 + k₁) K(k₁).