English
The squared norm of exp(q) is (exp(re q))^2.
Русский
Квадрат нормы exp(q) равен (exp(re q))^2.
LaTeX
$$$\|\exp_{\mathbb{R}}(q)\|^{2} = (\exp_{\mathbb{R}}(q_{\mathrm{re}}))^{2}.$$$
Lean4
theorem normSq_exp (q : ℍ[ℝ]) : normSq (exp ℝ q) = exp ℝ q.re ^ 2 :=
calc
normSq (exp ℝ q) = normSq (exp ℝ q.re • (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im)) := by rw [exp_eq]
_ = exp ℝ q.re ^ 2 * normSq (↑(Real.cos ‖q.im‖) + (Real.sin ‖q.im‖ / ‖q.im‖) • q.im) := by rw [normSq_smul]
_ = exp ℝ q.re ^ 2 * (Real.cos ‖q.im‖ ^ 2 + Real.sin ‖q.im‖ ^ 2) :=
by
congr 1
obtain hv | hv := eq_or_ne ‖q.im‖ 0
· simp [hv]
rw [normSq_add, normSq_smul, star_smul, coe_mul_eq_smul, re_smul, re_smul, re_star, re_im, smul_zero, smul_zero,
mul_zero, add_zero, div_pow, normSq_coe, normSq_eq_norm_mul_self, ← sq, div_mul_cancel₀ _ (pow_ne_zero _ hv)]
_ = exp ℝ q.re ^ 2 := by rw [Real.cos_sq_add_sin_sq, mul_one]
