English
If q is imaginary (real part zero), then the even-degree terms of expSeries along q are real and equal to (-1)^n ||q||^{2n}/(2n)!, embedded as real scalars.
Русский
Если q чисто мнимое (re q = 0), то чётные члены экспонентной серии вдоль q равны действительным числам (-1)^n ||q||^{2n}/(2n)!, встроенным как вещественные скаляры.
LaTeX
$$$\mathrm{expSeries}_{2n}(q) = \iota\Bigg((-1)^{n} \frac{\|q\|^{2n}}{(2n)!}\Bigg).$$$
Lean4
/-- The even terms of `expSeries` are real, and correspond to the series for $\cos ‖q‖$. -/
theorem expSeries_even_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) (n : ℕ) :
expSeries ℝ (Quaternion ℝ) (2 * n) (fun _ => q) = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / (2 * n)!) :=
by
rw [expSeries_apply_eq]
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
letI k : ℝ := ↑(2 * n)!
calc
k⁻¹ • q ^ (2 * n) = k⁻¹ • (-normSq q) ^ n := by rw [pow_mul, hq2]
_ = k⁻¹ • ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) := ?_
_ = ↑((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / k) := ?_
· congr 1
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq]
push_cast
rfl
· rw [← coe_mul_eq_smul, div_eq_mul_inv]
norm_cast
ring_nf
