The Jacobi elliptic functions of a real variable

For a modulus k with k ^ 2 < 1, the integral of the first kind φ ↦ F(φ, k) is an order isomorphism of ℝ (TauCeti.Real.legendreFOrderIso). This file defines its inverse, the Jacobi amplitude jacobiAm k, and the three basic Jacobi elliptic functions (DLMF §22.16(i))

• jacobiSn k u = sin (jacobiAm k u);
• jacobiCn k u = cos (jacobiAm k u);
• jacobiDn k u = √(1 - k ^ 2 * jacobiSn k u ^ 2),

as functions ℝ → ℝ with the modulus as first argument. For k ^ 2 ≥ 1 the amplitude is the junk value id; theorems that need k ^ 2 < 1 say so.

We prove the basic theory:

• the amplitude inverts F, is odd, continuous and strictly increasing, satisfies am(u + 2 n K) = am(u) + n π and am(K) = π / 2, has derivative dn, and is nonexpansive in its argument;
• the identities sn² + cn² = 1 and dn² + k² sn² = 1, positivity of dn, and the parities of sn, cn and dn in the argument and in the modulus;
• the derivatives sn′ = cn dn, cn′ = -sn dn, dn′ = -k² sn cn, and the first-order differential equation (sn′)² = (1 - sn²)(1 - k² sn²);
• the antiperiods 2K of sn and cn, hence their period 4K, the period 2K of dn, and the values at u = K;
• the points where sn = 1, and hence that 4K is the least positive period of sn;
• the degeneration at modulus 0: am = id, sn = sin, cn = cos, dn = 1.

Here K = legendreK k is the complete integral of the first kind.

References

• NIST Digital Library of Mathematical Functions, Chapter 22, https://dlmf.nist.gov/22.
• E. T. Whittaker and G. N. Watson, A Course of Modern Analysis, Chapter XXII.

Definitions

noncomputable def TauCeti.Real.jacobiAm (k : ℝ) : ℝ → ℝ

The Jacobi amplitude am(u, k) (DLMF §22.16(i)): for k ^ 2 < 1, the inverse of the integral of the first kind φ ↦ F(φ, k), so that F(am(u, k), k) = u. For k ^ 2 ≥ 1 it is the junk value id.

noncomputable def TauCeti.Real.jacobiSn (k u : ℝ) : ℝ

The Jacobi elliptic function sn(u, k) = sin (am(u, k)).

noncomputable def TauCeti.Real.jacobiCn (k u : ℝ) : ℝ

The Jacobi elliptic function cn(u, k) = cos (am(u, k)).

noncomputable def TauCeti.Real.jacobiDn (k u : ℝ) : ℝ

The Jacobi elliptic function dn(u, k) = √(1 - k² sn²(u, k)).

theorem TauCeti.Real.jacobiSn_def (k u : ℝ) : jacobiSn k u = Real.sin (jacobiAm k u)

theorem TauCeti.Real.jacobiCn_def (k u : ℝ) : jacobiCn k u = Real.cos (jacobiAm k u)

theorem TauCeti.Real.jacobiDn_def (k u : ℝ) : jacobiDn k u = √(1 - k ^ 2 * jacobiSn k u ^ 2)

The amplitude

@[simp]

theorem TauCeti.Real.coe_legendreFOrderIso_symm {k : ℝ} (hk : k ^ 2 < 1) : ⇑(legendreFOrderIso hk).symm = jacobiAm k

For k ^ 2 < 1, the inverse of the order isomorphism φ ↦ F(φ, k) is the amplitude.

theorem TauCeti.Real.jacobiAm_of_one_le_sq {k : ℝ} (hk : 1 ≤ k ^ 2) : jacobiAm k = id

For k ^ 2 ≥ 1 the amplitude is the junk value id.

@[simp]

theorem TauCeti.Real.legendreF_jacobiAm {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : legendreF (jacobiAm k u) k = u

@[simp]

theorem TauCeti.Real.jacobiAm_legendreF {k : ℝ} (hk : k ^ 2 < 1) (φ : ℝ) : jacobiAm k (legendreF φ k) = φ

theorem TauCeti.Real.jacobiAm_eq_iff {k : ℝ} (hk : k ^ 2 < 1) {u φ : ℝ} : jacobiAm k u = φ ↔ legendreF φ k = u

For k ^ 2 < 1, am(u, k) = φ exactly when F(φ, k) = u.

theorem TauCeti.Real.strictMono_jacobiAm (k : ℝ) : StrictMono (jacobiAm k)

The amplitude is strictly increasing, for every modulus.

theorem TauCeti.Real.continuous_jacobiAm (k : ℝ) : Continuous (jacobiAm k)

The amplitude is continuous, for every modulus.

@[simp]

theorem TauCeti.Real.jacobiAm_zero (k : ℝ) : jacobiAm k 0 = 0

@[simp]

theorem TauCeti.Real.jacobiAm_neg (k u : ℝ) : jacobiAm k (-u) = -jacobiAm k u

The amplitude is odd: am(-u, k) = -am(u, k).

@[simp]

theorem TauCeti.Real.jacobiAm_neg_modulus (k : ℝ) : jacobiAm (-k) = jacobiAm k

The amplitude is even in the modulus.

@[simp]

theorem TauCeti.Real.jacobiAm_zero_modulus : jacobiAm 0 = id

At modulus 0 the amplitude is the identity.

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

Quasi-periodicity of the amplitude: am(u + 2 n K, k) = am(u, k) + n π for every integer n.

theorem TauCeti.Real.jacobiAm_add_two_mul_legendreK {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : jacobiAm k (u + 2 * legendreK k) = jacobiAm k u + Real.pi

@[simp]

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

The amplitude at a quarter period is π / 2: am(K, k) = π / 2.

Algebraic identities

@[simp]

theorem TauCeti.Real.jacobiSn_sq_add_jacobiCn_sq (k u : ℝ) : jacobiSn k u ^ 2 + jacobiCn k u ^ 2 = 1

theorem TauCeti.Real.one_sub_sq_mul_jacobiSn_sq_nonneg {k : ℝ} (hk : k ^ 2 ≤ 1) (u : ℝ) : 0 ≤ 1 - k ^ 2 * jacobiSn k u ^ 2

For k ^ 2 ≤ 1, the radicand defining dn is nonnegative.

theorem TauCeti.Real.one_sub_sq_mul_jacobiSn_sq_pos {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : 0 < 1 - k ^ 2 * jacobiSn k u ^ 2

For k ^ 2 < 1, the radicand defining dn is positive.

theorem TauCeti.Real.jacobiDn_sq {k : ℝ} (hk : k ^ 2 ≤ 1) (u : ℝ) : jacobiDn k u ^ 2 = 1 - k ^ 2 * jacobiSn k u ^ 2

theorem TauCeti.Real.jacobiDn_sq_add_sq_mul_jacobiSn_sq {k : ℝ} (hk : k ^ 2 ≤ 1) (u : ℝ) : jacobiDn k u ^ 2 + k ^ 2 * jacobiSn k u ^ 2 = 1

theorem TauCeti.Real.jacobiDn_nonneg (k u : ℝ) : 0 ≤ jacobiDn k u

theorem TauCeti.Real.jacobiDn_pos {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : 0 < jacobiDn k u

theorem TauCeti.Real.jacobiDn_le_one (k u : ℝ) : jacobiDn k u ≤ 1

Values at zero and parity

@[simp]

theorem TauCeti.Real.jacobiSn_zero (k : ℝ) : jacobiSn k 0 = 0

@[simp]

theorem TauCeti.Real.jacobiCn_zero (k : ℝ) : jacobiCn k 0 = 1

@[simp]

theorem TauCeti.Real.jacobiDn_zero (k : ℝ) : jacobiDn k 0 = 1

@[simp]

theorem TauCeti.Real.jacobiSn_neg (k u : ℝ) : jacobiSn k (-u) = -jacobiSn k u

sn is odd.

@[simp]

theorem TauCeti.Real.jacobiCn_neg (k u : ℝ) : jacobiCn k (-u) = jacobiCn k u

cn is even.

@[simp]

theorem TauCeti.Real.jacobiDn_neg (k u : ℝ) : jacobiDn k (-u) = jacobiDn k u

dn is even.

@[simp]

theorem TauCeti.Real.jacobiSn_neg_modulus (k : ℝ) : jacobiSn (-k) = jacobiSn k

@[simp]

theorem TauCeti.Real.jacobiCn_neg_modulus (k : ℝ) : jacobiCn (-k) = jacobiCn k

@[simp]

theorem TauCeti.Real.jacobiDn_neg_modulus (k : ℝ) : jacobiDn (-k) = jacobiDn k

The degenerate modulus k = 0

@[simp]

theorem TauCeti.Real.jacobiSn_zero_modulus : jacobiSn 0 = Real.sin

@[simp]

theorem TauCeti.Real.jacobiCn_zero_modulus : jacobiCn 0 = Real.cos

@[simp]

theorem TauCeti.Real.jacobiDn_zero_modulus : jacobiDn 0 = 1

Continuity and derivatives

theorem TauCeti.Real.continuous_jacobiSn (k : ℝ) : Continuous (jacobiSn k)

theorem TauCeti.Real.continuous_jacobiCn (k : ℝ) : Continuous (jacobiCn k)

theorem TauCeti.Real.continuous_jacobiDn (k : ℝ) : Continuous (jacobiDn k)

theorem TauCeti.Real.hasDerivAt_jacobiAm {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : HasDerivAt (jacobiAm k) (jacobiDn k u) u

The derivative of the amplitude is dn: am′(u, k) = dn(u, k) (DLMF §22.16(i)).

theorem TauCeti.Real.lipschitzWith_jacobiAm (k : ℝ) : LipschitzWith 1 (jacobiAm k)

The Jacobi amplitude is nonexpansive in its real argument.

theorem TauCeti.Real.hasDerivAt_jacobiSn {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : HasDerivAt (jacobiSn k) (jacobiCn k u * jacobiDn k u) u

sn′ = cn · dn (DLMF §22.13(i)).

theorem TauCeti.Real.hasDerivAt_jacobiCn {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : HasDerivAt (jacobiCn k) (-jacobiSn k u * jacobiDn k u) u

cn′ = -sn · dn (DLMF §22.13(i)).

theorem TauCeti.Real.hasDerivAt_jacobiDn {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : HasDerivAt (jacobiDn k) (-k ^ 2 * jacobiSn k u * jacobiCn k u) u

dn′ = -k² · sn · cn (DLMF §22.13(i)).

theorem TauCeti.Real.deriv_jacobiSn_sq {k : ℝ} (hk : k ^ 2 < 1) (u : ℝ) : deriv (jacobiSn k) u ^ 2 = (1 - jacobiSn k u ^ 2) * (1 - k ^ 2 * jacobiSn k u ^ 2)

The first-order differential equation of sn (DLMF §22.13(ii)): (sn′)² = (1 - sn²)(1 - k² sn²).

Periods and values at the quarter period

theorem TauCeti.Real.jacobiSn_antiperiodic {k : ℝ} (hk : k ^ 2 < 1) : Function.Antiperiodic (jacobiSn k) (2 * legendreK k)

sn changes sign under a shift by 2K: sn(u + 2K) = -sn(u) (DLMF §22.4(iii)).

theorem TauCeti.Real.jacobiCn_antiperiodic {k : ℝ} (hk : k ^ 2 < 1) : Function.Antiperiodic (jacobiCn k) (2 * legendreK k)

cn changes sign under a shift by 2K: cn(u + 2K) = -cn(u) (DLMF §22.4(iii)).

theorem TauCeti.Real.jacobiSn_periodic {k : ℝ} (hk : k ^ 2 < 1) : Function.Periodic (jacobiSn k) (4 * legendreK k)

sn has period 4K.

theorem TauCeti.Real.jacobiCn_periodic {k : ℝ} (hk : k ^ 2 < 1) : Function.Periodic (jacobiCn k) (4 * legendreK k)

cn has period 4K.

theorem TauCeti.Real.jacobiDn_periodic {k : ℝ} (hk : k ^ 2 < 1) : Function.Periodic (jacobiDn k) (2 * legendreK k)

dn has period 2K.

@[simp]

theorem TauCeti.Real.jacobiSn_legendreK {k : ℝ} (hk : k ^ 2 < 1) : jacobiSn k (legendreK k) = 1

@[simp]

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

@[simp]

theorem TauCeti.Real.jacobiDn_legendreK {k : ℝ} (hk : k ^ 2 < 1) : jacobiDn k (legendreK k) = √(1 - k ^ 2)

dn(K, k) = √(1 - k²), the complementary modulus.

theorem TauCeti.Real.jacobiSn_eq_one_iff {k : ℝ} (hk : k ^ 2 < 1) {u : ℝ} : jacobiSn k u = 1 ↔ ∃ (n : ℤ), legendreK k + ↑n * (4 * legendreK k) = u

sn attains the value 1 exactly at the points K + 4 n K, n ∈ ℤ.

theorem TauCeti.Real.isLeast_jacobiSn_period {k : ℝ} (hk : k ^ 2 < 1) : IsLeast {p : ℝ | 0 < p ∧ Function.Periodic (jacobiSn k) p} (4 * legendreK k)

4K is the least positive period of sn (DLMF §22.4(i)). For k = 0 it is the least positive period 2π of sin.