chore(Analysis/NormedSpace/QuaternionExponential): extract helper lem…

…mas (#9494)

Besides being split in three, this proof is largely untouched.

Mathlib/Analysis/NormedSpace/QuaternionExponential.lean

@@ -35,6 +35,48 @@ theorem exp_coe (r : ℝ) : exp ℝ (r : ℍ[ℝ]) = ↑(exp ℝ r) :=
   (map_exp ℝ (algebraMap ℝ ℍ[ℝ]) (continuous_algebraMap _ _) _).symm
 #align quaternion.exp_coe Quaternion.exp_coe
 
+/-- 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
+
+/-- 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
+
 /-- 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 : ℝ}
@@ -43,48 +85,13 @@ theorem hasSum_expSeries_of_imaginary {q : Quaternion ℝ} (hq : q.re = 0) {c 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
-  obtain rfl | hq0 := eq_or_ne q 0
-  · simp_rw [expSeries_apply_zero, norm_zero, div_zero, zero_smul, add_zero]
-    simp_rw [norm_zero] at hc
-    convert hc using 1
-    ext (_ | n) : 1
-    · rw [pow_zero, Nat.zero_eq, mul_zero, pow_zero, Nat.factorial_zero, Nat.cast_one,
-        div_one, one_mul, Pi.single_eq_same, coe_one]
-    · rw [zero_pow (mul_pos two_pos (Nat.succ_pos _)), mul_zero, zero_div,
-        Pi.single_eq_of_ne n.succ_ne_zero, coe_zero]
-  simp_rw [expSeries_apply_eq]
-  have hq2 : q ^ 2 = -normSq q := sq_eq_neg_normSq.mpr hq
-  have hqn := norm_ne_zero_iff.mpr hq0
-  refine' HasSum.even_add_odd _ _
+  refine HasSum.even_add_odd ?_ ?_
   · convert hc using 1
     ext n : 1
-    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
+    rw [expSeries_even_of_imaginary hq]
   · convert hs using 1
     ext n : 1
-    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
+    rw [expSeries_odd_of_imaginary hq]
 #align quaternion.has_sum_exp_series_of_imaginary Quaternion.hasSum_expSeries_of_imaginary
 
 /-- The closed form for the quaternion exponential on imaginary quaternions. -/