Physlib.Mathematics.SpecialFunctions.EllipticIntegral

The complete elliptic integral of the first kind

This file may eventually be upstreamed to Mathlib.

i. Overview

Legendre's complete elliptic integral of the first kind is, in the parameter convention,

`K(m) = ∫ φ in 0..π/2, (1 - m sin² φ) ^ (-1/2)`

(Abramowitz & Stegun 17.3.1). The physics literature more often uses the modulus convention and writes `K(k)`, as Landau & Lifshitz do, for what is here `completeEllipticK (k ^ 2)`; the two conventions are related by `m = k²`. Mathlib knows the Weierstrass elliptic function `℘` (`PeriodPair.weierstrassP`) but has no Legendre-form elliptic integrals; this file defines the complete integral of the first kind and develops its basic theory on the domain `m < 1`, where the radicand `1 - m sin² φ` is positive and the integrand continuous.

The integral enters physics wherever a period or a potential is computed exactly rather than in a small-parameter expansion. Physlib's use of it so far is the simple pendulum: released from rest at amplitude `θ₀`, the pendulum has period `4 √(ℓ / g) K(sin² (θ₀ / 2))` (Landau & Lifshitz §11, Problem 1), the consumer being `Physlib.ClassicalMechanics.Pendulum.SimplePendulum.PeriodFormula`. More broadly, the complete integrals of the first and second kind give the magnetic field of a circular current loop and the potential of a uniformly charged ring, and the second kind, `E`, gives the arc length of an ellipse. This file defines `K` so that such results can be stated.

For `m ≥ 1` the definition still elaborates, but its value is not Legendre's. At `m = 1` the integrand is `1 / cos φ`, which is not interval integrable on `[0, π/2]`, so the integral is `0` by `intervalIntegral.integral_undef`, whereas `K(1) = ∞`. For `m > 1` the radicand is negative on `(arcsin (1/√m), π/2]`, where the real power at exponent `-(1/2)` of a negative base vanishes (`Real.rpow_def_of_neg` supplies the factor `cos (-(1 / 2) * π) = 0`), so the Lean value is the finite positive integral over `[0, arcsin (1/√m)]`; by the reciprocal-modulus transformation this is `K(1/m) / √m`, the real part of the complex Legendre integral (DLMF §19.7(ii)) — not proved here. Every lemma of this file about a general parameter therefore carries its domain hypothesis `m < 1` explicitly.

ii. Key results

- `completeEllipticK` : the complete elliptic integral of the first kind, as a function of the parameter `m`. - `completeEllipticK_zero` : `K 0 = π / 2`. - `completeEllipticK_pos` : for `m < 1` the integral is positive. - `completeEllipticK_mono` : for `m₁ ≤ m₂ < 1`, `K m₁ ≤ K m₂`. - `completeEllipticK_strictMono` : for `m₁ < m₂ < 1`, `K m₁ < K m₂`. - `pi_div_two_le_completeEllipticK` : for `0 ≤ m < 1`, `π / 2 ≤ K m`. - `completeEllipticK_le` : for `0 ≤ m < 1`, `K m ≤ π / 2 * (1 - m) ^ (-1/2)`. - `continuousOn_completeEllipticK` : `K` is continuous on `(-∞, 1)`. - `continuousAt_completeEllipticK` : `K` is continuous at every `m < 1`.

iii. Table of contents

A. Definition and the integrand
B. Value at zero and positivity
C. Monotonicity and bounds in the parameter
D. Continuity on the domain

iv. References

- M. Abramowitz, I. A. Stegun, Handbook of Mathematical Functions, §17.3 (the parameter convention, 17.3.1). - NIST DLMF §19.7(ii) (the reciprocal-modulus transformation). - Landau & Lifshitz, Mechanics, 3rd ed., §11, Problem 1 (the pendulum period as `K(k)`, modulus convention).

A. Definition and the integrand

The integral is defined for every real parameter `m`; on the domain `m < 1` the radicand is positive, so the integrand is continuous and interval integrable.

B. Value at zero and positivity

At `m = 0` the integrand is the constant `1` and the integral is elementary; for `m < 1` the integral is positive, being the integral of a positive continuous function.

C. Monotonicity and bounds in the parameter

For fixed `φ` the radicand `1 - m sin² φ` decreases in `m`, so the integrand, a negative power of the radicand, increases in `m` on the domain; integrating the pointwise inequality over `[0, π/2]` gives monotonicity of `K`, and since the inequality is strict at `φ = π/2` the monotonicity is strict. Together with `K 0 = π / 2` this bounds `K` below on `[0, 1)`; bounding the radicand below by `1 - m` bounds `K` above by `π / 2 * (1 - m) ^ (-1/2)` there.

D. Continuity on the domain

The integrand is jointly continuous in `(m, φ)` on `(-∞, 1) × ℝ`, where the radicand is positive, but not on all of `ℝ × ℝ`. Restricting the parameter to the subtype `Set.Iio 1` makes the joint continuity global, so Mathlib's continuity of a parametric interval integral with fixed endpoints (`intervalIntegral.continuous_parametric_intervalIntegral_of_continuous'`) applies and gives continuity of `K` on the domain. Continuity at each point `m < 1` follows, `(-∞, 1)` being a neighbourhood of `m`.

16 declarations

definition

Complete elliptic integral of the first kind $K(m)$

#completeEllipticK

The complete elliptic integral of the first kind $K(m)$ is defined for a real number $m$ as the integral: $K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi$ where $m$ is the parameter and $\phi$ is the variable of integration. For $m < 1$ , this corresponds to the standard Legendre form where the integrand is continuous and positive.

theorem

$K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi$

#completeEllipticK_def

For any real number $m$ , the complete elliptic integral of the first kind $K(m)$ is given by the integral: $K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi$

theorem

$1 - m \sin^2 \phi > 0$ for $m < 1$

#completeEllipticK_radicand_pos

For any real number $m < 1$ and any real number $\phi$ , the radicand $1 - m \sin^2 \phi$ appearing in the definition of the complete elliptic integral of the first kind $K(m)$ is strictly positive.

theorem

Continuity of the integrand of the complete elliptic integral of the first kind for $m < 1$

#continuous_completeEllipticK_integrand

For any real number $m < 1$ , the function $f(\phi) = (1 - m \sin^2 \phi)^{-1/2}$ is continuous for all $\phi \in \mathbb{R}$ . This function is the integrand used in the definition of Legendre's complete elliptic integral of the first kind $K(m)$ .

theorem

The integrand of the complete elliptic integral of the first kind is interval integrable for $m < 1$

#intervalIntegrable_completeEllipticK_integrand

For any real number $m < 1$ , the function $f(\varphi) = (1 - m \sin^2 \varphi)^{-1/2}$ is interval integrable on the interval $[0, \pi/2]$ .

theorem

$K(0) = \pi / 2$

#completeEllipticK_zero

The complete elliptic integral of the first kind $K(m)$ evaluated at parameter $m = 0$ is equal to $\pi / 2$ . At this parameter value, the integrand of the integral reduces to the constant function $1$ .

theorem

$K(m) > 0$ for $m < 1$

#completeEllipticK_pos

For any real number $m < 1$ , the complete elliptic integral of the first kind $K(m)$ is strictly positive, i.e., $K(m) > 0$ .

theorem

$m_1 \le m_2 < 1 \implies K(m_1) \le K(m_2)$

#completeEllipticK_mono

For any real numbers $m_1$ and $m_2$ such that $m_1 \le m_2$ and $m_2 < 1$ , the complete elliptic integral of the first kind $K(m)$ , defined as $K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi,$ satisfies $K(m_1) \le K(m_2)$ .

theorem

$K(m)$ is Monotone on $(-\infty, 1)$

#monotoneOn_completeEllipticK

The complete elliptic integral of the first kind $K(m)$ is monotone on the interval $(-\infty, 1)$ . That is, for any $m_1, m_2 < 1$ , if $m_1 \leq m_2$ , then $K(m_1) \leq K(m_2)$ .

theorem

Strict monotonicity of $K(m)$ for $m < 1$

#completeEllipticK_strictMono

For any real numbers $m_1$ and $m_2$ such that $m_1 < m_2 < 1$ , the complete elliptic integral of the first kind $K(m)$ satisfies $K(m_1) < K(m_2)$ . Here, $K(m)$ is defined as $K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi.$

theorem

$K(m)$ is Strictly Increasing on $(-\infty, 1)$

#strictMonoOn_completeEllipticK

The complete elliptic integral of the first kind $K(m)$ , defined as $K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi,$ is strictly increasing on the interval $(-\infty, 1)$ .

theorem

$\frac{\pi}{2} \le K(m)$ for $0 \le m < 1$

#pi_div_two_le_completeEllipticK

For any real number $m$ such that $0 \le m < 1$ , the complete elliptic integral of the first kind $K(m)$ is bounded below by $\pi/2$ , that is, $\frac{\pi}{2} \le K(m)$ .

theorem

$K(m) \le \frac{\pi}{2} (1 - m)^{-1/2}$ for $0 \le m < 1$

#completeEllipticK_le

For any real number $m$ such that $0 \le m < 1$ , the complete elliptic integral of the first kind $K(m)$ satisfies the inequality $K(m) \le \frac{\pi}{2} (1 - m)^{-1/2}.$

theorem

$K(m)$ is continuous on $(-\infty, 1)$

#continuousOn_completeEllipticK

The complete elliptic integral of the first kind $K(m)$ , defined for a real parameter $m$ as $K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi$ is continuous on the interval $(-\infty, 1)$ .

theorem

$K(m)$ is continuous for $m < 1$

#continuousAt_completeEllipticK

For any real number $m$ such that $m < 1$ , the complete elliptic integral of the first kind $K(m)$ is continuous at $m$ .

theorem

$K(m)$ is continuous at $m = 0$

#continuousAt_completeEllipticK_zero

The complete elliptic integral of the first kind $K(m)$ is continuous at $m = 0$ .

Physlib.Mathematics.SpecialFunctions.EllipticIntegral

The complete elliptic integral of the first kind

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Definition and the integrand

B. Value at zero and positivity

C. Monotonicity and bounds in the parameter

D. Continuity on the domain

Complete elliptic integral of the first kind K(m)K(m)K(m)

K(m)=∫0π/2(1−msin⁡2ϕ)−1/2dϕK(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phiK(m)=∫0π/2​(1−msin2ϕ)−1/2dϕ

1−msin⁡2ϕ>01 - m \sin^2 \phi > 01−msin2ϕ>0 for m<1m < 1m<1

Continuity of the integrand of the complete elliptic integral of the first kind for m<1m < 1m<1

The integrand of the complete elliptic integral of the first kind is interval integrable for m<1m < 1m<1

K(0)=π/2K(0) = \pi / 2K(0)=π/2

K(m)>0K(m) > 0K(m)>0 for m<1m < 1m<1

m1≤m2<1 ⟹ K(m1)≤K(m2)m_1 \le m_2 < 1 \implies K(m_1) \le K(m_2)m1​≤m2​<1⟹K(m1​)≤K(m2​)

K(m)K(m)K(m) is Monotone on (−∞,1)(-\infty, 1)(−∞,1)

Strict monotonicity of K(m)K(m)K(m) for m<1m < 1m<1

K(m)K(m)K(m) is Strictly Increasing on (−∞,1)(-\infty, 1)(−∞,1)

π2≤K(m)\frac{\pi}{2} \le K(m)2π​≤K(m) for 0≤m<10 \le m < 10≤m<1

K(m)≤π2(1−m)−1/2K(m) \le \frac{\pi}{2} (1 - m)^{-1/2}K(m)≤2π​(1−m)−1/2 for 0≤m<10 \le m < 10≤m<1

K(m)K(m)K(m) is continuous on (−∞,1)(-\infty, 1)(−∞,1)

K(m)K(m)K(m) is continuous for m<1m < 1m<1

K(m)K(m)K(m) is continuous at m=0m = 0m=0

Complete elliptic integral of the first kind $K(m)$

$K(m) = \int_{0}^{\pi/2} (1 - m \sin^2 \phi)^{-1/2} d\phi$

$1 - m \sin^2 \phi > 0$ for $m < 1$

Continuity of the integrand of the complete elliptic integral of the first kind for $m < 1$

The integrand of the complete elliptic integral of the first kind is interval integrable for $m < 1$

$K(0) = \pi / 2$

$K(m) > 0$ for $m < 1$

$m_1 \le m_2 < 1 \implies K(m_1) \le K(m_2)$

$K(m)$ is Monotone on $(-\infty, 1)$

Strict monotonicity of $K(m)$ for $m < 1$

$K(m)$ is Strictly Increasing on $(-\infty, 1)$

$\frac{\pi}{2} \le K(m)$ for $0 \le m < 1$

$K(m) \le \frac{\pi}{2} (1 - m)^{-1/2}$ for $0 \le m < 1$

$K(m)$ is continuous on $(-\infty, 1)$

$K(m)$ is continuous for $m < 1$

$K(m)$ is continuous at $m = 0$