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.

Instances For
    source
    @[implicit_reducible]
    instance Quaternion.instInnerReal :
    Inner ℝ (Quaternion ℝ)
    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
    @[implicit_reducible]
    noncomputable instance Quaternion.instNormedAddCommGroupReal :
    NormedAddCommGroup (Quaternion ℝ)
    source
    @[implicit_reducible]
    noncomputable instance Quaternion.instInnerProductSpaceReal :
    InnerProductSpace ℝ (Quaternion ℝ)
    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
    theorem Quaternion.norm_star (a : Quaternion ℝ) :
    ‖star a‖ = ‖a‖
    source
    theorem Quaternion.nnnorm_star (a : Quaternion ℝ) :
    ‖star a‖₊ = ‖a‖₊
    source
    @[implicit_reducible]
    noncomputable instance Quaternion.instNormedDivisionRingReal :
    NormedDivisionRing (Quaternion ℝ)
    source
    @[implicit_reducible]
    noncomputable instance Quaternion.instNormedAlgebraReal :
    NormedAlgebra ℝ (Quaternion ℝ)
    source
    instance Quaternion.instCStarRingReal :
    CStarRing (Quaternion ℝ)
    source
    def Quaternion.coeComplex (z : ℂ) :
    Quaternion ℝ

    Coercion from ℂ to ℍ.

    Instances For
      source
      @[implicit_reducible]
      instance Quaternion.instCoeComplexReal :
      Coe ℂ (Quaternion ℝ)
      source
      @[simp]
      theorem Quaternion.re_coeComplex (z : ℂ) :
      (↑z).re = z.re
      source
      @[simp]
      theorem Quaternion.imI_coeComplex (z : ℂ) :
      (↑z).imI = z.im
      source
      @[simp]
      theorem Quaternion.imJ_coeComplex (z : ℂ) :
      (↑z).imJ = 0
      source
      @[simp]
      theorem Quaternion.imK_coeComplex (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
      noncomputable def Quaternion.ofComplex :
      ℂ →ₐ[ℝ] Quaternion ℝ

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

      Instances For
        source
        @[simp]
        theorem Quaternion.coe_ofComplex :
        ⇑ofComplex = coeComplex
        source
        theorem Quaternion.norm_toLp_equivTuple (x : Quaternion ℝ) :
        ‖WithLp.toLp 2 ((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.

        Instances For
          source
          @[simp]
          theorem Quaternion.linearIsometryEquivTuple_symm_apply (a : EuclideanSpace ℝ (Fin 4)) :
          linearIsometryEquivTuple.symm a = { re := a.ofLp 0, imI := a.ofLp 1, imJ := a.ofLp 2, imK := a.ofLp 3 }
          source
          @[simp]
          theorem Quaternion.linearIsometryEquivTuple_apply (a : Quaternion ℝ) :
          linearIsometryEquivTuple a = !₂[a.re, a.imI, a.imJ, a.imK]
          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} {L : SummationFilter α} {f : α → ℝ} {r : ℝ} :
          HasSum (fun (a : α) => ↑(f a)) (↑r) L ↔ HasSum f r L
          source
          @[simp]
          theorem Quaternion.summable_coe {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} :
          Summable (fun (a : α) => ↑(f a)) L ↔ Summable f L
          source
          theorem Quaternion.tsum_coe {α : Type u_1} {L : SummationFilter α} (f : α → ℝ) :
          ∑'[L] (a : α), ↑(f a) = ↑(∑'[L] (a : α), f a)