Lemmas about NormedSpace.exp
on Quaternion
s #
This file contains results about NormedSpace.exp
on Quaternion ℝ
.
Main results #
Quaternion.exp_eq
: the general expansion of the quaternion exponential in terms ofReal.cos
andReal.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.
The odd terms of expSeries
are real, and correspond to the series for
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)
:
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.re_exp
(q : Quaternion ℝ)
:
(NormedSpace.exp ℝ q).re = NormedSpace.exp ℝ q.re * Real.cos ‖q - ↑q.re‖
theorem
Quaternion.normSq_exp
(q : Quaternion ℝ)
:
Quaternion.normSq (NormedSpace.exp ℝ q) = NormedSpace.exp ℝ q.re ^ 2
@[simp]
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
.