Cayley coordinates for three-dimensional rotations

The vector (x, y, z) represents the unit quaternion proportional to (1, x, y, z). Unlike Euler coordinates, the resulting rotation matrix is rational in the three parameters. These coordinates cover exactly the rotations without angle pi; in particular they cover every rotation whose trace is nonnegative.

def Cayley.cayleyDenom (x y z : ℝ) : ℝ

The positive denominator in the three-dimensional Cayley transform.

Equations

• Cayley.cayleyDenom x y z = 1 + x ^ 2 + y ^ 2 + z ^ 2

theorem Cayley.cayleyDenom_pos (x y z : ℝ) : 0 < cayleyDenom x y z

theorem Cayley.cayleyDenom_ne (x y z : ℝ) : cayleyDenom x y z ≠ 0

def Cayley.cayleyNumeratorMatrix {R : Type} [CommRing R] (x y z : R) : Matrix (Fin 3) (Fin 3) R

Polynomial numerator of the Cayley rotation, defined over any commutative ring so rational certificate evaluation uses the same formula.

Equations

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

noncomputable def Cayley.cayleyMatrix (x y z : ℝ) : Matrix (Fin 3) (Fin 3) ℝ

The rational rotation matrix with Cayley vector (x, y, z).

Equations

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

theorem Cayley.cayleyMatrix_eq_div_numerator (x y z : ℝ) : cayleyMatrix x y z = Matrix.of fun (i j : Fin 3) => cayleyNumeratorMatrix x y z i j / cayleyDenom x y z

theorem Cayley.cayleyNumeratorMatrix_eq_denom_smul (x y z : ℝ) : cayleyNumeratorMatrix x y z = cayleyDenom x y z • cayleyMatrix x y z

theorem Cayley.cayleyMatrix_mem_SO3 (x y z : ℝ) : cayleyMatrix x y z ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ

Cayley matrices are orientation-preserving orthogonal matrices.

noncomputable def Cayley.cayleyVector (x y z : ℝ) : Euc(3)

The Euclidean vector represented by the three scalar coordinates.

Equations

• Cayley.cayleyVector x y z = !₂[x, y, z]

theorem Cayley.cayleyMatrix_apply_sub (x y z : ℝ) (v : Euc(3)) : (Matrix.toEuclideanLin (cayleyMatrix x y z)) v - v = (2 / cayleyDenom x y z) • BalancedSupport.cross3 (cayleyVector x y z) v + (2 / cayleyDenom x y z) • BalancedSupport.cross3 (cayleyVector x y z) (BalancedSupport.cross3 (cayleyVector x y z) v)

Exact Rodrigues form of the Cayley transform.

theorem Cayley.cross3_smul_left (c : ℝ) (u v : Euc(3)) : BalancedSupport.cross3 (c • u) v = c • BalancedSupport.cross3 u v

theorem Cayley.cross3_smul_right (c : ℝ) (u v : Euc(3)) : BalancedSupport.cross3 u (c • v) = c • BalancedSupport.cross3 u v

theorem Cayley.cayleyMatrix_smul_unit_apply_sub (c : ℝ) (axis v : Euc(3)) (haxis : ‖axis‖ = 1) : (Matrix.toEuclideanLin (cayleyMatrix (c * axis.ofLp 0) (c * axis.ofLp 1) (c * axis.ofLp 2))) v - v = (2 * c / (1 + c ^ 2)) • BalancedSupport.cross3 axis v + (2 * c ^ 2 / (1 + c ^ 2)) • BalancedSupport.cross3 axis (BalancedSupport.cross3 axis v)

Cayley rotation about a unit axis, written in Rodrigues form.

theorem Cayley.trace_cayleyMatrix (x y z : ℝ) : (cayleyMatrix x y z).trace = (3 - (x ^ 2 + y ^ 2 + z ^ 2)) / cayleyDenom x y z

Trace is a rational function of the squared Cayley radius.

theorem Cayley.BalancedSupport.inner_cross3_cycle (d u v : Euc(3)) : inner ℝ d (cross3 u v) = inner ℝ u (cross3 v d)

theorem Cayley.BalancedSupport.AxisAngle.first_eq_cross3 {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) (v : Euc(3)) : a.first v = cross3 a.axis v

theorem Cayley.BalancedSupport.AxisAngle.first_first {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) (v : Euc(3)) : a.first (a.first v) = a.remainder v

theorem Cayley.BalancedSupport.AxisAngle.remainder_eq_cross3_cross3 {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) (v : Euc(3)) : a.remainder v = cross3 a.axis (cross3 a.axis v)

theorem Cayley.BalancedSupport.AxisAngle.linear_trace_eq {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) : (LinearMap.trace ℝ Euc(3)) ↑Q = 1 + 2 * Real.cos a.angle

Linear trace recovers the cosine of any axis-angle presentation.

theorem Cayley.BalancedSupport.AxisAngle.matrix_trace_eq {A : Matrix (Fin 3) (Fin 3) ℝ} (a : AxisAngle (LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A))) : A.trace = 1 + 2 * Real.cos a.angle

Matrix trace recovers the cosine of an axis-angle presentation.

theorem Cayley.exists_cayleyMatrix_of_trace_nonneg (A : Matrix (Fin 3) (Fin 3) ℝ) (hA : A ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) (htrace : 0 ≤ A.trace) : ∃ (x : ℝ) (y : ℝ) (z : ℝ), x ^ 2 + y ^ 2 + z ^ 2 ≤ 3 ∧ A = cayleyMatrix x y z

Every special orthogonal matrix of nonnegative trace has a Cayley vector of squared radius at most three, giving a closed, bounded Cayley chart for the nonnegative-trace rotations.