AGM evaluation of the complete elliptic integral of the second kind

Landen's transformation gives a telescoping series for E / K along Mathlib's AGM sequence. The terms are weighted differences of squares of the arithmetic and geometric means. Since one AGM step turns this difference into a squared gap, Mathlib's geometric gap bound suffices to show that the remainder tends to zero.

References

• NIST DLMF §19.8(i), https://dlmf.nist.gov/19.8.
• B. C. Carlson, Special Functions of Applied Mathematics, §9.5, Exercises 3–4.
• Bastiaan J Braams, lean-codes, Carlson/Elliptic/AGMSecondKind.lean, commit 2b8cba1 (Apache-2.0), specifically Carlson.hasSum_agmA_zero and Carlson.carlsonRE_eq_agm, for the telescoping proof plan. Here we use the real Legendre Landen identities and Mathlib's NNReal.agmSequences, not Carlson's general R-function.

theorem TauCeti.Real.hasSum_agmSequences_legendreEc_div_legendreK {a b : NNReal} (hb : 0 < b) (hba : b ≤ a) : HasSum (fun (n : ℕ) => 2 ^ n * (↑(a.agmSequences b n).2 ^ 2 - ↑(a.agmSequences b n).1 ^ 2)) ((↑a ^ 2 + ↑b ^ 2) / 2 - ↑a ^ 2 * legendreEc √(1 - (↑b / ↑a) ^ 2) / legendreK √(1 - (↑b / ↑a) ^ 2))

The weighted squared differences of the AGM means sum to (a² + b²)/2 - a² E(√(1 - (b/a)²))/K(√(1 - (b/a)²)). Mathlib's index zero is already one AGM step. In particular, the series is summable.

theorem TauCeti.Real.hasSum_legendreEc_agm {k : ℝ} (hk : k ^ 2 < 1) : HasSum (fun (n : ℕ) => 2 ^ n * (↑(NNReal.agmSequences 1 (NNReal.sqrt (1 - k ^ 2).toNNReal) n).2 ^ 2 - ↑(NNReal.agmSequences 1 (NNReal.sqrt (1 - k ^ 2).toNNReal) n).1 ^ 2)) (1 - k ^ 2 / 2 - legendreEc k / legendreK k)

The squared AGM corrections form a convergent series evaluating E(k) / K(k). The sequence starts after one step: its difference of squares is cₙ₊₁² in the classical convention c₀ = k, cₙ₊₁ = (aₙ - gₙ) / 2.

theorem TauCeti.Real.legendreEc_eq_agm_tsum {k : ℝ} (hk : k ^ 2 < 1) : legendreEc k = legendreK k * (1 - k ^ 2 / 2 - ∑' (n : ℕ), 2 ^ n * (↑(NNReal.agmSequences 1 (NNReal.sqrt (1 - k ^ 2).toNNReal) n).2 ^ 2 - ↑(NNReal.agmSequences 1 (NNReal.sqrt (1 - k ^ 2).toNNReal) n).1 ^ 2))

AGM evaluation of the complete second kind (DLMF 19.8.6). The initial correction is k² / 2; the remaining corrections use Mathlib's AGM sequence, whose index zero is already one step after (1, √(1 - k²)).