Lemmas about exp on Quaternions

This file contains results about 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 : ℝ) : exp ℝ ↑r = ↑(exp ℝ r)

theorem Quaternion.hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c : ℝ} {s : ℝ} (hc : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(Nat.factorial (2 * n))) c) (hs : HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(Nat.factorial (2 * n + 1))) s) : HasSum (fun n => ↑(expSeries ℝ (Quaternion ℝ) n) fun x => 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 : Quaternion ℝ) (hq : q.re = 0) : exp ℝ q = ↑(Real.cos ‖q‖) + (Real.sin ‖q‖ / ‖q‖) • q

The closed form for the quaternion exponential on imaginary quaternions.

theorem Quaternion.exp_eq (q : Quaternion ℝ) : exp ℝ q = exp ℝ q.re • (↑(Real.cos ‖Quaternion.im q‖) + (Real.sin ‖Quaternion.im q‖ / ‖Quaternion.im q‖) • Quaternion.im q)

The closed form for the quaternion exponential on arbitrary quaternions.

theorem Quaternion.re_exp (q : Quaternion ℝ) : (exp ℝ q).re = exp ℝ q.re * Real.cos ‖q - ↑q.re‖

theorem Quaternion.im_exp (q : Quaternion ℝ) : Quaternion.im (exp ℝ q) = (exp ℝ q.re * (Real.sin ‖Quaternion.im q‖ / ‖Quaternion.im q‖)) • Quaternion.im q

theorem Quaternion.normSq_exp (q : Quaternion ℝ) : ↑Quaternion.normSq (exp ℝ q) = exp ℝ q.re ^ 2

@[simp]

theorem Quaternion.norm_exp (q : Quaternion ℝ) : ‖exp ℝ q‖ = ‖exp ℝ q.re‖

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