Legendre's elliptic integrals

This file defines Legendre's incomplete elliptic integrals of the first, second and third kinds (DLMF 19.2.4, 19.2.5, 19.2.7), as functions of a real amplitude φ, a real modulus k and a real characteristic α2 (written α² in prose; it may be negative):

• TauCeti.Real.legendreF φ k = ∫ θ in 0..φ, (1 - k ^ 2 * sin θ ^ 2) ^ (-1 / 2);
• TauCeti.Real.legendreE φ k = ∫ θ in 0..φ, (1 - k ^ 2 * sin θ ^ 2) ^ (1 / 2);
• TauCeti.Real.legendrePi φ k α2 is the integral over [0, φ] of (1 - α2 * sin θ ^ 2)⁻¹ * (1 - k ^ 2 * sin θ ^ 2) ^ (-1 / 2);

together with the complete integrals legendreK k, legendreEc k and legendrePic k α2, their values at φ = π / 2. The powers are Real.rpow. These are total functions of their real arguments; their values are meaningful for k ^ 2 < 1 and α2 < 1, under which every integrand is continuous and bounded between two positive constants, and every theorem below states the hypotheses it needs. The integral of the second kind needs no hypothesis at all for the bounds on its integrand, nor for continuity, differentiability, positivity and quasi-periodicity in φ, and it is strictly increasing in φ for k ^ 2 ≤ 1.

We prove the basic theory in the amplitude:

• the integrands are continuous, positive, bounded by explicit constants and interval integrable;
• the fundamental theorem of calculus HasDerivAt (legendreF · k) ((1 - k ^ 2 * sin φ ^ 2) ^ (-1 / 2)) φ and its analogues, so the three integrals are continuous and strictly increasing in φ, and positive for φ > 0; in particular the complete integrals are positive;
• the integrals are odd in φ and even in k;
• quasi-periodicity: legendreF (φ + n * π) k = legendreF φ k + 2 * n * legendreK k for integers n, and likewise for the other two kinds; in particular the Lebesgue integral of the integrand of the first kind over (0, π) is 2 * legendreK k;
• legendreFOrderIso: for k ^ 2 < 1, the map φ ↦ legendreF φ k is an order isomorphism of ℝ, whose inverse is the Jacobi amplitude;
• the degenerate modulus k = 0: legendreF φ 0 = legendreE φ 0 = φ, and legendreK 0 = legendreEc 0 = π / 2;
• the characteristic α2 = 0: legendrePi φ k 0 = legendreF φ k.
• on [0, π / 2], the integrals of the second and third kinds in terms of the first (legendreE_eq_legendreF_sub, legendrePi_eq_legendreF_add).

The conventions (modulus rather than parameter, argument order (φ, k) and (φ, k, α2)) are those of DLMF Chapter 19 and of B. Braams' lean-codes formalization of B. C. Carlson's Special Functions of Applied Mathematics, so that the two developments stay interoperable.

References

• NIST Digital Library of Mathematical Functions, §19.2, https://dlmf.nist.gov/19.2.
• B. C. Carlson, Special Functions of Applied Mathematics, Academic Press, 1977, Chapter 9.

Definitions

noncomputable def TauCeti.Real.legendreF (φ k : ℝ) : ℝ

Legendre's incomplete elliptic integral of the first kind (DLMF 19.2.4), F(φ, k) = ∫₀^φ (1 - k² sin² θ)^(-1/2) dθ, with amplitude φ and modulus k. It is meaningful for k ^ 2 < 1.

noncomputable def TauCeti.Real.legendreE (φ k : ℝ) : ℝ

Legendre's incomplete elliptic integral of the second kind (DLMF 19.2.5), E(φ, k) = ∫₀^φ (1 - k² sin² θ)^(1/2) dθ, with amplitude φ and modulus k. It is meaningful for k ^ 2 ≤ 1.

noncomputable def TauCeti.Real.legendrePi (φ k α2 : ℝ) : ℝ

Legendre's incomplete elliptic integral of the third kind (DLMF 19.2.7), Π(φ, k, α²) = ∫₀^φ (1 - α² sin² θ)⁻¹ (1 - k² sin² θ)^(-1/2) dθ, with amplitude φ, modulus k and characteristic α2, which may be negative. It is meaningful for k ^ 2 < 1 and α2 < 1.

noncomputable def TauCeti.Real.legendreK (k : ℝ) : ℝ

The complete elliptic integral of the first kind, K(k) = F(π/2, k).

noncomputable def TauCeti.Real.legendreEc (k : ℝ) : ℝ

The complete elliptic integral of the second kind, E(k) = E(π/2, k).

noncomputable def TauCeti.Real.legendrePic (k α2 : ℝ) : ℝ

The complete elliptic integral of the third kind, Π(k, α²) = Π(π/2, k, α²).

theorem TauCeti.Real.legendreF_def (φ k : ℝ) : legendreF φ k = ∫ (θ : ℝ) in 0..φ, (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

theorem TauCeti.Real.legendreE_def (φ k : ℝ) : legendreE φ k = ∫ (θ : ℝ) in 0..φ, (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2)

theorem TauCeti.Real.legendrePi_def (φ k α2 : ℝ) : legendrePi φ k α2 = ∫ (θ : ℝ) in 0..φ, (1 - α2 * Real.sin θ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

theorem TauCeti.Real.legendreK_def (k : ℝ) : legendreK k = legendreF (Real.pi / 2) k

theorem TauCeti.Real.legendreEc_def (k : ℝ) : legendreEc k = legendreE (Real.pi / 2) k

theorem TauCeti.Real.legendrePic_def (k α2 : ℝ) : legendrePic k α2 = legendrePi (Real.pi / 2) k α2

The integrands

The first kind

theorem TauCeti.Real.continuous_legendreF_integrand {k : ℝ} (hk : k ^ 2 < 1) : Continuous fun (θ : ℝ) => (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

theorem TauCeti.Real.one_le_legendreF_integrand {k : ℝ} (hk : k ^ 2 < 1) (θ : ℝ) : 1 ≤ (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

The integrand of the first kind is at least 1.

theorem TauCeti.Real.legendreF_integrand_le {k : ℝ} (hk : k ^ 2 < 1) (θ : ℝ) : (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) ≤ (1 - k ^ 2) ^ (-1 / 2)

The integrand of the first kind is at most (1 - k²)^(-1/2).

theorem TauCeti.Real.legendreF_integrand_eq_inv_sqrt (k θ : ℝ) : (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) = (√(1 - k ^ 2 * Real.sin θ ^ 2))⁻¹

The integrand of the first kind is the inverse square root of 1 - k² sin² θ.

theorem TauCeti.Real.intervalIntegrable_legendreF_integrand {k : ℝ} (hk : k ^ 2 < 1) (a b : ℝ) : IntervalIntegrable (fun (θ : ℝ) => (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)) MeasureTheory.volume a b

theorem TauCeti.Real.continuousOn_legendreF_integrand {φ k : ℝ} (hφ0 : 0 ≤ φ) (hφ : φ ≤ Real.pi / 2) (hk : k ^ 2 * Real.sin φ ^ 2 < 1) : ContinuousOn (fun (θ : ℝ) => (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)) (Set.uIcc 0 φ)

The integrand of the first kind is continuous on [0, φ] when 0 ≤ φ ≤ π / 2 and k² sin² φ < 1.

The second kind

theorem TauCeti.Real.continuous_legendreE_integrand (k : ℝ) : Continuous fun (θ : ℝ) => (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2)

The integrand of the second kind is continuous for every modulus.

theorem TauCeti.Real.legendreE_integrand_pos {k : ℝ} (hk : k ^ 2 < 1) (θ : ℝ) : 0 < (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2)

theorem TauCeti.Real.legendreE_integrand_nonneg (k θ : ℝ) : 0 ≤ (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2)

The integrand of the second kind is nonnegative, for every modulus.

theorem TauCeti.Real.le_legendreE_integrand (k θ : ℝ) : (1 - k ^ 2) ^ (1 / 2) ≤ (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2)

The integrand of the second kind is at least (1 - k²)^(1/2), for every modulus.

theorem TauCeti.Real.legendreE_integrand_le_one (k θ : ℝ) : (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2) ≤ 1

The integrand of the second kind is at most 1, for every modulus.

theorem TauCeti.Real.intervalIntegrable_legendreE_integrand (k a b : ℝ) : IntervalIntegrable (fun (θ : ℝ) => (1 - k ^ 2 * Real.sin θ ^ 2) ^ (1 / 2)) MeasureTheory.volume a b

The third kind

theorem TauCeti.Real.continuous_legendrePi_integrand {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) : Continuous fun (θ : ℝ) => (1 - α2 * Real.sin θ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

theorem TauCeti.Real.inv_max_le_legendrePi_integrand {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (θ : ℝ) : (max 1 (1 - α2))⁻¹ ≤ (1 - α2 * Real.sin θ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

The integrand of the third kind is at least (max 1 (1 - α²))⁻¹.

theorem TauCeti.Real.legendrePi_integrand_pos {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (θ : ℝ) : 0 < (1 - α2 * Real.sin θ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)

theorem TauCeti.Real.legendrePi_integrand_le {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (θ : ℝ) : (1 - α2 * Real.sin θ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) ≤ (min 1 (1 - α2))⁻¹ * (1 - k ^ 2) ^ (-1 / 2)

The integrand of the third kind is at most (min 1 (1 - α²))⁻¹ (1 - k²)^(-1/2).

theorem TauCeti.Real.intervalIntegrable_legendrePi_integrand {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (a b : ℝ) : IntervalIntegrable (fun (θ : ℝ) => (1 - α2 * Real.sin θ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)) MeasureTheory.volume a b

The integral of the first kind

@[simp]

theorem TauCeti.Real.legendreF_zero (k : ℝ) : legendreF 0 k = 0

theorem TauCeti.Real.hasDerivAt_legendreF {k : ℝ} (hk : k ^ 2 < 1) (φ : ℝ) : HasDerivAt (fun (x : ℝ) => legendreF x k) ((1 - k ^ 2 * Real.sin φ ^ 2) ^ (-1 / 2)) φ

The integral of the first kind is a primitive of its integrand.

theorem TauCeti.Real.continuous_legendreF {k : ℝ} (hk : k ^ 2 < 1) : Continuous fun (x : ℝ) => legendreF x k

For k ^ 2 < 1, F(φ, k) is continuous in the amplitude φ.

theorem TauCeti.Real.strictMono_legendreF {k : ℝ} (hk : k ^ 2 < 1) : StrictMono fun (x : ℝ) => legendreF x k

For k ^ 2 < 1, F(φ, k) is strictly increasing in the amplitude φ.

theorem TauCeti.Real.legendreF_pos {φ k : ℝ} (hk : k ^ 2 < 1) (hφ : 0 < φ) : 0 < legendreF φ k

For k ^ 2 < 1, F(φ, k) is positive for positive amplitude φ.

theorem TauCeti.Real.self_le_legendreF {φ k : ℝ} (hk : k ^ 2 < 1) (hφ : 0 ≤ φ) : φ ≤ legendreF φ k

For nonnegative amplitude, φ ≤ F(φ, k), since the integrand is at least 1.

theorem TauCeti.Real.legendreF_le_div_sqrt {φ k : ℝ} (hk : k ^ 2 < 1) (hφ : 0 ≤ φ) : legendreF φ k ≤ φ / √(1 - k ^ 2)

An elementary upper bound for the incomplete elliptic integral of the first kind at nonnegative amplitude, valid for either sign of the modulus.

@[simp]

theorem TauCeti.Real.legendreF_neg (φ k : ℝ) : legendreF (-φ) k = -legendreF φ k

F(φ, k) is odd in the amplitude.

@[simp]

theorem TauCeti.Real.legendreF_neg_modulus (φ k : ℝ) : legendreF φ (-k) = legendreF φ k

F(φ, k) is even in the modulus.

theorem TauCeti.Real.legendreF_le_self {φ k : ℝ} (hk : k ^ 2 < 1) (hφ : φ ≤ 0) : legendreF φ k ≤ φ

For nonpositive amplitude, F(φ, k) ≤ φ.

theorem TauCeti.Real.legendreF_add_int_mul_pi {k : ℝ} (hk : k ^ 2 < 1) (φ : ℝ) (n : ℤ) : legendreF (φ + ↑n * Real.pi) k = legendreF φ k + 2 * ↑n * legendreK k

Quasi-periodicity of F: F(φ + nπ, k) = F(φ, k) + 2 n K(k) for every integer n.

theorem TauCeti.Real.legendreF_add_pi {k : ℝ} (hk : k ^ 2 < 1) (φ : ℝ) : legendreF (φ + Real.pi) k = legendreF φ k + 2 * legendreK k

theorem TauCeti.Real.legendreF_int_mul_pi {k : ℝ} (hk : k ^ 2 < 1) (n : ℤ) : legendreF (↑n * Real.pi) k = 2 * ↑n * legendreK k

theorem TauCeti.Real.lintegral_Ioo_zero_pi_legendreF_integrand {k : ℝ} (hk : k ^ 2 < 1) : ∫⁻ (θ : ℝ) in Set.Ioo 0 Real.pi, ENNReal.ofReal ((1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2)) = ENNReal.ofReal (2 * legendreK k)

For k ^ 2 < 1, the Lebesgue integral of the integrand of the first kind over (0, π) is F(π, k) = 2 K(k), as an identity in ℝ≥0∞.

theorem TauCeti.Real.tendsto_legendreF_atTop {k : ℝ} (hk : k ^ 2 < 1) : Filter.Tendsto (fun (x : ℝ) => legendreF x k) Filter.atTop Filter.atTop

For k ^ 2 < 1, F(φ, k) tends to +∞ as the amplitude φ tends to +∞.

theorem TauCeti.Real.tendsto_legendreF_atBot {k : ℝ} (hk : k ^ 2 < 1) : Filter.Tendsto (fun (x : ℝ) => legendreF x k) Filter.atBot Filter.atBot

For k ^ 2 < 1, F(φ, k) tends to -∞ as the amplitude φ tends to -∞.

noncomputable def TauCeti.Real.legendreFOrderIso {k : ℝ} (hk : k ^ 2 < 1) : ℝ ≃o ℝ

For k ^ 2 < 1, the integral of the first kind φ ↦ F(φ, k) as an order isomorphism of ℝ. Its inverse is the Jacobi amplitude u ↦ am(u, k).

@[simp]

theorem TauCeti.Real.coe_legendreFOrderIso {k : ℝ} (hk : k ^ 2 < 1) : ⇑(legendreFOrderIso hk) = fun (x : ℝ) => legendreF x k

@[simp]

theorem TauCeti.Real.legendreF_zero_modulus (φ : ℝ) : legendreF φ 0 = φ

At modulus 0 the integral of the first kind is the identity: F(φ, 0) = φ.

theorem TauCeti.Real.legendreK_pos {k : ℝ} (hk : k ^ 2 < 1) : 0 < legendreK k

For k ^ 2 < 1, the complete integral of the first kind K(k) is positive.

theorem TauCeti.Real.legendreK_le_pi_div_two_div_sqrt {k : ℝ} (hk : k ^ 2 < 1) : legendreK k ≤ Real.pi / 2 / √(1 - k ^ 2)

An elementary upper bound for the complete elliptic integral of the first kind, valid for either sign of the modulus.

@[simp]

theorem TauCeti.Real.legendreK_neg (k : ℝ) : legendreK (-k) = legendreK k

@[simp]

theorem TauCeti.Real.legendreK_abs (k : ℝ) : legendreK |k| = legendreK k

Taking the absolute value of the modulus leaves the complete first kind unchanged.

@[simp]

theorem TauCeti.Real.legendreK_zero : legendreK 0 = Real.pi / 2

The integral of the second kind

@[simp]

theorem TauCeti.Real.legendreE_zero (k : ℝ) : legendreE 0 k = 0

theorem TauCeti.Real.hasDerivAt_legendreE (k φ : ℝ) : HasDerivAt (fun (x : ℝ) => legendreE x k) ((1 - k ^ 2 * Real.sin φ ^ 2) ^ (1 / 2)) φ

The integral of the second kind is a primitive of its integrand, for every modulus.

theorem TauCeti.Real.continuous_legendreE (k : ℝ) : Continuous fun (x : ℝ) => legendreE x k

For every modulus k, E(φ, k) is continuous in the amplitude φ.

theorem TauCeti.Real.strictMono_legendreE {k : ℝ} (hk : k ^ 2 ≤ 1) : StrictMono fun (x : ℝ) => legendreE x k

For k ^ 2 ≤ 1, E(φ, k) is strictly increasing in the amplitude φ.

theorem TauCeti.Real.legendreE_pos {φ k : ℝ} (hφ : 0 < φ) : 0 < legendreE φ k

For every modulus k, E(φ, k) is positive for positive amplitude φ.

@[simp]

theorem TauCeti.Real.legendreE_neg (φ k : ℝ) : legendreE (-φ) k = -legendreE φ k

E(φ, k) is odd in the amplitude.

@[simp]

theorem TauCeti.Real.legendreE_neg_modulus (φ k : ℝ) : legendreE φ (-k) = legendreE φ k

E(φ, k) is even in the modulus.

theorem TauCeti.Real.legendreE_add_int_mul_pi (φ k : ℝ) (n : ℤ) : legendreE (φ + ↑n * Real.pi) k = legendreE φ k + 2 * ↑n * legendreEc k

Quasi-periodicity of E: E(φ + nπ, k) = E(φ, k) + 2 n E(k) for every integer n and every modulus.

theorem TauCeti.Real.legendreE_add_pi (φ k : ℝ) : legendreE (φ + Real.pi) k = legendreE φ k + 2 * legendreEc k

theorem TauCeti.Real.legendreE_int_mul_pi (k : ℝ) (n : ℤ) : legendreE (↑n * Real.pi) k = 2 * ↑n * legendreEc k

@[simp]

theorem TauCeti.Real.legendreE_zero_modulus (φ : ℝ) : legendreE φ 0 = φ

At modulus 0 the integral of the second kind is the identity: E(φ, 0) = φ.

theorem TauCeti.Real.legendreE_eq_legendreF_sub {φ k : ℝ} (hφ0 : 0 ≤ φ) (hφ : φ ≤ Real.pi / 2) (hk : k ^ 2 * Real.sin φ ^ 2 < 1) : legendreE φ k = legendreF φ k - k ^ 2 * ∫ (θ : ℝ) in 0..φ, (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) * Real.sin θ ^ 2

The integral of the second kind in terms of the first: E(φ, k) = F(φ, k) - k² ∫₀^φ sin² θ (1 - k² sin² θ)^(-1/2) dθ for 0 ≤ φ ≤ π / 2 and k² sin² φ < 1.

theorem TauCeti.Real.legendreEc_pos (k : ℝ) : 0 < legendreEc k

For every modulus k, the complete integral of the second kind E(k) is positive.

@[simp]

theorem TauCeti.Real.legendreEc_neg (k : ℝ) : legendreEc (-k) = legendreEc k

@[simp]

theorem TauCeti.Real.legendreEc_abs (k : ℝ) : legendreEc |k| = legendreEc k

Taking the absolute value of the modulus leaves the complete second kind unchanged.

@[simp]

theorem TauCeti.Real.legendreEc_zero : legendreEc 0 = Real.pi / 2

The integral of the third kind

@[simp]

theorem TauCeti.Real.legendrePi_zero (k α2 : ℝ) : legendrePi 0 k α2 = 0

@[simp]

theorem TauCeti.Real.legendrePi_zero_characteristic (φ k : ℝ) : legendrePi φ k 0 = legendreF φ k

At characteristic 0 the integral of the third kind is that of the first kind: Π(φ, k, 0) = F(φ, k).

theorem TauCeti.Real.hasDerivAt_legendrePi {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (φ : ℝ) : HasDerivAt (fun (x : ℝ) => legendrePi x k α2) ((1 - α2 * Real.sin φ ^ 2)⁻¹ * (1 - k ^ 2 * Real.sin φ ^ 2) ^ (-1 / 2)) φ

The integral of the third kind is a primitive of its integrand.

theorem TauCeti.Real.continuous_legendrePi {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) : Continuous fun (x : ℝ) => legendrePi x k α2

For k ^ 2 < 1 and α2 < 1, Π(φ, k, α²) is continuous in the amplitude φ.

theorem TauCeti.Real.strictMono_legendrePi {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) : StrictMono fun (x : ℝ) => legendrePi x k α2

For k ^ 2 < 1 and α2 < 1, Π(φ, k, α²) is strictly increasing in the amplitude φ.

theorem TauCeti.Real.legendrePi_pos {φ k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (hφ : 0 < φ) : 0 < legendrePi φ k α2

For k ^ 2 < 1 and α2 < 1, Π(φ, k, α²) is positive for positive amplitude φ.

@[simp]

theorem TauCeti.Real.legendrePi_neg (φ k α2 : ℝ) : legendrePi (-φ) k α2 = -legendrePi φ k α2

Π(φ, k, α²) is odd in the amplitude.

@[simp]

theorem TauCeti.Real.legendrePi_neg_modulus (φ k α2 : ℝ) : legendrePi φ (-k) α2 = legendrePi φ k α2

Π(φ, k, α²) is even in the modulus.

theorem TauCeti.Real.legendrePi_add_int_mul_pi {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (φ : ℝ) (n : ℤ) : legendrePi (φ + ↑n * Real.pi) k α2 = legendrePi φ k α2 + 2 * ↑n * legendrePic k α2

Quasi-periodicity of Π: Π(φ + nπ, k, α²) = Π(φ, k, α²) + 2 n Π(k, α²) for every integer n.

theorem TauCeti.Real.legendrePi_add_pi {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (φ : ℝ) : legendrePi (φ + Real.pi) k α2 = legendrePi φ k α2 + 2 * legendrePic k α2

theorem TauCeti.Real.legendrePi_int_mul_pi {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) (n : ℤ) : legendrePi (↑n * Real.pi) k α2 = 2 * ↑n * legendrePic k α2

theorem TauCeti.Real.legendrePi_eq_legendreF_add {φ k α2 : ℝ} (hφ0 : 0 ≤ φ) (hφ : φ ≤ Real.pi / 2) (hk : k ^ 2 * Real.sin φ ^ 2 < 1) (hα : α2 * Real.sin φ ^ 2 < 1) : legendrePi φ k α2 = legendreF φ k + α2 * ∫ (θ : ℝ) in 0..φ, (1 - k ^ 2 * Real.sin θ ^ 2) ^ (-1 / 2) * (Real.sin θ ^ 2 / (1 - α2 * Real.sin θ ^ 2))

The integral of the third kind in terms of the first: Π(φ, k, α²) = F(φ, k) + α² ∫₀^φ sin² θ (1 - α² sin² θ)⁻¹ (1 - k² sin² θ)^(-1/2) dθ for 0 ≤ φ ≤ π / 2, k² sin² φ < 1 and α² sin² φ < 1.

theorem TauCeti.Real.legendrePic_pos {k α2 : ℝ} (hk : k ^ 2 < 1) (hα : α2 < 1) : 0 < legendrePic k α2

For k ^ 2 < 1 and α2 < 1, the complete integral of the third kind Π(k, α²) is positive.

@[simp]

theorem TauCeti.Real.legendrePic_neg_modulus (k α2 : ℝ) : legendrePic (-k) α2 = legendrePic k α2

@[simp]

theorem TauCeti.Real.legendrePic_zero_characteristic (k : ℝ) : legendrePic k 0 = legendreK k

Π(k, 0) = K(k).