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 : ℝ) : NormedSpace.exp ℝ ↑r = ↑(NormedSpace.exp ℝ r)

theorem Quaternion.expSeries_even_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) (n : ℕ) : ((NormedSpace.expSeries ℝ (Quaternion ℝ) (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 : Quaternion ℝ} (hq : q.re = 0) (n : ℕ) : ((NormedSpace.expSeries ℝ (Quaternion ℝ) (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 : Quaternion ℝ} (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 : ℕ) => (NormedSpace.expSeries ℝ (Quaternion ℝ) 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 : Quaternion ℝ) (hq : q.re = 0) : NormedSpace.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 ℝ) : NormedSpace.exp ℝ q = NormedSpace.exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)

The closed form for the quaternion exponential on arbitrary quaternions.

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

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

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

@[simp]

theorem Quaternion.norm_exp (q : Quaternion ℝ) : ‖NormedSpace.exp ℝ q‖ = ‖NormedSpace.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 NormedSpace.exp_zero and norm_one.