English
If q is imaginary (re q = 0), then odd-degree terms of expSeries along q are proportional to q with the coefficient ((-1)^n ||q||^{2n+1})/((2n+1)! ||q||).
Русский
Если q чисто мнимое (re q = 0), то нечётные члены expSeries вдоль q пропорциональны q: ((-1)^n ||q||^{2n+1})/((2n+1)! ||q||) · q.
LaTeX
$$$\mathrm{expSeries}_{2n+1}(q) = \left((-1)^n \frac{\|q\|^{2n+1}}{(2n+1)\!\,\|q\|}\right) \cdot q.$$$
Lean4
/-- The odd terms of `expSeries` are real, and correspond to the series for
$\frac{q}{‖q‖} \sin ‖q‖$. -/
theorem expSeries_odd_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) (n : ℕ) :
expSeries ℝ (Quaternion ℝ) (2 * n + 1) (fun _ => q) =
(((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / (2 * n + 1)!) / ‖q‖) • q :=
by
rw [expSeries_apply_eq]
obtain rfl | hq0 := eq_or_ne q 0
· simp
have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
have hqn := norm_ne_zero_iff.mpr hq0
let k : ℝ := ↑(2 * n + 1)!
calc
k⁻¹ • q ^ (2 * n + 1) = k⁻¹ • ((-normSq q) ^ n * q) := by rw [pow_succ, pow_mul, hq2]
_ = k⁻¹ • ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n)) • q := ?_
_ = ((-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / k / ‖q‖) • q := ?_
· congr 1
rw [neg_pow, normSq_eq_norm_mul_self, pow_mul, sq, ← coe_mul_eq_smul]
norm_cast
· rw [smul_smul]
congr 1
simp_rw [pow_succ, mul_div_assoc, div_div_cancel_left' hqn]
ring
