Material for [SY25] Lemma 10 and Lemma 12.

theorem Bounding.rotR_mat_sub_rotR_mat (α α' : ℝ) : rotR_mat α - rotR_mat α' = (2 * Real.sin ((α - α') / 2)) • rotR_mat ((α + α') / 2 + Real.pi / 2)

The difference of two rotation matrices is a scalar multiple of a rotation matrix.

theorem Bounding.rotR_sub_rotR (α α' : ℝ) : rotR α - rotR α' = (2 * Real.sin ((α - α') / 2)) • rotR ((α + α') / 2 + Real.pi / 2)

The difference of two rotations is a scalar multiple of a rotation.

theorem Bounding.dist_rotR {α α' : ℝ} : ‖rotR α - rotR α'‖ = 2 * |Real.sin ((α - α') / 2)|

noncomputable def Bounding.projPerp_mat (d : Fin 3) : Matrix (Fin 3) (Fin 3) ℝ

The diagonal matrix of the projection onto the coordinate plane perpendicular to axis d.

Equations

• Bounding.projPerp_mat d = Matrix.diagonal fun (i : Fin 3) => if i = d then 0 else 1

noncomputable def Bounding.projPerpL (d : Fin 3) : Euc(3) →L[ℝ] Euc(3)

The orthogonal projection of ℝ³ onto the coordinate plane perpendicular to axis d.

Equations

• Bounding.projPerpL d = LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin (Bounding.projPerp_mat d))

theorem Bounding.projPerpL_apply (d : Fin 3) (v : Euc(3)) (i : Fin 3) : ((projPerpL d) v).ofLp i = if i = d then 0 else v.ofLp i

theorem Bounding.projPerpL_norm_one (d : Fin 3) : ‖projPerpL d‖ = 1

theorem Bounding.rot3_mat_sub_rot3_mat (d : Fin 3) (α α' : ℝ) : rot3_mat d α - rot3_mat d α' = (2 * Real.sin ((α - α') / 2)) • (rot3_mat d ((α + α') / 2 + Real.pi / 2) * projPerp_mat d)

The difference of two rotation matrices about axis d is a scalar multiple of a rotation matrix times the projection onto the plane of rotation.

theorem Bounding.rot3_eq_rot3_mat_toEuclideanLin {d : Fin 3} {θ : ℝ} : ↑((rot3 d) θ) = Matrix.toEuclideanLin (rot3_mat d θ)

theorem Bounding.rot3_sub_rot3 (d : Fin 3) (α α' : ℝ) : (rot3 d) α - (rot3 d) α' = (2 * Real.sin ((α - α') / 2)) • (rot3 d) ((α + α') / 2 + Real.pi / 2) ∘SL projPerpL d

The difference of two rotations about axis d is a scalar multiple of a rotation composed with the projection onto the plane of rotation.

theorem Bounding.dist_rot3 {d : Fin 3} {α α' : ℝ} : ‖(rot3 d) α - (rot3 d) α'‖ = 2 * |Real.sin ((α - α') / 2)|

theorem Bounding.dist_rot3_eq_dist_rotR {d : Fin 3} {α α' : ℝ} : ‖(rot3 d) α - (rot3 d) α'‖ = ‖rotR α - rotR α'‖

theorem Bounding.norm_rotR_sub_rotR_lt {ε α α_ : ℝ} (hε : 0 < ε) (hα : |α - α_| ≤ ε) : ‖rotR α - rotR α_‖ < ε

theorem Bounding.norm_RxL_sub_RxL_eq {α α_ : ℝ} : ‖RxL α - RxL α_‖ = ‖rotR α - rotR α_‖

theorem Bounding.norm_RyL_sub_RyL_eq {α α_ : ℝ} : ‖RyL α - RyL α_‖ = ‖rotR α - rotR α_‖

theorem Bounding.norm_RzL_sub_RzL_eq {α α_ : ℝ} : ‖RzL α - RzL α_‖ = ‖rotR α - rotR α_‖