Documentation

Cayley.Soundness.QIReal

Real values of the checker's dyadic numbers #

source
noncomputable def Cayley.D (q : QI) :
ℝ

The real value of ⟨m, e⟩ = m / 2^e.

Equations
Instances For
    source
    @[simp]
    theorem Cayley.D_mk (m : ℤ) (e : ℕ) :
    D { m := m, e := e } = ↑m / 2 ^ e
    source
    theorem Cayley.QI.pow2_eq (k : ℕ) :
    pow2 k = 2 ^ k
    source
    @[simp]
    theorem Cayley.D_add (a b : QI) :
    D (a + b) = D a + D b
    source
    @[simp]
    theorem Cayley.D_mul (a b : QI) :
    D (a * b) = D a * D b
    source
    @[simp]
    theorem Cayley.D_neg (a : QI) :
    D (-a) = -D a
    source
    @[simp]
    theorem Cayley.D_sub (a b : QI) :
    D (a - b) = D a - D b
    source
    @[simp]
    theorem Cayley.D_ofNat' (n : ℕ) :
    D (OfNat.ofNat n) = ↑n
    source
    @[simp]
    theorem Cayley.D_zero :
    D 0 = 0
    source
    @[simp]
    theorem Cayley.D_one :
    D 1 = 1
    source
    theorem Cayley.D_errε :
    D errε = 1 / 2 ^ 60
    source
    @[simp]
    theorem Cayley.D_intCast (n : ℤ) :
    D ↑n = ↑n
    source
    theorem Cayley.D_le_iff (a b : QI) :
    D a ≤ D b ↔ a ≤ b
    source
    theorem Cayley.D_lt_iff (a b : QI) :
    D a < D b ↔ a < b
    source
    theorem Cayley.D_d80 (m : ℤ) :
    D (d80 m) = ↑m / 2 ^ 80
    source
    noncomputable def Cayley.V3.toR (v : V3 QI) :
    Fin 3 → ℝ

    Real vector of a constant V3.

    Equations
    Instances For
      source
      noncomputable def Cayley.M3.toR (m : M3 QI) :
      Matrix (Fin 3) (Fin 3) ℝ

      Real matrix of a constant M3.

      Equations
      Instances For
        source
        def Cayley.crossR (a b : Fin 3 → ℝ) :
        Fin 3 → ℝ

        The cross product of real vectors.

        Equations
        Instances For