Documentation

Mathlib.Analysis.Normed.Algebra.QuaternionExponential

Lemmas about NormedSpace.exp on Quaternions #

This file contains results about NormedSpace.exp on Quaternion.

Main results #

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‖).

The closed form for the quaternion exponential on imaginary quaternions.

The closed form for the quaternion exponential on arbitrary quaternions.

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.