The addition theorem for the Jacobi elliptic functions

For a modulus k with k ^ 2 < 1, we prove the addition theorem for the real Jacobi elliptic functions (DLMF 22.8.1–22.8.3): writing D = 1 - k² sn²(u) sn²(v),

• sn(u + v) = (sn u · cn v · dn v + sn v · cn u · dn u) / D;
• cn(u + v) = (cn u · cn v - sn u · dn u · sn v · dn v) / D;
• dn(u + v) = (dn u · dn v - k² · sn u · cn u · sn v · cn v) / D,

together with the positivity of the common denominator D.

Implementation notes

The proof is Euler's: fix a = u + v and regard each right-hand side as a function of t = u, with v = a - t. The derivatives sn′ = cn dn, cn′ = -sn dn, dn′ = -k² sn cn and the identities sn² + cn² = 1, dn² + k² sn² = 1 show that its derivative vanishes, so it is constant in t; its value at t = 0 is the left-hand side.

References

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

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

The denominator 1 - k² sn²(u) sn²(v) of the addition theorem is positive for k ^ 2 < 1.

Euler's argument

The addition theorem

theorem TauCeti.Real.jacobiSn_add {k : ℝ} (hk : k ^ 2 < 1) (u v : ℝ) : jacobiSn k (u + v) = (jacobiSn k u * jacobiCn k v * jacobiDn k v + jacobiSn k v * jacobiCn k u * jacobiDn k u) / (1 - k ^ 2 * jacobiSn k u ^ 2 * jacobiSn k v ^ 2)

The addition theorem for sn (DLMF 22.8.1): sn(u + v) = (sn u · cn v · dn v + sn v · cn u · dn u) / (1 - k² sn²(u) sn²(v)).

theorem TauCeti.Real.jacobiCn_add {k : ℝ} (hk : k ^ 2 < 1) (u v : ℝ) : jacobiCn k (u + v) = (jacobiCn k u * jacobiCn k v - jacobiSn k u * jacobiDn k u * jacobiSn k v * jacobiDn k v) / (1 - k ^ 2 * jacobiSn k u ^ 2 * jacobiSn k v ^ 2)

The addition theorem for cn (DLMF 22.8.2): cn(u + v) = (cn u · cn v - sn u · dn u · sn v · dn v) / (1 - k² sn²(u) sn²(v)).

theorem TauCeti.Real.jacobiDn_add {k : ℝ} (hk : k ^ 2 < 1) (u v : ℝ) : jacobiDn k (u + v) = (jacobiDn k u * jacobiDn k v - k ^ 2 * jacobiSn k u * jacobiCn k u * jacobiSn k v * jacobiCn k v) / (1 - k ^ 2 * jacobiSn k u ^ 2 * jacobiSn k v ^ 2)

The addition theorem for dn (DLMF 22.8.3): dn(u + v) = (dn u · dn v - k² · sn u · cn u · sn v · cn v) / (1 - k² sn²(u) sn²(v)).