Exact axis-angle decomposition

The local balanced-support argument needs an exact finite-rotation identity, not an infinitesimal approximation. We obtain it from the existing theorem that every element of SO(3) is orthogonally conjugate to a rotation about the z axis.

noncomputable def Cayley.BalancedSupport.zFirst (v : Euc(3)) : Euc(3)

Equations

• Cayley.BalancedSupport.zFirst v = !₂[-v.ofLp 1, v.ofLp 0, 0]

noncomputable def Cayley.BalancedSupport.zRemainder (v : Euc(3)) : Euc(3)

Equations

• Cayley.BalancedSupport.zRemainder v = !₂[-v.ofLp 0, -v.ofLp 1, 0]

noncomputable def Cayley.BalancedSupport.cross3 (v w : Euc(3)) : Euc(3)

Euclidean-space wrapper for the ordinary three-dimensional cross product.

Equations

• Cayley.BalancedSupport.cross3 v w = WithLp.toLp 2 ((crossProduct v.ofLp) w.ofLp)

noncomputable def Cayley.BalancedSupport.zAxis : Euc(3)

The standard unit z vector.

Equations

• Cayley.BalancedSupport.zAxis = !₂[0, 0, 1]

theorem Cayley.BalancedSupport.zFirst_eq_cross3 (v : Euc(3)) : zFirst v = cross3 zAxis v

def Cayley.BalancedSupport.vecRows (x y z : Fin 3 → ℝ) : Matrix (Fin 3) (Fin 3) ℝ

Equations

• Cayley.BalancedSupport.vecRows x y z = ![x, y, z]

theorem Cayley.BalancedSupport.inner_cross3_eq_det (u v w : Euc(3)) : inner ℝ u (cross3 v w) = (vecRows u.ofLp v.ofLp w.ofLp).det

theorem Cayley.BalancedSupport.oriented_frame_first_inner (frame : Euc(3) ≃ₗᵢ[ℝ] Euc(3)) (inverseMatrix : Matrix (Fin 3) (Fin 3) ℝ) (hinverse : ∀ (x : Euc(3)), (frame.symm x).ofLp = inverseMatrix.mulVec x.ofLp) (v d : Euc(3)) : inner ℝ d (frame (zFirst (frame.symm v))) = inverseMatrix.det * inner ℝ (frame zAxis) (cross3 v d)

Orientation-preserving orthonormal frames carry the standard infinitesimal z rotation to cross product with their z axis.

theorem Cayley.BalancedSupport.Rz_apply_sub_exact (s : ℝ) (v : Euc(3)) : (RzL s) v - v = Real.sin s • zFirst v + (1 - Real.cos s) • zRemainder v

structure Cayley.BalancedSupport.AxisAngle (Q : Euc(3) →L[ℝ] Euc(3)) : Type

An axis-angle presentation of a three-dimensional rotation. The axis is encoded by the orthonormal frame taking the standard z axis to that axis.

• frame : Euc(3) ≃ₗᵢ[ℝ] Euc(3)
• axis : Euc(3)
• axis_norm : ‖self.axis‖ = 1
• first_inner (v d : Euc(3)) : inner ℝ d (self.frame (zFirst (self.frame.symm v))) = inner ℝ self.axis (cross3 v d)
• angle : ℝ
• angle_mem : self.angle ∈ Set.Ioc (-Real.pi) Real.pi
• rotation_eq : Q = self.frame.toLinearIsometry.toContinuousLinearMap ∘SL RzL self.angle ∘SL self.frame.symm.toLinearIsometry.toContinuousLinearMap

noncomputable def Cayley.BalancedSupport.AxisAngle.first {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) (v : Euc(3)) : Euc(3)

Equations

• a.first v = a.frame (Cayley.BalancedSupport.zFirst (a.frame.symm v))

noncomputable def Cayley.BalancedSupport.AxisAngle.remainder {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) (v : Euc(3)) : Euc(3)

Equations

• a.remainder v = a.frame (Cayley.BalancedSupport.zRemainder (a.frame.symm v))

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

theorem Cayley.BalancedSupport.AxisAngle.apply_sub_exact {Q : Euc(3) →L[ℝ] Euc(3)} (a : AxisAngle Q) (v : Euc(3)) : Q v - v = Real.sin a.angle • a.first v + (1 - Real.cos a.angle) • a.remainder v

theorem Cayley.BalancedSupport.Rz_mod_two_pi (γ : ℝ) : ∃ γ' ∈ Set.Ioc (-Real.pi) Real.pi, Rz_mat γ = Rz_mat γ'

theorem Cayley.BalancedSupport.SO3_is_conj_Rz_within_pi (A : Matrix (Fin 3) (Fin 3) ℝ) (hA : A ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) : ∃ (U : Matrix (Fin 3) (Fin 3) ℝ) (_ : U ∈ Matrix.orthogonalGroup (Fin 3) ℝ), ∃ γ ∈ Set.Ioc (-Real.pi) Real.pi, A = U * Rz_mat γ * U⁻¹

theorem Cayley.BalancedSupport.exists_axisAngle (A : Matrix (Fin 3) (Fin 3) ℝ) (hA : A ∈ Matrix.specialOrthogonalGroup (Fin 3) ℝ) : Nonempty (AxisAngle (LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)))

Every special orthogonal matrix has an exact AxisAngle presentation with angle in (-π,π].