instance R3_dim_3 : Fact (Module.finrank ℝ R3 = 2 + 1)

Here we define and develop basic properties of the parametrized family rot of rotations. We work with both this family and the corresponding family rot_iso of isometries.

It is much easier to work with the isometry representation as much as possible and convert back to matrices at the end (in particular, see lemma same_action).

theorem s2_nonzero (ax : ↑S2) : ↑ax ≠ 0

noncomputable def ax_space (ax : ↑S2) : Submodule ℝ R3

Equations

• ax_space ax = ℝ ∙ ↑ax

noncomputable def orth (ax : ↑S2) : Submodule ℝ R3

Equations

• orth ax = (ℝ ∙ ↑ax)ᗮ

instance orth_dim_2 (ax : ↑S2) : Fact (Module.finrank ℝ ↥(orth ax) = 2)

def choice_set (ax : ↑S2) : Set ↥(orth ax)

Equations

• choice_set ax = {x : ↥(orth ax) | x ≠ 0}

theorem orth_nonempty (ax : ↑S2) : ∃ (y : ↥(orth ax)), y ∈ choice_set ax

noncomputable def x_B_c (ax : ↑S2) : ↑(choice_set ax)

Equations

• x_B_c ax = ⟨Classical.choose ⋯, ⋯⟩

noncomputable def x_B (ax : ↑S2) : ↥(orth ax)

Equations

• x_B ax = (1 / ‖↑(x_B_c ax)‖) • ↑(x_B_c ax)

theorem x_B_nz (ax : ↑S2) : x_B ax ≠ 0

noncomputable def tmp_basis (ax : ↑S2) : OrthonormalBasis (Fin 2) ℝ ↥(orth ax)

Equations

• tmp_basis ax = OrthonormalBasis.fromOrthogonalSpanSingleton 2 ⋯

noncomputable def plane_o (ax : ↑S2) : Orientation ℝ (↥(orth ax)) (Fin 2)

Equations

• plane_o ax = (tmp_basis ax).toBasis.orientation

noncomputable def orth_B (ax : ↑S2) : Module.Basis (Fin 2) ℝ ↥(orth ax)

Equations

• orth_B ax = (plane_o ax).basisRightAngleRotation (x_B ax) ⋯

noncomputable def ax_B (ax : ↑S2) : Module.Basis (Fin 1) ℝ ↥(ax_space ax)

Equations

• ax_B ax = Module.Basis.mk ⋯ ⋯

noncomputable def rot_iso_plane_equiv (ax : ↑S2) (θ : ℝ) : ↥(orth ax) ≃ₗᵢ[ℝ] ↥(orth ax)

Equations

• rot_iso_plane_equiv ax θ = (plane_o ax).rotation ↑θ

noncomputable def rot_iso_plane_to_st (ax : ↑S2) (θ : ℝ) : ↥(orth ax) →ₗᵢ[ℝ] ↥(orth ax)

Equations

• rot_iso_plane_to_st ax θ = (rot_iso_plane_equiv ax θ).toLinearIsometry

theorem triv_rot_inner (ax : ↑S2) : rot_iso_plane_to_st ax 0 = 1

noncomputable def operp (ax : ↑S2) (v : R3) : ↥(orth ax)

Equations

• operp ax v = (orth ax).orthogonalProjection v

noncomputable def spar (ax : ↑S2) (v : R3) : R3

Equations

• spar ax v = (ℝ ∙ ↑ax).starProjection v

theorem operp_add {u v : R3} (ax : ↑S2) : operp ax (u + v) = operp ax u + operp ax v

theorem spar_add {u v : R3} (ax : ↑S2) : spar ax (u + v) = spar ax u + spar ax v

theorem operp_spar {v : R3} (ax : ↑S2) : operp ax (spar ax v) = 0

theorem spar_spar {v : R3} (ax : ↑S2) : spar ax (spar ax v) = spar ax v

theorem spar_operp {v : R3} (ax : ↑S2) : spar ax ↑(operp ax v) = 0

theorem spar_of_orth (ax : ↑S2) (x : R3) : x ∈ orth ax → spar ax x = 0

theorem spar_of_ax_space (ax : ↑S2) (x : R3) : x ∈ ax_space ax → spar ax x = x

theorem operp_of_ax_space (ax : ↑S2) (x : R3) : x ∈ ax_space ax → operp ax x = 0

theorem rips_add {S T : ℝ} (ax : ↑S2) (v : ↥(orth ax)) : (rot_iso_plane_to_st ax S) ((rot_iso_plane_to_st ax T) v) = (rot_iso_plane_to_st ax (S + T)) v

noncomputable def up (ax : ↑S2) : ↥(orth ax) →ₗᵢ[ℝ] R3

Equations

• up ax = (orth ax).subtypeₗᵢ

theorem up_mem (ax : ↑S2) (v : ↥(orth ax)) : (up ax) v ∈ orth ax

theorem operp_up (ax : ↑S2) (v : ↥(orth ax)) : operp ax ((up ax) v) = v

theorem operp_up_2 (ax : ↑S2) (v : ↥(orth ax)) : operp ax ↑v = v

theorem spar_up_2 (ax : ↑S2) (v : ↥(orth ax)) : spar ax ↑v = 0

theorem spar_up_rot (ax : ↑S2) (v : ↥(orth ax)) : spar ax ((up ax) v) = 0

theorem el_by_parts (ax : ↑S2) (x : R3) : x = ↑(operp ax x) + spar ax x

noncomputable def ang_diff (axis : ↑S2) (s t : R3) : Real.Angle

Equations

• ang_diff axis s t = (plane_o axis).oangle (operp axis s) (operp axis t)

noncomputable def rot_by_parts (ax : ↑S2) (θ : ℝ) (v : R3) : R3

Equations

• rot_by_parts ax θ v = ((up ax).comp (rot_iso_plane_to_st ax θ)) (operp ax v) + spar ax v

theorem triv_rot_by_parts (ax : ↑S2) : rot_by_parts ax 0 = id

theorem rot_by_parts_comp {x : R3} (ax : ↑S2) (θ τ : ℝ) : rot_by_parts ax θ (rot_by_parts ax τ x) = rot_by_parts ax (θ + τ) x

noncomputable def rot_iso (ax : ↑S2) (θ : ℝ) : R3 ≃ₗᵢ[ℝ] R3

Equations

• rot_iso ax θ = { toFun := rot_by_parts ax θ, map_add' := ⋯, map_smul' := ⋯, invFun := rot_by_parts ax (-θ), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

theorem rot_iso_comp {x : R3} (ax : ↑S2) (θ τ : ℝ) : (rot_iso ax θ) ((rot_iso ax τ) x) = (rot_iso ax (θ + τ)) x

theorem rot_iso_fixed_back (axis : ↑S2) (v : R3) (k : ℤ) : (rot_iso axis (2 * Real.pi * ↑k)) v = v

theorem triv_rot_iso (ax : ↑S2) : rot_iso ax 0 = 1

instance orth_dim_3 : Fact (Module.finrank ℝ R3 = 3)

noncomputable def Basis3 : OrthonormalBasis (Fin 3) ℝ R3

Equations

• Basis3 = EuclideanSpace.basisFun (Fin 3) ℝ

def mod_dim : Fin 2 → Type

Equations

• mod_dim ⟨0, isLt⟩ = Fin 2
• mod_dim ⟨1, isLt⟩ = Fin 1

instance mod_dim_fintype (i : Fin 2) : Fintype (mod_dim i)

Equations

• mod_dim_fintype ⟨0, isLt⟩ = Fin.fintype 2
• mod_dim_fintype ⟨1, isLt⟩ = Fin.fintype 1

instance mod_dim_decidableEq (i : Fin 2) : DecidableEq (mod_dim i)

Equations

• mod_dim_decidableEq ⟨0, isLt⟩ = id (instDecidableEqFin 2)
• mod_dim_decidableEq ⟨1, isLt⟩ = id (instDecidableEqFin 1)

noncomputable def submods (ax : ↑S2) : Fin 2 → Submodule ℝ R3

Equations

• submods ax = ![orth ax, ax_space ax]

theorem internal_pr (ax : ↑S2) : DirectSum.IsInternal (submods ax)

noncomputable def sm_bases (ax : ↑S2) (i : Fin 2) : Module.Basis (mod_dim i) ℝ ↥(submods ax i)

Equations

• sm_bases ax ⟨0, isLt⟩ = orth_B ax
• sm_bases ax ⟨1, isLt⟩ = ax_B ax

theorem hf {θ : ℝ} (ax : ↑S2) (i : Fin 2) : Set.MapsTo ⇑↑(rot_iso ax θ).toLinearEquiv ↑(submods ax i) ↑(submods ax i)

def PROD_BLOCK : Type

Equations

• PROD_BLOCK = Matrix ((i : Fin 2) × mod_dim i) ((i : Fin 2) × mod_dim i) ℝ

noncomputable def rot_mat_block_1 (ax : ↑S2) (θ : ℝ) : PROD_BLOCK

Equations

• rot_mat_block_1 ax θ = (LinearMap.toMatrix (⋯.collectedBasis (sm_bases ax)) (⋯.collectedBasis (sm_bases ax))) ↑(rot_iso ax θ).toLinearEquiv

noncomputable def rot_mat_block_2 (ax : ↑S2) (θ : ℝ) : PROD_BLOCK

Equations

• rot_mat_block_2 ax θ = Matrix.blockDiagonal' fun (i : Fin 2) => (LinearMap.toMatrix (sm_bases ax i) (sm_bases ax i)) ((↑(rot_iso ax θ).toLinearEquiv).restrict ⋯)

theorem rot_mat_block_prop (ax : ↑S2) (θ : ℝ) : rot_mat_block_1 ax θ = rot_mat_block_2 ax θ

theorem block_1_lem {θ : ℝ} (ax : ↑S2) : (LinearMap.toMatrix (sm_bases ax 0) (sm_bases ax 0)) ((↑(rot_iso ax θ).toLinearEquiv).restrict ⋯) = !![Real.cos θ, -Real.sin θ; Real.sin θ, Real.cos θ]

theorem block_2_lem {θ : ℝ} (ax : ↑S2) : (LinearMap.toMatrix (sm_bases ax 1) (sm_bases ax 1)) ((↑(rot_iso ax θ).toLinearEquiv).restrict ⋯) = !![1]

theorem block_repr (ax : ↑S2) (θ : ℝ) : (LinearMap.toMatrix (⋯.collectedBasis (sm_bases ax)) (⋯.collectedBasis (sm_bases ax))) ↑(rot_iso ax θ).toLinearEquiv = Matrix.blockDiagonal' fun (i : Fin 2) => match i with | ⟨0, isLt⟩ => !![Real.cos θ, -Real.sin θ; Real.sin θ, Real.cos θ] | ⟨1, isLt⟩ => !![1]

noncomputable def rot_mat_inner (θ : ℝ) : MAT

Equations

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

noncomputable def rot_mat_inner_trans (θ : ℝ) : MAT

Equations

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

theorem rmi_trans_equiv (θ : ℝ) : Matrix.transpose (rot_mat_inner θ) = rot_mat_inner_trans θ

theorem rot_mat_inner_is_special (θ : ℝ) : rot_mat_inner θ ∈ SO3

def fTS_fun : Fin 3 → (i : Fin 2) × mod_dim i

Equations

• fTS_fun ⟨0, isLt⟩ = ⟨⟨0, fTS_fun._proof_1⟩, ⟨0, fTS_fun._proof_1⟩⟩
• fTS_fun ⟨1, isLt⟩ = ⟨⟨0, fTS_fun._proof_1⟩, ⟨1, fTS_fun._proof_2⟩⟩
• fTS_fun ⟨2, isLt⟩ = ⟨⟨1, fTS_fun._proof_2⟩, ⟨0, fTS_fun._proof_3⟩⟩

theorem fTS_fun_bij : Function.Bijective fTS_fun

noncomputable def finToSigma : Fin 3 ≃ (i : Fin 2) × mod_dim i

Equations

• finToSigma = Equiv.ofBijective fTS_fun fTS_fun_bij

noncomputable def COB_MB (ax : ↑S2) : Module.Basis (Fin 3) ℝ R3

Equations

• COB_MB ax = (⋯.collectedBasis (sm_bases ax)).reindex finToSigma.symm

theorem COB_MB_is_ortho (ax : ↑S2) : Orthonormal ℝ ⇑(COB_MB ax)

noncomputable def COB (ax : ↑S2) : OrthonormalBasis (Fin 3) ℝ R3

Equations

• COB ax = (COB_MB ax).toOrthonormalBasis ⋯

theorem COB_to_basis (ax : ↑S2) : (COB ax).toBasis = COB_MB ax

noncomputable def COB_mat (ax : ↑S2) : MAT

Equations

• COB_mat ax = (LinearMap.toMatrix Basis3.toBasis (COB ax).toBasis) 1

theorem cob_mat_other_repr (ax : ↑S2) : COB_mat ax = (COB ax).toBasis.toMatrix ⇑Basis3

theorem COB_mat_is_ortho (ax : ↑S2) : COB_mat ax ∈ Matrix.orthogonalGroup (Fin 3) ℝ

noncomputable def rot_mat (ax : ↑S2) (θ : ℝ) : MAT

Equations

• rot_mat ax θ = (COB_mat ax)⁻¹ * rot_mat_inner θ * COB_mat ax

theorem rot_mat_is_special (ax : ↑S2) (θ : ℝ) : rot_mat ax θ ∈ SO3

noncomputable def rot (ax : ↑S2) (θ : ℝ) : ↥SO3

Equations

• rot ax θ = ⟨rot_mat ax θ, ⋯⟩

theorem triv_rot (ax : ↑S2) : rot ax 0 = 1

theorem rot_mat_inner_comp_add (s t : ℝ) : rot_mat_inner s * rot_mat_inner t = rot_mat_inner (s + t)

theorem rot_mat_comp_add (ax : ↑S2) (s t : ℝ) : rot_mat ax s * rot_mat ax t = rot_mat ax (s + t)

theorem rot_comp_add (ax : ↑S2) (s t : ℝ) : f (rot ax s) ∘ f (rot ax t) = f (rot ax (s + t))

theorem rot_pow_lemma (ax : ↑S2) (θ : ℝ) (N : ℕ) : (f (rot ax θ))^[N] = f (rot ax (↑N * θ))

theorem rot_iso_pow_lemma (ax : ↑S2) (θ : ℝ) (N : ℕ) : (⇑(rot_iso ax θ))^[N] = ⇑(rot_iso ax (↑N * θ))

theorem orth_toMatrix_mulVec_repr (B C : OrthonormalBasis (Fin 3) ℝ R3) (f : R3 →ₗ[ℝ] R3) (x : R3) : ((LinearMap.toMatrix B.toBasis C.toBasis) f).mulVec (B.repr x).ofLp = (C.repr (f x)).ofLp

theorem inner_as_to_matrix_MB {T : ℝ} (ax : ↑S2) : rot_mat_inner T = (LinearMap.toMatrix (COB_MB ax) (COB_MB ax)) ↑(rot_iso ax T).toLinearEquiv

theorem inner_as_to_matrix {T : ℝ} (ax : ↑S2) : rot_mat_inner T = (LinearMap.toMatrix (COB ax).toBasis (COB ax).toBasis) ↑(rot_iso ax T).toLinearEquiv

theorem same_action {T : ℝ} (ax : ↑S2) (s : R3) : rot ax T • s = (rot_iso ax T) s