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 #

@[simp, norm_cast]
theorem quaternion.exp_coe (r : ) :
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‖).

The closed form for the quaternion exponential on imaginary quaternions.

The closed form for the quaternion exponential on arbitrary quaternions.

@[simp]

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.