Documentation

Mathlib.Analysis.Quaternion

Quaternions as a normed algebra #

In this file we define the following structures on the space ℍ := ℍ[ℝ] of quaternions:

We show that the norm on ℍ[ℝ] agrees with the euclidean norm of its components.

Notation #

The following notation is available with open Quaternion or open scoped Quaternion:

Tags #

quaternion, normed ring, normed space, normed algebra

source
def Quaternion.termℍ :
Lean.ParserDescr

Space of quaternions over a type, denoted as ℍ[R]. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Equations
Instances For
    source
    instance Quaternion.instInnerReal :
    Inner ℝ (Quaternion ℝ)
    Equations
    source
    theorem Quaternion.inner_self (a : Quaternion ℝ) :
    inner a a = normSq a
    source
    theorem Quaternion.inner_def (a b : Quaternion ℝ) :
    inner a b = (a * star b).re
    source
    noncomputable instance Quaternion.instNormedAddCommGroupReal :
    NormedAddCommGroup (Quaternion ℝ)
    Equations
    source
    noncomputable instance Quaternion.instInnerProductSpaceReal :
    InnerProductSpace ℝ (Quaternion ℝ)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem Quaternion.normSq_eq_norm_mul_self (a : Quaternion ℝ) :
    normSq a = ‖a‖ * ‖a‖
    source
    instance Quaternion.instNormOneClassReal :
    NormOneClass (Quaternion ℝ)
    source
    @[simp]
    theorem Quaternion.norm_coe (a : ℝ) :
    ‖↑a‖ = ‖a‖
    source
    @[simp]
    theorem Quaternion.nnnorm_coe (a : ℝ) :
    ‖↑a‖₊ = ‖a‖₊
    source
    @[simp]
    theorem Quaternion.norm_star (a : Quaternion ℝ) :
    ‖star a‖ = ‖a‖
    source
    @[simp]
    theorem Quaternion.nnnorm_star (a : Quaternion ℝ) :
    ‖star a‖₊ = ‖a‖₊
    source
    noncomputable instance Quaternion.instNormedDivisionRingReal :
    NormedDivisionRing (Quaternion ℝ)
    Equations
    source
    noncomputable instance Quaternion.instNormedAlgebraReal :
    NormedAlgebra ℝ (Quaternion ℝ)
    Equations
    source
    instance Quaternion.instCStarRingReal :
    CStarRing (Quaternion ℝ)
    source
    def Quaternion.coeComplex (z : ℂ) :
    Quaternion ℝ

    Coercion from ℂ to ℍ.

    Equations
    • ↑z = { re := z.re, imI := z.im, imJ := 0, imK := 0 }
    Instances For
      source
      instance Quaternion.instCoeComplexReal :
      Coe ℂ (Quaternion ℝ)
      Equations
      source
      @[simp]
      theorem Quaternion.coeComplex_re (z : ℂ) :
      (↑z).re = z.re
      source
      @[simp]
      theorem Quaternion.coeComplex_imI (z : ℂ) :
      (↑z).imI = z.im
      source
      @[simp]
      theorem Quaternion.coeComplex_imJ (z : ℂ) :
      (↑z).imJ = 0
      source
      @[simp]
      theorem Quaternion.coeComplex_imK (z : ℂ) :
      (↑z).imK = 0
      source
      @[simp]
      theorem Quaternion.coeComplex_add (z w : ℂ) :
      ↑(z + w) = ↑z + ↑w
      source
      @[simp]
      theorem Quaternion.coeComplex_mul (z w : ℂ) :
      ↑(z * w) = ↑z * ↑w
      source
      @[simp]
      theorem Quaternion.coeComplex_zero :
      ↑0 = 0
      source
      @[simp]
      theorem Quaternion.coeComplex_one :
      ↑1 = 1
      source
      @[simp]
      theorem Quaternion.coe_real_complex_mul (r : ℝ) (z : ℂ) :
      r • ↑z = ↑r * ↑z
      source
      @[simp]
      theorem Quaternion.coeComplex_coe (r : ℝ) :
      ↑↑r = ↑r
      source
      def Quaternion.ofComplex :
      ℂ →ₐ[ℝ] Quaternion ℝ

      Coercion ℂ →ₐ[ℝ] ℍ as an algebra homomorphism.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Quaternion.coe_ofComplex :
        ⇑ofComplex = coeComplex
        source
        theorem Quaternion.norm_piLp_equiv_symm_equivTuple (x : Quaternion ℝ) :
        ‖(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x)‖ = ‖x‖

        The norm of the components as a euclidean vector equals the norm of the quaternion.

        source
        noncomputable def Quaternion.linearIsometryEquivTuple :
        Quaternion ℝ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4)

        QuaternionAlgebra.linearEquivTuple as a LinearIsometryEquiv.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem Quaternion.linearIsometryEquivTuple_apply (a : Quaternion ℝ) :
          linearIsometryEquivTuple a = !₂[a.re, a.imI, a.imJ, a.imK]
          source
          @[simp]
          theorem Quaternion.linearIsometryEquivTuple_symm_apply (a : EuclideanSpace ℝ (Fin 4)) :
          linearIsometryEquivTuple.symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
          source
          theorem Quaternion.continuous_coe :
          Continuous coe
          source
          theorem Quaternion.continuous_normSq :
          Continuous ⇑normSq
          source
          theorem Quaternion.continuous_re :
          Continuous fun (q : Quaternion ℝ) => q.re
          source
          theorem Quaternion.continuous_imI :
          Continuous fun (q : Quaternion ℝ) => q.imI
          source
          theorem Quaternion.continuous_imJ :
          Continuous fun (q : Quaternion ℝ) => q.imJ
          source
          theorem Quaternion.continuous_imK :
          Continuous fun (q : Quaternion ℝ) => q.imK
          source
          theorem Quaternion.continuous_im :
          Continuous fun (q : Quaternion ℝ) => q.im
          source
          instance Quaternion.instCompleteSpaceReal :
          CompleteSpace (Quaternion ℝ)
          source
          @[simp]
          theorem Quaternion.hasSum_coe {α : Type u_1} {f : α → ℝ} {r : ℝ} :
          HasSum (fun (a : α) => ↑(f a)) ↑r ↔ HasSum f r
          source
          @[simp]
          theorem Quaternion.summable_coe {α : Type u_1} {f : α → ℝ} :
          (Summable fun (a : α) => ↑(f a)) ↔ Summable f
          source
          theorem Quaternion.tsum_coe {α : Type u_1} (f : α → ℝ) :
          ∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)