Continuity and derivatives of Legendre's integrals in the modulus

This file studies Legendre's elliptic integrals as functions of the modulus k.

• Continuity. On the nonsingular range k ^ 2 < 1, legendreF φ, legendrePi φ · α2 (for α2 < 1) and their complete values legendreK, legendrePic · α2 are continuous in k. The integrals of the second kind legendreE φ and legendreEc are continuous on all of ℝ, in particular at the singular moduli k = ±1.
• Derivatives (DLMF §19.4). For k ≠ 0 and k ^ 2 < 1, with k′² = 1 - k² and Δ = √(1 - k² sin² φ), ∂F/∂k = (E - k′² F) / (k k′²) - k sin φ cos φ / (k′² Δ) and ∂E/∂k = (E - F) / k. At φ = π/2 these become dK/dk = (E(k) - k′² K(k)) / (k k′²) and dE/dk = (E(k) - K(k)) / k. At k = 0 every derivative in the modulus vanishes.
• Legendre's differential equations. Differentiating the formulas for dK/dk and dE/dk once more shows that K and E are twice differentiable at every k ≠ 0 with k ^ 2 < 1, and that on all of k ^ 2 < 1 k k′² K′′ + (1 - 3k²) K′ - k K = 0 and k k′² E′′ + k′² E′ + k E = 0.

The integrals are differentiated under the integral sign (TauCeti.hasDerivAt_intervalIntegral_of_contDiffOn), using the smoothness TauCeti.contDiffOn_one_sub_sq_mul_sin_sq_rpow of the integrands. For the first kind, the integrand of the derivative is rewritten as a difference of the integrands of Π(φ, k, k²) and F(φ, k), and the evaluation TauCeti.Real.legendrePi_modulus_sq of Π(φ, k, k²) in terms of E(φ, k) supplies the integration by parts. For the second kind, the integrand of the derivative is already the difference of the integrands of E(φ, k) and F(φ, k), divided by k.

The first-derivative formulas are also the input to the proof by differentiation of Legendre's relation E(k) K(k′) + E(k′) K(k) - K(k) K(k′) = π/2 for 0 < k < 1, where k′ = √(1 - k²) is the complementary modulus.

Main statements

• TauCeti.Real.continuousOn_legendreK, TauCeti.Real.continuous_legendreEc and TauCeti.Real.continuousOn_legendrePic: continuity of the complete integrals in the modulus.
• TauCeti.Real.hasDerivAt_legendreF_modulus and TauCeti.Real.hasDerivAt_legendreE_modulus: the derivatives of the incomplete integrals in the modulus.
• TauCeti.Real.hasDerivAt_legendreK and TauCeti.Real.hasDerivAt_legendreEc: the derivatives of the complete integrals, with TauCeti.Real.hasDerivAt_legendreK_zero and TauCeti.Real.hasDerivAt_legendreEc_zero at k = 0.
• TauCeti.Real.hasDerivAt_deriv_legendreK and TauCeti.Real.hasDerivAt_deriv_legendreEc: the second derivatives of the complete integrals.
• TauCeti.Real.legendreK_differential_equation and TauCeti.Real.legendreEc_differential_equation: Legendre's differential equations.

References

• NIST Digital Library of Mathematical Functions, §19.4, https://dlmf.nist.gov/19.4.

Differentiation under the integral sign

theorem TauCeti.Real.hasDerivAt_integral_one_sub_sq_mul_sin_sq_rpow {k : ℝ} (hk : k ^ 2 < 1) (p a b : ℝ) : HasDerivAt (fun (k : ℝ) => ∫ (θ : ℝ) in a..b, (1 - k ^ 2 * Real.sin θ ^ 2) ^ p) (∫ (θ : ℝ) in a..b, -(2 * p * k * Real.sin θ ^ 2 * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (p - 1))) k

Differentiation in the modulus under the integral sign. For k ^ 2 < 1 and every real exponent p, the derivative in k of ∫ θ in a..b, (1 - k² sin² θ) ^ p is ∫ θ in a..b, -2 p k sin² θ (1 - k² sin² θ) ^ (p - 1). The cases p = -1/2 and p = 1/2 over [0, φ] are the integrals legendreF φ k and legendreE φ k.

Continuity in the modulus

theorem TauCeti.Real.continuousOn_legendreF_modulus (φ : ℝ) : ContinuousOn (legendreF φ) {k : ℝ | k ^ 2 < 1}

The incomplete integral of the first kind is continuous in the modulus on k ^ 2 < 1.

theorem TauCeti.Real.continuous_legendreE_modulus (φ : ℝ) : Continuous (legendreE φ)

The incomplete integral of the second kind is continuous in the modulus on all of ℝ.

theorem TauCeti.Real.continuousOn_legendrePi_modulus (φ : ℝ) {α2 : ℝ} (hα : α2 < 1) : ContinuousOn (fun (x : ℝ) => legendrePi φ x α2) {k : ℝ | k ^ 2 < 1}

For α2 < 1, the incomplete integral of the third kind is continuous in the modulus on k ^ 2 < 1.

theorem TauCeti.Real.continuousOn_legendreK : ContinuousOn legendreK {k : ℝ | k ^ 2 < 1}

Continuity of K in the modulus on k ^ 2 < 1.

theorem TauCeti.Real.continuous_legendreEc : Continuous legendreEc

Continuity of E in the modulus on all of ℝ, including the singular moduli ±1.

theorem TauCeti.Real.continuousOn_legendrePic {α2 : ℝ} (hα : α2 < 1) : ContinuousOn (fun (x : ℝ) => legendrePic x α2) {k : ℝ | k ^ 2 < 1}

Continuity of Π(·, α²) in the modulus on k ^ 2 < 1, for α2 < 1.

Derivatives in the modulus

theorem TauCeti.Real.hasDerivAt_legendreF_modulus_zero (φ : ℝ) : HasDerivAt (legendreF φ) 0 0

At k = 0 the incomplete integral of the first kind has derivative 0 in the modulus.

theorem TauCeti.Real.hasDerivAt_legendreE_modulus_zero (φ : ℝ) : HasDerivAt (legendreE φ) 0 0

At k = 0 the incomplete integral of the second kind has derivative 0 in the modulus.

theorem TauCeti.Real.hasDerivAt_legendreF_modulus (φ : ℝ) {k : ℝ} (hk : k ^ 2 < 1) : HasDerivAt (legendreF φ) ((legendreE φ k - (1 - k ^ 2) * legendreF φ k) / (k * (1 - k ^ 2)) - k * Real.sin φ * Real.cos φ / ((1 - k ^ 2) * √(1 - k ^ 2 * Real.sin φ ^ 2))) k

The derivative of F(φ, k) in the modulus (DLMF §19.4): for k ^ 2 < 1, ∂F/∂k = (E - (1 - k²) F) / (k (1 - k²)) - k sin φ cos φ / ((1 - k²) √(1 - k² sin² φ)). At k = 0 both terms vanish by the convention x / 0 = 0, in accordance with hasDerivAt_legendreF_modulus_zero.

theorem TauCeti.Real.hasDerivAt_legendreE_modulus (φ : ℝ) {k : ℝ} (hk : k ^ 2 < 1) : HasDerivAt (legendreE φ) ((legendreE φ k - legendreF φ k) / k) k

The derivative of E(φ, k) in the modulus (DLMF §19.4): for k ^ 2 < 1, ∂E/∂k = (E - F) / k. At k = 0 the right-hand side is 0 by the convention x / 0 = 0, in accordance with hasDerivAt_legendreE_modulus_zero.

theorem TauCeti.Real.hasDerivAt_legendreK {k : ℝ} (hk : k ^ 2 < 1) : HasDerivAt legendreK ((legendreEc k - (1 - k ^ 2) * legendreK k) / (k * (1 - k ^ 2))) k

The derivative of K (DLMF 19.4.1): for k ^ 2 < 1, K′(k) = (E(k) - (1 - k²) K(k)) / (k (1 - k²)). At k = 0 the right-hand side is 0 by the convention x / 0 = 0, in accordance with hasDerivAt_legendreK_zero.

theorem TauCeti.Real.hasDerivAt_legendreEc {k : ℝ} (hk : k ^ 2 < 1) : HasDerivAt legendreEc ((legendreEc k - legendreK k) / k) k

The derivative of E (DLMF 19.4.1): for k ^ 2 < 1, E′(k) = (E(k) - K(k)) / k. At k = 0 the right-hand side is 0 by the convention x / 0 = 0, in accordance with hasDerivAt_legendreEc_zero.

theorem TauCeti.Real.hasDerivAt_legendreK_zero : HasDerivAt legendreK 0 0

K′(0) = 0.

theorem TauCeti.Real.hasDerivAt_legendreEc_zero : HasDerivAt legendreEc 0 0

E′(0) = 0.

Second derivatives and Legendre's differential equations

theorem TauCeti.Real.deriv_legendreK {k : ℝ} (hk : k ^ 2 < 1) : deriv legendreK k = (legendreEc k - (1 - k ^ 2) * legendreK k) / (k * (1 - k ^ 2))

K′(k) = (E(k) - (1 - k²) K(k)) / (k (1 - k²)) for k ^ 2 < 1, in deriv form.

theorem TauCeti.Real.deriv_legendreEc {k : ℝ} (hk : k ^ 2 < 1) : deriv legendreEc k = (legendreEc k - legendreK k) / k

E′(k) = (E(k) - K(k)) / k for k ^ 2 < 1, in deriv form.

@[simp]

theorem TauCeti.Real.deriv_legendreK_zero : deriv legendreK 0 = 0

@[simp]

theorem TauCeti.Real.deriv_legendreEc_zero : deriv legendreEc 0 = 0

theorem TauCeti.Real.hasDerivAt_deriv_legendreK {k : ℝ} (hk₀ : k ≠ 0) (hk : k ^ 2 < 1) : HasDerivAt (deriv legendreK) (((1 - k ^ 2) * (1 - 2 * k ^ 2) * legendreK k - (1 - 3 * k ^ 2) * legendreEc k) / (k ^ 2 * (1 - k ^ 2) ^ 2)) k

The second derivative of K: for k ≠ 0 and k ^ 2 < 1, K′′(k) = ((1 - k²) (1 - 2k²) K(k) - (1 - 3k²) E(k)) / (k² (1 - k²)²). In particular K is twice differentiable at k.

theorem TauCeti.Real.hasDerivAt_deriv_legendreEc {k : ℝ} (hk₀ : k ≠ 0) (hk : k ^ 2 < 1) : HasDerivAt (deriv legendreEc) (-(legendreEc k - (1 - k ^ 2) * legendreK k) / (k ^ 2 * (1 - k ^ 2))) k

The second derivative of E (DLMF §19.4): for k ≠ 0 and k ^ 2 < 1, E′′(k) = -(E(k) - (1 - k²) K(k)) / (k² (1 - k²)), that is E′′(k) = -K′(k) / k. In particular E is twice differentiable at k.

theorem TauCeti.Real.legendreK_differential_equation {k : ℝ} (hk : k ^ 2 < 1) : k * (1 - k ^ 2) * deriv^[2] legendreK k + (1 - 3 * k ^ 2) * deriv legendreK k - k * legendreK k = 0

Legendre's differential equation for K (DLMF §19.4): for k ^ 2 < 1, k (1 - k²) K′′(k) + (1 - 3k²) K′(k) - k K(k) = 0. At k = 0 it reduces to K′(0) = 0.

theorem TauCeti.Real.legendreEc_differential_equation {k : ℝ} (hk : k ^ 2 < 1) : k * (1 - k ^ 2) * deriv^[2] legendreEc k + (1 - k ^ 2) * deriv legendreEc k + k * legendreEc k = 0

Legendre's differential equation for E (DLMF §19.4): for k ^ 2 < 1, k (1 - k²) E′′(k) + (1 - k²) E′(k) + k E(k) = 0. At k = 0 it reduces to E′(0) = 0.