The duplication theorem for Carlson's R_F

This file proves the duplication theorem for Carlson's symmetric integral of the first kind (DLMF 19.26.18) at nonnegative real arguments: with λ = √x √y + √y √z + √z √x,

R_F(x, y, z) = R_F((x + λ)/4, (y + λ)/4, (z + λ)/4).

Iterating it drives the three arguments together towards a common value, where R_F is given by its diagonal value R_F(x, x, x) = x^(-1/2); this is the basis of Carlson's duplication algorithm for computing elliptic integrals.

Main results

• Complex.carlsonRF_ofReal_duplication — the duplication theorem for R_F at nonnegative real arguments.

Implementation notes

The proof is a change of variables in the defining integral. Write a = √(t + x), b = √(t + y), c = √(t + z) and λ(t) = ab + bc + ca, so that λ = λ(0). The substitution u = (t + λ(t) - λ)/4 maps (0, ∞) increasingly onto itself, and it satisfies u + (x + λ)/4 = (a + b)(a + c)/4 together with its two cyclic companions. Since du/dt · abc = (a + b)(b + c)(c + a)/8, it carries the integrand of the right-hand side to that of the left-hand side. The identity holds as an equality of Bochner integrals, so no convergence hypothesis is needed.

References

• NIST Digital Library of Mathematical Functions, §19.26(ii), https://dlmf.nist.gov/19.26.
• B. C. Carlson, Computing elliptic integrals by duplication, Numer. Math. 33 (1979), 1–16.
• B. C. Carlson, Numerical computation of real or complex elliptic integrals, Numer. Algorithms 10 (1995), 13–26.

B. Braams' lean-codes (https://github.com/bjbraams/lean-codes) also proves the duplication theorem, on top of Carlson's general R-function. This file works directly from the integral definition of Complex.carlsonRF and is not ported from it.

theorem Complex.carlsonRF_ofReal_duplication {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : have l := √x * √y + √y * √z + √z * √x; (↑x).carlsonRF ↑y ↑z = (↑((x + l) / 4)).carlsonRF ↑((y + l) / 4) ↑((z + l) / 4)

The duplication theorem for R_F (DLMF 19.26.18) at nonnegative real arguments: for real x, y, z ≥ 0, with λ = √x √y + √y √z + √z √x, R_F(x, y, z) = R_F((x + λ)/4, (y + λ)/4, (z + λ)/4).

No hypothesis beyond nonnegativity is needed. When two of x, y, z vanish, the defining integrals on both sides diverge and the identity is between the totalized values 0.