English
The Euclidean norm of the 4-tuple of quaternion components equals the quaternion norm: for x = a + bi + cj + dk, we have √(a^2 + b^2 + c^2 + d^2) = ∥x∥.
Русский
Евклидова норма четверного вектора компонент кватерниона равна норме самого кватерниона: для x = a + bi + cj + dk имеем √(a^2 + b^2 + c^2 + d^2) = ∥x∥.
LaTeX
$$$\\| (a,b,c,d) \\| = \\sqrt{a^2+b^2+c^2+d^2} = \\| a + b i + c j + d k \\|.$$$
Lean4
/-- The norm of the components as a Euclidean vector equals the norm of the quaternion. -/
theorem norm_toLp_equivTuple (x : ℍ) : ‖WithLp.toLp 2 (equivTuple ℝ x)‖ = ‖x‖ :=
by
rw [norm_eq_sqrt_real_inner, norm_eq_sqrt_real_inner, inner_self, normSq_def', PiLp.inner_apply, Fin.sum_univ_four]
simp_rw [RCLike.inner_apply, starRingEnd_apply, star_trivial, ← sq]
rfl
