Material for [SY25] Lemma 12.

theorem Bounding.dist_rot3_apply {d : Fin 3} {α α' : ℝ} {v : Euc(3)} : ‖((rot3 d) α - (rot3 d) α') v‖ = 2 * |Real.sin ((α - α') / 2)| * ‖WithLp.toLp 2 (d.removeNth v.ofLp)‖

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

theorem Bounding.dist_rot2_apply {α α' : ℝ} {v : Euc(2)} : ‖(rot2 α - rot2 α') v‖ = 2 * |Real.sin ((α - α') / 2)| * ‖v‖

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

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

theorem Bounding.two_mul_abs_sin_half_le {α : ℝ} : 2 * |Real.sin (α / 2)| ≤ |α|

theorem Bounding.dist_rot2_le_dist {α α' : ℝ} : ‖rot2 α - rot2 α'‖ ≤ ‖α - α'‖

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

Equations

• ⋯ = ⋯