feat(analysis/normed_space/quaternion_exponential): lemmas about the …

…quaternion exponential (#18349)

This gives the result that $\exp q = \exp r (\cos \|v\| + \frac{v}{\|v\|} \sin \|v\|)$ where $r$ is the real part and $v$ the imaginary part.

After adding some missing algebraic lemmas, the result that $\|\exp q\| = \|\exp r\|$ is then simple.

src/algebra/quaternion.lean

@@ -415,13 +415,20 @@ lemma eq_re_iff_mem_range_coe {a : ℍ[R, c₁, c₂]} :
   a = a.re ↔ a ∈ set.range (coe : R → ℍ[R, c₁, c₂]) :=
 ⟨λ h, ⟨a.re, h.symm⟩, λ ⟨x, h⟩, eq_re_of_eq_coe h.symm⟩
 
+section char_zero
+variables [no_zero_divisors R] [char_zero R]
+
 @[simp]
-lemma conj_fixed {R : Type*} [comm_ring R] [no_zero_divisors R] [char_zero R]
-  {c₁ c₂ : R} {a : ℍ[R, c₁, c₂]} :
+lemma conj_eq_self {c₁ c₂ : R} {a : ℍ[R, c₁, c₂]} :
   conj a = a ↔ a = a.re :=
 by simp [ext_iff, neg_eq_iff_add_eq_zero, add_self_eq_zero]
 
--- Can't use `rw ← conj_fixed` in the proof without additional assumptions
+lemma conj_eq_neg {c₁ c₂ : R} {a : ℍ[R, c₁, c₂]} :
+  conj a = -a ↔ a.re = 0 :=
+by simp [ext_iff, eq_neg_iff_add_eq_zero]
+
+end char_zero
+-- Can't use `rw ← conj_eq_self` in the proof without additional assumptions
 
 lemma conj_mul_eq_coe : conj a * a = (conj a * a).re := by ext; simp; ring_exp
 
@@ -687,9 +694,14 @@ quaternion_algebra.eq_re_of_eq_coe h
 lemma eq_re_iff_mem_range_coe {a : ℍ[R]} : a = a.re ↔ a ∈ set.range (coe : R → ℍ[R]) :=
 quaternion_algebra.eq_re_iff_mem_range_coe
 
-@[simp] lemma conj_fixed {R : Type*} [comm_ring R] [no_zero_divisors R] [char_zero R] {a : ℍ[R]} :
-  conj a = a ↔ a = a.re :=
-quaternion_algebra.conj_fixed
+section char_zero
+variables [no_zero_divisors R] [char_zero R]
+
+@[simp] lemma conj_eq_self {a : ℍ[R]} : conj a = a ↔ a = a.re := quaternion_algebra.conj_eq_self
+
+@[simp] lemma conj_eq_neg {a : ℍ[R]} : conj a = -a ↔ a.re = 0 := quaternion_algebra.conj_eq_neg
+
+end char_zero
 
 lemma conj_mul_eq_coe : conj a * a = (conj a * a).re := a.conj_mul_eq_coe
 
@@ -749,6 +761,16 @@ lemma coe_norm_sq_add :
   (norm_sq (a + b) : ℍ[R]) = norm_sq a + a * b.conj + b * a.conj + norm_sq b :=
 by simp [← self_mul_conj, mul_add, add_mul, add_assoc]
 
+lemma norm_sq_smul (r : R) (q : ℍ[R]) : norm_sq (r • q) = r^2 * norm_sq q :=
+by simp_rw [norm_sq_def, conj_smul, smul_mul_smul, smul_re, sq, smul_eq_mul]
+
+lemma norm_sq_add (a b : ℍ[R]) : norm_sq (a + b) = norm_sq a + norm_sq b + 2 * (a * conj b).re :=
+calc norm_sq (a + b) = (norm_sq a + (a * conj b).re) + ((b * conj a).re + norm_sq b)
+                     : by simp_rw [norm_sq_def, conj_add, add_mul, mul_add, add_re]
+                 ... = norm_sq a + norm_sq b + ((a * conj b).re + (b * conj a).re) : by abel
+                 ... = norm_sq a + norm_sq b + 2 * (a * conj b).re
+                     : by rw [←add_re, ←conj_mul_conj a b, self_add_conj', coe_re]
+
 end quaternion
 
 namespace quaternion
@@ -787,6 +809,22 @@ instance : no_zero_divisors ℍ[R] :=
 instance : is_domain ℍ[R] :=
 no_zero_divisors.to_is_domain _
 
+lemma sq_eq_norm_sq : a^2 = norm_sq a ↔ a = a.re :=
+begin
+  simp_rw [←conj_eq_self],
+  obtain rfl | hq0 := eq_or_ne a 0,
+  { simp },
+  { rw [←conj_mul_self, sq, mul_left_inj' hq0, eq_comm] }
+end
+
+lemma sq_eq_neg_norm_sq : a^2 = -norm_sq a ↔ a.re = 0 :=
+begin
+  simp_rw [←conj_eq_neg],
+  obtain rfl | hq0 := eq_or_ne a 0,
+  { simp },
+  rw [←conj_mul_self, ←mul_neg, ←neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm],
+end
+
 end linear_ordered_comm_ring
 
 section field

src/analysis/normed_space/exponential.lean

@@ -99,18 +99,17 @@ tsum_congr (λ n, exp_series_apply_eq x n)
 lemma exp_eq_tsum : exp 𝕂 = (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) :=
 funext exp_series_sum_eq
 
-@[simp] lemma exp_zero [t2_space 𝔸] : exp 𝕂 (0 : 𝔸) = 1 :=
+lemma exp_series_apply_zero (n : ℕ) : exp_series 𝕂 𝔸 n (λ _, (0 : 𝔸)) = pi.single 0 1 n :=
 begin
-  suffices : (λ x : 𝔸, ∑' (n : ℕ), (n!⁻¹ : 𝕂) • x^n) 0 = ∑' (n : ℕ), if n = 0 then 1 else 0,
-  { have key : ∀ n ∉ ({0} : finset ℕ), (if n = 0 then (1 : 𝔸) else 0) = 0,
-      from λ n hn, if_neg (finset.not_mem_singleton.mp hn),
-    rw [exp_eq_tsum, this, tsum_eq_sum key, finset.sum_singleton],
-    simp },
-  refine tsum_congr (λ n, _),
-  split_ifs with h h;
-  simp [h]
+  rw exp_series_apply_eq,
+  cases n,
+  { rw [pow_zero, nat.factorial_zero, nat.cast_one, inv_one, one_smul, pi.single_eq_same], },
+  { rw [zero_pow (nat.succ_pos _), smul_zero, pi.single_eq_of_ne (n.succ_ne_zero)], },
 end
 
+@[simp] lemma exp_zero [t2_space 𝔸] : exp 𝕂 (0 : 𝔸) = 1 :=
+by simp_rw [exp_eq_tsum, ←exp_series_apply_eq, exp_series_apply_zero, tsum_pi_single]
+
 @[simp] lemma exp_op [t2_space 𝔸] (x : 𝔸) :
   exp 𝕂 (mul_opposite.op x) = mul_opposite.op (exp 𝕂 x) :=
 by simp_rw [exp, exp_series_sum_eq, ←mul_opposite.op_pow, ←mul_opposite.op_smul, tsum_op]

src/analysis/normed_space/quaternion_exponential.lean

@@ -0,0 +1,134 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import analysis.quaternion
+import analysis.normed_space.exponential
+import analysis.inner_product_space.pi_L2
+import analysis.special_functions.trigonometric.series
+
+/-!
+# Lemmas about `exp` on `quaternion`s
+
+This file contains results about `exp` on `quaternion ℝ`.
+
+## Main results
+
+* `quaternion.exp_eq`: the general expansion of the quaternion exponential in terms of `real.cos`
+  and `real.sin`.
+* `quaternion.exp_of_re_eq_zero`: the special case when the quaternion has a zero real part.
+* `quaternion.norm_exp`: the norm of the quaternion exponential is the norm of the exponential of
+  the real part.
+
+-/
+
+open_locale quaternion nat
+
+namespace quaternion
+
+lemma conj_exp (q : ℍ[ℝ]) : conj (exp ℝ q) = exp ℝ (conj q) := star_exp q
+
+@[simp, norm_cast] lemma exp_coe (r : ℝ) : exp ℝ (r : ℍ[ℝ]) = ↑(exp ℝ r) :=
+(map_exp ℝ (algebra_map ℝ ℍ[ℝ]) (continuous_algebra_map _ _) _).symm
+
+/-- 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‖)`. -/
+lemma has_sum_exp_series_of_imaginary
+  {q : quaternion ℝ} (hq : q.re = 0) {c s : ℝ}
+  (hc : has_sum (λ n, (-1)^n * ‖q‖^(2 * n) / (2 * n)!) c)
+  (hs : has_sum (λ n, (-1)^n * ‖q‖^(2 * n + 1) / (2 * n + 1)!) s) :
+  has_sum (λ n, exp_series ℝ _ n (λ _, q)) (↑c + (s / ‖q‖) • q) :=
+begin
+  replace hc := has_sum_coe.mpr hc,
+  replace hs := (hs.div_const ‖q‖).smul_const q,
+  obtain rfl | hq0 := eq_or_ne q 0,
+  { simp_rw [exp_series_apply_zero, norm_zero, div_zero, zero_smul, add_zero],
+    simp_rw [norm_zero] at hc,
+    convert hc,
+    ext (_ | n) : 1,
+    { rw [pow_zero, 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 exp_series_apply_eq,
+  have hq2 : q^2 = -norm_sq q := sq_eq_neg_norm_sq.mpr hq,
+  have hqn := norm_ne_zero_iff.mpr hq0,
+  refine has_sum.even_add_odd _ _,
+  { convert hc using 1,
+    ext n : 1,
+    let k : ℝ := ↑(2 * n)!,
+    calc k⁻¹ • q ^ (2 * n)
+        = k⁻¹ • ((-norm_sq q) ^ n) : by rw [pow_mul, hq2]
+    ... = k⁻¹ • ↑((-1) ^ n * ‖q‖ ^ (2 * n)) : _
+    ... = ↑((-1) ^ n * ‖q‖ ^ (2 * n) / k) : _,
+    { congr' 1,
+      rw [neg_pow, norm_sq_eq_norm_sq, pow_mul, sq],
+      push_cast },
+    { rw [←coe_mul_eq_smul, div_eq_mul_inv],
+      norm_cast,
+      ring_nf } },
+  { convert hs using 1,
+    ext n : 1,
+    let k : ℝ := ↑(2 * n + 1)!,
+    calc k⁻¹ • q ^ (2 * n + 1)
+        = k⁻¹ • ((-norm_sq 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, norm_sq_eq_norm_sq, pow_mul, sq, ←coe_mul_eq_smul],
+      push_cast },
+    { rw smul_smul,
+      congr' 1,
+      simp_rw [pow_succ', mul_div_assoc, div_div_cancel_left' hqn],
+      ring } },
+end
+
+/-- The closed form for the quaternion exponential on imaginary quaternions. -/
+lemma exp_of_re_eq_zero (q : quaternion ℝ) (hq : q.re = 0) :
+  exp ℝ q = ↑(real.cos ‖q‖) + (real.sin ‖q‖ / ‖q‖) • q :=
+begin
+  rw [exp_eq_tsum],
+  refine has_sum.tsum_eq _,
+  simp_rw ← exp_series_apply_eq,
+  exact has_sum_exp_series_of_imaginary hq (real.has_sum_cos _) (real.has_sum_sin _),
+end
+
+/-- The closed form for the quaternion exponential on arbitrary quaternions. -/
+lemma exp_eq (q : quaternion ℝ) :
+  exp ℝ q = exp ℝ q.re • (↑(real.cos ‖q.im‖) + (real.sin ‖q.im‖ / ‖q.im‖) • q.im) :=
+begin
+  rw [←exp_of_re_eq_zero q.im q.im_re, ←coe_mul_eq_smul, ←exp_coe, ←exp_add_of_commute, re_add_im],
+  exact algebra.commutes q.re (_ : ℍ[ℝ]),
+end
+
+lemma re_exp (q : ℍ[ℝ]) : (exp ℝ q).re = exp ℝ q.re * (real.cos ‖q - q.re‖) :=
+by simp [exp_eq]
+
+lemma im_exp (q : ℍ[ℝ]) : (exp ℝ q).im = (exp ℝ q.re * (real.sin ‖q.im‖ / ‖q.im‖)) • q.im :=
+by simp [exp_eq, smul_smul]
+
+lemma norm_sq_exp (q : ℍ[ℝ]) : norm_sq (exp ℝ q) = (exp ℝ q.re)^2 :=
+calc norm_sq (exp ℝ q)
+    = norm_sq (exp ℝ q.re • (↑(real.cos ‖q.im‖) + (real.sin ‖q.im‖ / ‖q.im‖) • q.im))
+    : by rw exp_eq
+... = (exp ℝ q.re)^2 * norm_sq ((↑(real.cos ‖q.im‖) + (real.sin ‖q.im‖ / ‖q.im‖) • q.im))
+    : by rw [norm_sq_smul]
+... = (exp ℝ q.re)^2 * ((real.cos ‖q.im‖) ^ 2 + (real.sin ‖q.im‖)^2)
+    : begin
+      congr' 1,
+      obtain hv | hv := eq_or_ne (‖q.im‖) 0,
+      { simp [hv] },
+      rw [norm_sq_add, norm_sq_smul, conj_smul, coe_mul_eq_smul, smul_re, smul_re, conj_re, im_re,
+        smul_zero, smul_zero, mul_zero, add_zero, div_pow, norm_sq_coe, norm_sq_eq_norm_sq, ←sq,
+        div_mul_cancel _ (pow_ne_zero _ hv)],
+    end
+... = (exp ℝ q.re)^2 : by rw [real.cos_sq_add_sin_sq, mul_one]
+
+/-- Note that this implies that exponentials of pure imaginary quaternions are unit quaternions
+since in that case the RHS is `1` via `exp_zero` and `norm_one`. -/
+@[simp] lemma norm_exp (q : ℍ[ℝ]) : ‖exp ℝ q‖ = ‖exp ℝ q.re‖ :=
+by rw [norm_eq_sqrt_real_inner (exp ℝ q), inner_self, norm_sq_exp, real.sqrt_sq_eq_abs,
+  real.norm_eq_abs]
+
+end quaternion

src/analysis/quaternion.lean

@@ -157,4 +157,29 @@ begin
   exact (complete_space_congr this).1 (by apply_instance)
 end
 
+section infinite_sum
+variables {α : Type*}
+
+@[simp, norm_cast] lemma has_sum_coe {f : α → ℝ} {r : ℝ} :
+  has_sum (λ a, (f a : ℍ)) (↑r : ℍ) ↔ has_sum f r :=
+⟨λ h, by simpa only using
+  h.map (show ℍ →ₗ[ℝ] ℝ, from quaternion_algebra.re_lm _ _) continuous_re,
+  λ h, by simpa only using h.map (algebra_map ℝ ℍ) (continuous_algebra_map _ _)⟩
+
+@[simp, norm_cast]
+lemma summable_coe {f : α → ℝ} : summable (λ a, (f a : ℍ)) ↔ summable f :=
+by simpa only using summable.map_iff_of_left_inverse (algebra_map ℝ ℍ)
+  (show ℍ →ₗ[ℝ] ℝ, from quaternion_algebra.re_lm _ _)
+  (continuous_algebra_map _ _) continuous_re coe_re
+
+@[norm_cast] lemma tsum_coe (f : α → ℝ) : ∑' a, (f a : ℍ) = ↑(∑' a, f a) :=
+begin
+  by_cases hf : summable f,
+  { exact (has_sum_coe.mpr hf.has_sum).tsum_eq, },
+  { simp [tsum_eq_zero_of_not_summable hf,
+      tsum_eq_zero_of_not_summable (summable_coe.not.mpr hf)] },
+end
+
+end infinite_sum
+
 end quaternion