Elementary evaluations of Legendre's elliptic integrals

At the degenerate moduli and for special characteristics, Legendre's elliptic integrals reduce to elementary functions. This file proves those reductions.

• Modulus one. For |φ| < π / 2, F(φ, 1) = artanh (sin φ), and for |φ| ≤ π / 2, E(φ, 1) = sin φ; hence E(1) = 1. The complete integral of the first kind has no finite value at k = 1: K(k) → +∞ as k → 1⁻. At every fixed |φ| < π / 2, however, F(φ, k) → artanh (sin φ) as k → 1⁻.
• Third kind (DLMF 19.6.11, 19.6.13). For α2 < 1 and |φ| < π / 2, Π(φ, 0, α²) = arctan (√(1 - α²) tan φ) / √(1 - α²), hence Π(0, α²) = π / (2 √(1 - α²)); and for k ^ 2 < 1, Π(φ, k, k²) = (E(φ, k) - k² sin φ cos φ / √(1 - k² sin² φ)) / (1 - k²).

The evaluations at k = 0 of the first two kinds, and Π(φ, k, 0) = F(φ, k), live next to the definitions, in TauCeti/Analysis/SpecialFunctions/EllipticIntegral/Legendre.lean.

Main statements

• TauCeti.Real.legendreF_one_modulus, TauCeti.Real.legendreE_one_modulus and TauCeti.Real.legendreEc_one: the integrals at modulus 1.
• TauCeti.Real.tendsto_legendreK_nhdsLT_one: K(k) → +∞ as k → 1⁻.
• TauCeti.Real.legendrePi_zero_modulus, TauCeti.Real.legendrePic_zero_modulus and TauCeti.Real.legendrePi_modulus_sq: the elementary reductions of the third kind.

References

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

Modulus one

@[simp]

theorem TauCeti.Real.legendreF_one_modulus {φ : ℝ} (hφ : |φ| < Real.pi / 2) : legendreF φ 1 = Real.artanh (Real.sin φ)

The integral of the first kind at modulus one: for |φ| < π / 2, F(φ, 1) = ∫₀^φ sec θ dθ = artanh (sin φ).

theorem TauCeti.Real.tendsto_legendreF_nhdsLT_one {φ : ℝ} (hφ : |φ| < Real.pi / 2) : Filter.Tendsto (legendreF φ) (nhdsWithin 1 (Set.Iio 1)) (nhds (Real.artanh (Real.sin φ)))

At an amplitude strictly between -π/2 and π/2, the first-kind integral tends to artanh (sin φ) as the modulus tends to one from below.

@[simp]

theorem TauCeti.Real.legendreE_one_modulus {φ : ℝ} (hφ : |φ| ≤ Real.pi / 2) : legendreE φ 1 = Real.sin φ

The integral of the second kind at modulus one: for |φ| ≤ π / 2, E(φ, 1) = ∫₀^φ cos θ dθ = sin φ.

@[simp]

theorem TauCeti.Real.legendreEc_one : legendreEc 1 = 1

The complete integral of the second kind at modulus one: E(1) = 1.

theorem TauCeti.Real.tendsto_legendreK_nhdsLT_one : Filter.Tendsto legendreK (nhdsWithin 1 (Set.Iio 1)) Filter.atTop

Divergence of K at modulus one: the complete integral of the first kind tends to +∞ as the modulus tends to 1 from below.

Elementary reductions of the third kind

theorem TauCeti.Real.legendrePi_zero_modulus {φ α2 : ℝ} (hα : α2 < 1) (hφ : |φ| < Real.pi / 2) : legendrePi φ 0 α2 = Real.arctan (√(1 - α2) * Real.tan φ) / √(1 - α2)

The integral of the third kind at modulus zero (DLMF 19.6.11): for α2 < 1 and |φ| < π / 2, Π(φ, 0, α²) = arctan (√(1 - α²) tan φ) / √(1 - α²).

theorem TauCeti.Real.legendrePic_zero_modulus {α2 : ℝ} (hα : α2 < 1) : legendrePic 0 α2 = Real.pi / (2 * √(1 - α2))

The complete integral of the third kind at modulus zero: Π(0, α²) = π / (2 √(1 - α²)) for α2 < 1.

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

The integral of the third kind at characteristic k² (DLMF 19.6.13): for k ^ 2 < 1, Π(φ, k, k²) = (E(φ, k) - k² sin φ cos φ / √(1 - k² sin² φ)) / (1 - k²).

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

Π(k, k²) = E(k) / (1 - k²) for k ^ 2 < 1.