# Lemmas about NormedSpace.exp on Quaternions #

This file contains results about NormedSpace.exp on Quaternion ℝ.

## Main results #

• Quaternion.exp_eq: the general expansion of the quaternion exponential in terms of Real.cos and Real.sin.
• Quaternion.exp_of_re_eq_zero: the special case when the quaternion has a zero real part.
• Quaternion.norm_exp: the norm of the quaternion exponential is the norm of the exponential of the real part.
@[simp]
theorem Quaternion.exp_coe (r : ) :
= ()
theorem Quaternion.expSeries_even_of_imaginary {q : } (hq : q.re = 0) (n : ) :
((NormedSpace.expSeries () (2 * n)) fun (x : Fin (2 * n)) => q) = ((-1) ^ n * q ^ (2 * n) / (2 * n).factorial)

The even terms of expSeries are real, and correspond to the series for $\cos ‖q‖$.

theorem Quaternion.expSeries_odd_of_imaginary {q : } (hq : q.re = 0) (n : ) :
((NormedSpace.expSeries () (2 * n + 1)) fun (x : Fin (2 * n + 1)) => q) = ((-1) ^ n * q ^ (2 * n + 1) / (2 * n + 1).factorial / q) q

The odd terms of expSeries are real, and correspond to the series for $\frac{q}{‖q‖} \sin ‖q‖$.

theorem Quaternion.hasSum_expSeries_of_imaginary {q : } (hq : q.re = 0) {c : } {s : } (hc : HasSum (fun (n : ) => (-1) ^ n * q ^ (2 * n) / (2 * n).factorial) c) (hs : HasSum (fun (n : ) => (-1) ^ n * q ^ (2 * n + 1) / (2 * n + 1).factorial) s) :
HasSum (fun (n : ) => () fun (x : Fin n) => q) (c + (s / q) q)

Auxiliary result; if the power series corresponding to Real.cos and Real.sin evaluated at ‖q‖ tend to c and s, then the exponential series tends to c + (s / ‖q‖).

theorem Quaternion.exp_of_re_eq_zero (q : ) (hq : q.re = 0) :
= q.cos + (q.sin / q) q

The closed form for the quaternion exponential on imaginary quaternions.

theorem Quaternion.exp_eq (q : ) :
= NormedSpace.exp q.re (q.im.cos + (q.im.sin / q.im) q.im)

The closed form for the quaternion exponential on arbitrary quaternions.

theorem Quaternion.re_exp (q : ) :
().re = NormedSpace.exp q.re * q - q.re.cos
theorem Quaternion.im_exp (q : ) :
().im = (NormedSpace.exp q.re * (q.im.sin / q.im)) q.im
theorem Quaternion.normSq_exp (q : ) :
Quaternion.normSq () = NormedSpace.exp q.re ^ 2
@[simp]
theorem Quaternion.norm_exp (q : ) :

Note that this implies that exponentials of pure imaginary quaternions are unit quaternions since in that case the RHS is 1 via NormedSpace.exp_zero and norm_one.