Monotonicity of Legendre's integrals in the modulus

For nonnegative amplitude, increasing the squared modulus increases legendreF when the larger squared modulus is below 1, and decreases legendreE for all real moduli. For positive amplitude these comparisons are strict. In particular, legendreK is strictly increasing on [0, 1), and legendreEc is strictly decreasing on [0, ∞). Consequently legendreEc k ≤ π / 2 ≤ legendreK k on the nonsingular range, with equality only at zero. We also have the lower bound (1 - k²) K(k) ≤ E(k) for k² < 1. Squared-modulus comparisons also apply directly to negative moduli.

These order properties follow by comparing the defining integrands, without differentiating in the modulus. For strictness the integrands differ at a sufficiently small positive angle.

References

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

The conventions agree with B. Braams' lean-codes. Its LegendreStandard and CompleteK modules treat transformations through symmetric integrals; the comparison proofs here are independent and use the direct real integral definitions.

theorem TauCeti.Real.legendreF_le_of_sq_le {φ k l : ℝ} (hφ : 0 ≤ φ) (hkl : k ^ 2 ≤ l ^ 2) (hl : l ^ 2 < 1) : legendreF φ k ≤ legendreF φ l

For nonnegative amplitude, the first kind increases with the squared modulus when the larger squared modulus satisfies l ^ 2 < 1.

theorem TauCeti.Real.legendreE_le_of_sq_le {φ k l : ℝ} (hφ : 0 ≤ φ) (hkl : k ^ 2 ≤ l ^ 2) : legendreE φ l ≤ legendreE φ k

For nonnegative amplitude, the second kind decreases with the squared modulus. This non-strict comparison holds even beyond the nonsingular range.

theorem TauCeti.Real.monotoneOn_legendreF_modulus {φ : ℝ} (hφ : 0 ≤ φ) : MonotoneOn (legendreF φ) (Set.Ico 0 1)

For nonnegative amplitude, F(φ, k) is increasing in k ∈ [0, 1).

theorem TauCeti.Real.antitoneOn_legendreE_modulus {φ : ℝ} (hφ : 0 ≤ φ) : AntitoneOn (legendreE φ) (Set.Ici 0)

For nonnegative amplitude, E(φ, k) is decreasing on the nonnegative moduli.

theorem TauCeti.Real.legendreF_lt_of_sq_lt {φ k l : ℝ} (hφ : 0 < φ) (hkl : k ^ 2 < l ^ 2) (hl : l ^ 2 < 1) : legendreF φ k < legendreF φ l

For positive amplitude, the first kind strictly increases with the squared modulus when the larger squared modulus is below 1.

theorem TauCeti.Real.legendreE_lt_of_sq_lt {φ k l : ℝ} (hφ : 0 < φ) (hkl : k ^ 2 < l ^ 2) : legendreE φ l < legendreE φ k

For positive amplitude, the second kind strictly decreases with the squared modulus for all real moduli.

theorem TauCeti.Real.legendreK_lt_of_sq_lt {k l : ℝ} (hkl : k ^ 2 < l ^ 2) (hl : l ^ 2 < 1) : legendreK k < legendreK l

The complete first kind strictly increases with the squared modulus below 1.

theorem TauCeti.Real.legendreEc_lt_of_sq_lt {k l : ℝ} (hkl : k ^ 2 < l ^ 2) : legendreEc l < legendreEc k

The complete second kind strictly decreases with the squared modulus for all real moduli.

theorem TauCeti.Real.strictMonoOn_legendreK : StrictMonoOn legendreK (Set.Ico 0 1)

K is strictly increasing on [0, 1).

theorem TauCeti.Real.strictAntiOn_legendreEc : StrictAntiOn legendreEc (Set.Ici 0)

The complete second kind is strictly decreasing on the nonnegative moduli.

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

π / 2 is a lower bound for the complete first kind in the nonsingular range.

theorem TauCeti.Real.legendreEc_le_pi_div_two (k : ℝ) : legendreEc k ≤ Real.pi / 2

π / 2 is an upper bound for the complete second kind, for every real modulus.

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

The second kind lies above (1 - k²) K(k) in the nonsingular range.

@[simp]

theorem TauCeti.Real.legendreK_eq_pi_div_two_iff {k : ℝ} (hk : k ^ 2 < 1) : legendreK k = Real.pi / 2 ↔ k = 0

The lower bound for K is attained exactly at modulus zero.

@[simp]

theorem TauCeti.Real.legendreEc_eq_pi_div_two_iff {k : ℝ} : legendreEc k = Real.pi / 2 ↔ k = 0

The upper bound for the complete second kind is attained exactly at modulus zero.