Quaternion.norm_piLp_equiv_symm_equivTuple
theorem Quaternion.norm_piLp_equiv_symm_equivTuple :
∀ (x : Quaternion ℝ), ‖(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((Quaternion.equivTuple ℝ) x)‖ = ‖x‖
This theorem states that for any quaternion `x` with real components, the norm of the components when considered as a Euclidean vector (obtained by applying the inverse of the equivalence `WithLp.equiv 2 (Fin 4 → ℝ)` to the quaternion transformed into a tuple of 4 real numbers by `Quaternion.equivTuple ℝ`) is equal to the norm of the quaternion `x` itself. This implies the correspondence between the Euclidean norm of the 4-dimensional vector representation of a quaternion and the norm of the quaternion in its original form.
More concisely: The norm of a quaternion with real components, when regarded as a Euclidean vector, is equal to its quaternion norm.
|
Quaternion.inner_self
theorem Quaternion.inner_self : ∀ (a : Quaternion ℝ), ⟪a, a⟫_ℝ = Quaternion.normSq a
This theorem states that for any quaternion `a` over the real numbers, the inner product of `a` with itself is equal to the square of the norm of `a`. In other words, the inner product of a quaternion with itself, denoted as `⟪a, a⟫_ℝ`, always equals the square of its norm, which is computed by the function `Quaternion.normSq a`.
More concisely: For any quaternion `a` over the real numbers, the inner product of `a` with itself equals the square of its norm: `⟪a, a⟫_ℝ = Quaternion.normSq a².`
|
Quaternion.continuous_re
theorem Quaternion.continuous_re : Continuous fun q => q.re
This theorem states that the real part function, which extracts the real part from a quaternion, is a continuous function. This means that for any small change in the input quaternion, there will be correspondingly small changes in its real part, satisfying the formal definition of continuity in the context of mathematical functions.
More concisely: The real part function on quaternions is continuous.
|