English
If q is imaginary and sums c and s are the sums of the even and odd parts respectively, then the total expSeries sum equals c + (s/||q||) q.
Русский
Если q мнимая, и суммы c, s соответствуют чётной и нечётной частям, тогда сумма expSeries даёт c + (s/||q||) q.
LaTeX
$$$\text{HasSum} \;\big(n \mapsto \expSeries_{\mathbb{R}}(\mathbb{H}, q)(n)\big)\; (\uparrow c + (s/\|q\|) \cdot q).$$$
Lean4
/-- 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‖)`. -/
theorem hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c s : ℝ}
(hc : HasSum (fun n => (-1 : ℝ) ^ n * ‖q‖ ^ (2 * n) / (2 * n)!) c)
(hs : HasSum (fun n => (-1 : ℝ) ^ n * ‖q‖ ^ (2 * n + 1) / (2 * n + 1)!) s) :
HasSum (fun n => expSeries ℝ (Quaternion ℝ) n fun _ => q) (↑c + (s / ‖q‖) • q) :=
by
replace hc := hasSum_coe.mpr hc
replace hs := (hs.div_const ‖q‖).smul_const q
refine HasSum.even_add_odd ?_ ?_
· convert hc using 1
ext n : 1
rw [expSeries_even_of_imaginary hq]
· convert hs using 1
ext n : 1
rw [expSeries_odd_of_imaginary hq]
