mathlib3 documentation

analysis.normed_space.quaternion_exponential

Lemmas about exp on quaternions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains results about exp on quaternion ℝ.

Main results #

source
@[simp, norm_cast]
theorem quaternion.exp_coe (r : ℝ) :
exp ℝ ↑r = ↑(exp ℝ r)
source
theorem quaternion.has_sum_exp_series_of_imaginary {q : quaternion ℝ} (hq : q.re = 0) {c s : ℝ} (hc : has_sum (λ (n : ℕ), (-1) ^ n * ‖q‖ ^ (2 * n) / ↑((2 * n).factorial)) c) (hs : has_sum (λ (n : ℕ), (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑((2 * n + 1).factorial)) s) :
has_sum (λ (n : ℕ), ⇑(exp_series ℝ (quaternion ℝ) n) (λ (_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‖).

source
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.

source
theorem quaternion.exp_eq (q : quaternion ℝ) :
exp ℝ q = 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.

source
theorem quaternion.re_exp (q : quaternion ℝ) :
(exp ℝ q).re = exp ℝ q.re * real.cos ‖q - ↑(q.re)‖
source
theorem quaternion.im_exp (q : quaternion ℝ) :
(exp ℝ q).im = (exp ℝ q.re * (real.sin ‖q.im‖ / ‖q.im‖)) • q.im
source
theorem quaternion.norm_sq_exp (q : quaternion ℝ) :
⇑quaternion.norm_sq (exp ℝ q) = exp ℝ q.re ^ 2
source
@[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.