LeanPool.Rupert.Quaternion

Imported Lean Pool material for LeanPool.Rupert.Quaternion.

def matrixOfQuat {R : Type} [Field R] (q : Quaternion R) : Matrix (Fin 3) (Fin 3) R

Converts a quaternion to a normalized rotation matrix.

Equations

• One or more equations did not get rendered due to their size.

def denormMatrixOfQuat {R : Type} [Field R] (q : Quaternion R) : Matrix (Fin 3) (Fin 3) R

A version of converting quaternions to matrices without normalization, under the assumption that it might be easier to reason about it postponing the divisions until later.

Equations

• One or more equations did not get rendered due to their size.

theorem normalized_denorm_is_matrix {R : Type} [Field R] (q : Quaternion R) : match q with | { re := w, imI := x, imJ := y, imK := z } => have normsq := w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2; matrixOfQuat q = (1 / normsq) • denormMatrixOfQuat q

The normalized quaternion matrix is a scalar multiple of the denormalized matrix.

theorem denorm_half_unitary (q : Quaternion ℝ) : denormMatrixOfQuat q * star (denormMatrixOfQuat q) = Quaternion.normSq q ^ 2 • 1

theorem denorm_half_unitary2 (q : Quaternion ℝ) : star (denormMatrixOfQuat q) * denormMatrixOfQuat q = Quaternion.normSq q ^ 2 • 1

theorem matrixOfQuat_is_unitary (q : Quaternion ℝ) (nz : Quaternion.normSq q ≠ 0) : matrixOfQuat q ∈ Matrix.unitaryGroup (Fin 3) ℝ

theorem denormMatrixOfQuat_has_correct_det (q : Quaternion ℝ) : (denormMatrixOfQuat q).det = Quaternion.normSq q ^ 3

theorem matrixOfQuat_has_det_one (q : Quaternion ℝ) (nz : Quaternion.normSq q ≠ 0) : (matrixOfQuat q).det = 1

theorem matrixOfQuat_is_s03 {q : Quaternion ℝ} (nz : Quaternion.normSq q ≠ 0) : matrixOfQuat q ∈ SO3

noncomputable def rotateXQuat (θ : ℝ) : Quaternion ℝ

Quaternion for rotation about the x-axis by angle θ.

Equations

• rotateXQuat θ = { re := Real.cos (θ / 2), imI := Real.sin (θ / 2), imJ := 0, imK := 0 }

noncomputable def rotateXMat (θ : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

Matrix for rotation about the x-axis by angle θ.

Equations

• rotateXMat θ = !![1, 0, 0; 0, Real.cos θ, -Real.sin θ; 0, Real.sin θ, Real.cos θ]

theorem rotate_x (θ : ℝ) : matrixOfQuat (rotateXQuat θ) = rotateXMat θ

noncomputable def rotateToTarget (src tgt : ℝ³) : Quaternion ℝ

Quaternion rotating src toward tgt.

Equations

• One or more equations did not get rendered due to their size.