Carlson's symmetric elliptic integral of the first kind

This file defines Carlson's symmetric elliptic integral of the first kind (DLMF 19.16.1)

R_F(x, y, z) = ½ ∫₀^∞ (t + x)^(-1/2) (t + y)^(-1/2) (t + z)^(-1/2) dt

for complex x, y, z, with the principal branch of each factor (t + x) ^ (-1/2 : ℂ), together with its degenerate case R_C(x, y) = R_F(x, y, y) (DLMF 19.2.17). Carlson's integrals are symmetric replacements for Legendre's incomplete elliptic integrals: every Legendre integral is a combination of them, and they are the input to the duplication algorithm for computing elliptic integrals.

The integral defining R_F converges absolutely when x, y, z lie in Complex.slitPlane ∪ {0} and at most one of them is 0. Since R_F is symmetric, the convergence theorem Complex.integrableOn_carlsonRF_integrand is stated with the possibly vanishing argument in the first position. The behavior of carlsonRF outside this domain is not characterized here; where the integrand is not integrable, carlsonRF is the totalized value 0 of the Bochner integral and carries no meaning.

Main results

• Complex.carlsonRF, Complex.carlsonRC — the integrals R_F and R_C.
• Complex.integrableOn_carlsonRF_integrand, Complex.integrableOn_carlsonRC_integrand — absolute convergence of the defining integrals of R_F and R_C.
• Complex.carlsonRF_comm_left, Complex.carlsonRF_comm_right — R_F is symmetric in its three arguments.
• Complex.carlsonRF_ofReal_mul — homogeneity of degree -1/2 under positive real scaling.
• Complex.carlsonRF_self, Complex.carlsonRC_self — the diagonal values R_F(x, x, x) = R_C(x, x) = x^(-1/2).
• Complex.carlsonRF_pos, Complex.carlsonRC_pos — R_F and R_C are positive real numbers at nonnegative real arguments, at most one of the symmetric ones zero.
• Complex.carlsonRC_eq_integral — the defining integral of R_C (DLMF 19.2.17).
• Complex.carlsonRC_ofReal_eq_arccos, Complex.carlsonRC_ofReal_eq_arcosh — the elementary evaluation of R_C at real arguments (DLMF 19.2.19, 19.2.20): R_C(x, y) = arccos √(x/y) / √(y - x) for 0 ≤ x < y, and R_C(x, y) = arcosh √(x/y) / √(x - y) for 0 < y < x.
• Complex.carlsonRF_ofReal_eq_integral — at nonnegative real arguments, R_F is the real integral ½ ∫₀^∞ (√(t + x) √(t + y) √(t + z))⁻¹ dt.

References

• NIST Digital Library of Mathematical Functions, §19.16 and §19.2(iv), https://dlmf.nist.gov/19.16.
• B. C. Carlson, Special Functions of Applied Mathematics, Academic Press, 1977, Chapter 9.
• 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) formalizes Carlson's book, including R_F, on top of Carlson's general R-function, a Dirichlet average over a simplex. This file instead works directly from the integral definition above and is not ported from it.

noncomputable def Complex.carlsonRF (x y z : ℂ) : ℂ

Carlson's symmetric elliptic integral of the first kind (DLMF 19.16.1): R_F(x, y, z) = ½ ∫₀^∞ (t + x)^(-1/2) (t + y)^(-1/2) (t + z)^(-1/2) dt, with principal complex powers of each factor.

The integral converges when x, y, z ∈ slitPlane ∪ {0} with at most one of them 0 (integrableOn_carlsonRF_integrand); its behavior outside this domain is not characterized here. Where the integrand is not integrable, the value is the totalized junk value 0.

noncomputable def Complex.carlsonRC (x y : ℂ) : ℂ

Carlson's degenerate integral R_C(x, y) = R_F(x, y, y) (DLMF 19.2.17). Its integral form ½ ∫₀^∞ (t + x)^(-1/2) (t + y)⁻¹ dt is carlsonRC_eq_integral.

theorem Complex.carlsonRF_def (x y z : ℂ) : x.carlsonRF y z = 1 / 2 * ∫ (t : ℝ) in Set.Ioi 0, (↑t + x) ^ (-(1 / 2)) * (↑t + y) ^ (-(1 / 2)) * (↑t + z) ^ (-(1 / 2))

The defining integral of carlsonRF.

theorem Complex.carlsonRC_def (x y : ℂ) : x.carlsonRC y = x.carlsonRF y y

carlsonRC is the degenerate case R_C(x, y) = R_F(x, y, y) of carlsonRF.

Convergence

theorem Complex.integrableOn_carlsonRF_integrand {x y z : ℂ} (hx : x ∈ slitPlane ∪ {0}) (hy : y ∈ slitPlane) (hz : z ∈ slitPlane) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (↑t + x) ^ (-(1 / 2)) * (↑t + y) ^ (-(1 / 2)) * (↑t + z) ^ (-(1 / 2))) (Set.Ioi 0) MeasureTheory.volume

Convergence of R_F. The integrand of carlsonRF x y z is integrable on (0, ∞) when x ∈ slitPlane ∪ {0} and y, z ∈ slitPlane. By symmetry of the integrand this covers every argument triple in slitPlane ∪ {0} with at most one zero entry.

theorem Complex.integrableOn_carlsonRC_integrand {x y : ℂ} (hx : x ∈ slitPlane ∪ {0}) (hy : y ∈ slitPlane) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (↑t + x) ^ (-(1 / 2)) * (↑t + y)⁻¹) (Set.Ioi 0) MeasureTheory.volume

Convergence of R_C. The integrand t ↦ (t + x)^(-1/2) (t + y)⁻¹ of carlsonRC_eq_integral is integrable on (0, ∞) when x ∈ slitPlane ∪ {0} and y ∈ slitPlane.

Symmetry and homogeneity

theorem Complex.carlsonRF_comm_left (x y z : ℂ) : x.carlsonRF y z = y.carlsonRF x z

R_F is symmetric in its first two arguments.

theorem Complex.carlsonRF_comm_right (x y z : ℂ) : x.carlsonRF y z = x.carlsonRF z y

R_F is symmetric in its last two arguments.

theorem Complex.carlsonRF_ofReal_mul {l : ℝ} (hl : 0 < l) (x y z : ℂ) : (↑l * x).carlsonRF (↑l * y) (↑l * z) = ↑l ^ (-(1 / 2)) * x.carlsonRF y z

Homogeneity of R_F. For real l > 0, R_F(l x, l y, l z) = l^(-1/2) R_F(x, y, z). No hypothesis on x, y, z is needed: the substitution t = l s identifies the two integrals whether or not they converge.

Diagonal values

theorem Complex.carlsonRC_eq_integral (x y : ℂ) : x.carlsonRC y = 1 / 2 * ∫ (t : ℝ) in Set.Ioi 0, (↑t + x) ^ (-(1 / 2)) * (↑t + y)⁻¹

The integral form of R_C (DLMF 19.2.17): R_C(x, y) = ½ ∫₀^∞ (t + x)^(-1/2) (t + y)⁻¹ dt.

@[simp]

theorem Complex.carlsonRF_self {x : ℂ} (hx : x ∈ slitPlane) : x.carlsonRF x x = x ^ (-(1 / 2))

The diagonal value of R_F: R_F(x, x, x) = x^(-1/2) for x in the slit plane.

@[simp]

theorem Complex.carlsonRC_self {x : ℂ} (hx : x ∈ slitPlane) : x.carlsonRC x = x ^ (-(1 / 2))

The diagonal value of R_C: R_C(x, x) = x^(-1/2) for x in the slit plane.

Real arguments

theorem Complex.carlsonRF_ofReal_eq_integral {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : (↑x).carlsonRF ↑y ↑z = ↑(1 / 2 * ∫ (t : ℝ) in Set.Ioi 0, (√(t + x) * √(t + y) * √(t + z))⁻¹)

R_F at nonnegative real arguments is a real integral: R_F(x, y, z) = ½ ∫₀^∞ (√(t + x) √(t + y) √(t + z))⁻¹ dt for real x, y, z ≥ 0. The two integrands agree on (0, ∞), so no convergence hypothesis is needed.

theorem Complex.carlsonRF_pos {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 < y) (hz : 0 < z) : 0 < (↑x).carlsonRF ↑y ↑z

R_F is positive at real arguments: for real x ≥ 0 and y, z > 0, R_F(x, y, z) is a positive real number (in the order ComplexOrder, so its imaginary part is 0). By symmetry, any one of the three arguments may be the one that vanishes.

theorem Complex.carlsonRC_pos {x y : ℝ} (hx : 0 ≤ x) (hy : 0 < y) : 0 < (↑x).carlsonRC ↑y

R_C is positive at real arguments: for real x ≥ 0 and y > 0, R_C(x, y) is a positive real number (in the order ComplexOrder, so its imaginary part is 0).

Elementary evaluation of R_C

theorem Complex.carlsonRC_ofReal_eq_arccos {x y : ℝ} (hx : 0 ≤ x) (hxy : x < y) : (↑x).carlsonRC ↑y = ↑(Real.arccos √(x / y) / √(y - x))

Elementary R_C, circular case (DLMF 19.2.19): for real 0 ≤ x < y, R_C(x, y) = arccos (√(x / y)) / √(y - x).

theorem Complex.carlsonRC_ofReal_eq_arcosh {x y : ℝ} (hy : 0 < y) (hyx : y < x) : (↑x).carlsonRC ↑y = ↑(Real.arcosh √(x / y) / √(x - y))

Elementary R_C, hyperbolic case (DLMF 19.2.20): for real 0 < y < x, R_C(x, y) = arcosh (√(x / y)) / √(x - y).