Quaternion.exp_eq
theorem Quaternion.exp_eq :
∀ (q : Quaternion ℝ), NormedSpace.exp ℝ q = NormedSpace.exp ℝ q.re • (↑‖q.im‖.cos + (‖q.im‖.sin / ‖q.im‖) • q.im)
The given theorem provides a closed form for the exponential of an arbitrary quaternion. Specifically, it states that for any quaternion `q`, the exponential of `q` in the normed space over real numbers is equal to the exponential of the real part of `q` scaled by the sum of the real cosine of the norm of the imaginary part of `q` and the real sine of the norm of the imaginary part of `q` divided by the norm of the imaginary part of `q` itself, this whole sum being further scaled by the imaginary component of `q`. This result can be expressed mathematically as: `exp(q) = exp(Re(q)) * (cos(‖Im(q)‖) + sin(‖Im(q)‖) / ‖Im(q)‖ * Im(q))`.
More concisely: The exponential of a quaternion q is equal to the exponential of its real part scaled by the cosine and sine of its imaginary part's norm, multiplied by the imaginary part itself: exp(q) = exp(Re(q)) * (cos(‖Im(q)‖) + sin(‖Im(q)‖)/‖Im(q)‖ * Im(q)).
|
Quaternion.exp_of_re_eq_zero
theorem Quaternion.exp_of_re_eq_zero :
∀ (q : Quaternion ℝ), q.re = 0 → NormedSpace.exp ℝ q = ↑‖q‖.cos + (‖q‖.sin / ‖q‖) • q
This theorem states that for any quaternion `q` over the real numbers, if the real part `re` of `q` is zero (meaning `q` is an imaginary quaternion), then the exponential of `q` in the quaternion space can be given by a closed form expression. Specifically, the quaternion exponential of `q` is equal to the cosine of the norm of `q` (denoted as `‖q‖.cos`) plus the quotient of the sine of the norm of `q` and the norm of `q` (denoted as `‖q‖.sin / ‖q‖`) all scaled by `q` (denoted as `(‖q‖.sin / ‖q‖) • q`).
More concisely: For any imaginary quaternion `q` over the real numbers, the exponential of `q` in the quaternion space equals `cos(‖q‖) * 1 + sin(‖q‖) / ‖q‖ * q`, where `‖q‖` denotes the norm of `q`.
|
Quaternion.expSeries_odd_of_imaginary
theorem Quaternion.expSeries_odd_of_imaginary :
∀ {q : Quaternion ℝ},
q.re = 0 →
∀ (n : ℕ),
((NormedSpace.expSeries ℝ (Quaternion ℝ) (2 * n + 1)) fun x => q) =
((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1).factorial / ‖q‖) • q
This theorem states that for every quaternion `q` with real part equal to zero, the odd-indexed terms of the `expSeries` for the real numbers and the quaternions, evaluated at `q`, are real and align with the series for the normalized quaternion times the sine of the norm of the quaternion. More concretely, the (2n+1)-th term of the `expSeries` is equal to `((-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1).factorial / ‖q‖) • q`, where `n` is a natural number, `‖q‖` represents the norm of `q`, and `•` signifies scalar multiplication.
More concisely: For every quaternion q with real part equal to zero, the odd-indexed terms of its expSeries align with the series for the real number abs(q) multiplied by the sine of q's norm. That is, ((-1) ^ n * (||q|| ^ (2 * n + 1) / (2 * n + 1)!) * q) equals the (2n+1)-th term of q's expSeries.
|
Quaternion.hasSum_expSeries_of_imaginary
theorem Quaternion.hasSum_expSeries_of_imaginary :
∀ {q : Quaternion ℝ},
q.re = 0 →
∀ {c s : ℝ},
HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n).factorial) c →
HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1).factorial) s →
HasSum (fun n => (NormedSpace.expSeries ℝ (Quaternion ℝ) n) fun x => q) (↑c + (s / ‖q‖) • q)
This theorem states that for any quaternion `q` with real part equal to zero, if the power series corresponding to the `Real.cos` and `Real.sin` functions evaluated at the norm of `q` converge to some real numbers `c` and `s` respectively, then the exponential series evaluated at `q` converges to the quaternion `c + (s / ‖q‖) * q`. Here, the exponential series is defined according to the `NormedSpace.expSeries` definition given above. This theorem provides an auxiliary result in the study of quaternions and their associated exponential series.
More concisely: For any quaternion `q` with real part zero, if the power series of `Real.cos` and `Real.sin` at `‖q‖` converge to real numbers `c` and `s`, respectively, then the exponential series of `q` converges to the quaternion `c + (s / ‖q‖) * q`.
|
Quaternion.norm_exp
theorem Quaternion.norm_exp : ∀ (q : Quaternion ℝ), ‖NormedSpace.exp ℝ q‖ = ‖NormedSpace.exp ℝ q.re‖
This theorem states that the norm of the exponential of a quaternion `q` over the real numbers (`Quaternion ℝ`), obtained through the `NormedSpace.exp` function, is equal to the norm of the exponential of the real part of the quaternion (`q.re`). Note that this implies that the exponentials of pure imaginary quaternions are unit quaternions, since in the case of pure imaginary quaternions, the right-hand side becomes `1` via `NormedSpace.exp_zero` and `norm_one`.
More concisely: The norm of the exponential of a quaternion equals the norm of its real part for all quaternions in `Quaternion ℝ`. In other words, `NormedSpace.exp (Quaternion.re q) = NormedSpace.norm (NormedSpace.exp q)` for all `q` in `Quaternion ℝ`.
|
Quaternion.expSeries_even_of_imaginary
theorem Quaternion.expSeries_even_of_imaginary :
∀ {q : Quaternion ℝ},
q.re = 0 →
∀ (n : ℕ),
((NormedSpace.expSeries ℝ (Quaternion ℝ) (2 * n)) fun x => q) =
↑((-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n).factorial)
The theorem `Quaternion.expSeries_even_of_imaginary` states that for any quaternion `q` of real numbers where the real part is zero, the even terms of the exponential series `expSeries` are real and equal to the series for cosine of the quaternion norm. More precisely, the 2*n-th term of `expSeries` applied to `q` equals `(-1)^n * ‖q‖^(2*n) / (2*n)!`, where `n` is a non-negative integer, `^` denotes exponentiation, `‖q‖` is the norm of `q`, and `!` denotes factorial. This series is the same as the real series for cosine of the norm of the quaternion.
More concisely: For any imaginary quaternion q with real part 0, the even terms of its exponential series equal the real series for the cosine of its norm.
|