structure Pose : Type

• θ₁ : ℝ
• θ₂ : ℝ
• φ₁ : ℝ
• φ₂ : ℝ
• α : ℝ

noncomputable instance instPoseLikePose : PoseLike Pose

Equations

• instPoseLikePose = { inner := fun (vp : Pose) => (↑(rotRM vp.θ₁ vp.φ₁ vp.α)).toAffineMap, outer := fun (vp : Pose) => (↑(rotRM vp.θ₂ vp.φ₂ 0)).toAffineMap }

noncomputable def Pose.rotM₁ (p : Pose) : Euc(3) →L[ℝ] Euc(2)

Equations

• p.rotM₁ = rotM p.θ₁ p.φ₁

noncomputable def Pose.rotM₂ (p : Pose) : Euc(3) →L[ℝ] Euc(2)

Equations

• p.rotM₂ = rotM p.θ₂ p.φ₂

noncomputable def Pose.rotR (p : Pose) : Euc(2) →L[ℝ] Euc(2)

Equations

• p.rotR = rotR p.α

noncomputable def Pose.vecX₁ (p : Pose) : Euc(3)

Equations

• p.vecX₁ = vecX p.θ₁ p.φ₁

noncomputable def Pose.vecX₂ (p : Pose) : Euc(3)

Equations

• p.vecX₂ = vecX p.θ₂ p.φ₂

noncomputable def Pose.rotM₁θ (p : Pose) : Euc(3) →L[ℝ] Euc(2)

Equations

• p.rotM₁θ = rotMθ p.θ₁ p.φ₁

noncomputable def Pose.rotM₂θ (p : Pose) : Euc(3) →L[ℝ] Euc(2)

Equations

• p.rotM₂θ = rotMθ p.θ₂ p.φ₂

noncomputable def Pose.rotM₁φ (p : Pose) : Euc(3) →L[ℝ] Euc(2)

Equations

• p.rotM₁φ = rotMφ p.θ₁ p.φ₁

noncomputable def Pose.rotM₂φ (p : Pose) : Euc(3) →L[ℝ] Euc(2)

Equations

• p.rotM₂φ = rotMφ p.θ₂ p.φ₂

noncomputable def Pose.rotR' (p : Pose) : Euc(2) →L[ℝ] Euc(2)

Equations

• p.rotR' = rotR' p.α

noncomputable def Pose.inner (p : Pose) : Euc(3) →ᵃ[ℝ] Euc(2)

Equations

• p.inner = innerProj p

noncomputable def Pose.outer (p : Pose) : Euc(3) →ᵃ[ℝ] Euc(2)

Equations

• p.outer = outerProj p

inductive Pose.equiv (p1 p2 : Pose) : Prop

• on_the_nose {p1 p2 : Pose} : p1.inner = p2.inner ∧ p1.outer = p2.outer → p1.equiv p2
• off_by_neg {p1 p2 : Pose} : p1.inner = -p2.inner ∧ p1.outer = -p2.outer → p1.equiv p2

def Pose.innerParams (p : Pose) : Euc(3)

Equations

• p.innerParams = !₂[p.α, p.θ₁, p.φ₁]

def Pose.outerParams (p : Pose) : Euc(2)

Equations

• p.outerParams = !₂[p.θ₂, p.φ₂]

theorem Pose.p_outer_eq_outer_shadow (p : Pose) (S : Set Euc(3)) : ⇑p.outer '' S = outerShadow p S

theorem Pose.proj_rm_eq_m (θ φ : ℝ) (v : Euc(3)) : proj_xyL ((rotRM θ φ 0) v) = (rotM θ φ) v

theorem Pose.is_rupert_imp_inner_in_outer (p : Pose) (poly : Finset Euc(3)) (h_rupert : RupertPose p ((convexHull ℝ) ↑poly)) (v : Euc(3)) (hv : v ∈ poly) : p.inner v ∈ (convexHull ℝ) (⇑p.outer '' ↑poly)

If we have a convex polyhedron with p being a pose witness of the rupert property, then in particular every vertex in the "inner" transformation lies in the convex hull of the vertices under the "outer" transformation.

theorem Pose.inner_shadow_eq_img_inner (p : Pose) (S : Set Euc(3)) : innerShadow p S = ⇑p.inner '' S

theorem Pose.outer_shadow_eq_img_outer (p : Pose) (S : Set Euc(3)) : outerShadow p S = ⇑p.outer '' S

theorem Pose.inner_eq_RM (p : Pose) : ⇑p.inner = ⇑p.rotR ∘ ⇑p.rotM₁

theorem Pose.outer_eq_M (p : Pose) : ⇑p.outer = ⇑p.rotM₂

theorem Pose.inner_shadow_eq_RM (p : Pose) (S : Set Euc(3)) : innerShadow p S = ⇑(p.rotR.comp p.rotM₁) '' S

theorem Pose.outer_shadow_eq_M (p : Pose) (S : Set Euc(3)) : outerShadow p S = ⇑p.rotM₂ '' S

theorem Pose.poselike_inner_eq_proj_inner (p : Pose) : ⇑proj_xyL ∘ ⇑(PoseLike.inner p) = ⇑p.inner

theorem Pose.poselike_outer_eq_proj_outer (p : Pose) : ⇑proj_xyL ∘ ⇑(PoseLike.outer p) = ⇑p.outer

theorem Pose.equiv_rupert_imp_rupert {p1 p2 : Pose} {S : Set Euc(3)} (e : p1.equiv p2) (r : RupertPose p1 S) : RupertPose p2 S

theorem Pose.matrix_rm_eq_imp_pose_equiv {p q : Pose} (rme : ⇑p.rotR ∘ ⇑p.rotM₁ = ⇑q.rotR ∘ ⇑q.rotM₁) (rm2 : p.rotM₂ = q.rotM₂) : p.equiv q

theorem Pose.matrix_rm_eq_neg_imp_pose_equiv {p q : Pose} (rme : ⇑p.rotR ∘ ⇑p.rotM₁ = -⇑q.rotR ∘ ⇑q.rotM₁) (rm2 : p.rotM₂ = -q.rotM₂) : p.equiv q

theorem Pose.matrix_eq_imp_pose_equiv {p q : Pose} (re : p.rotR = q.rotR) (rm1 : p.rotM₁ = q.rotM₁) (rm2 : p.rotM₂ = q.rotM₂) : p.equiv q

theorem Pose.matrix_neg_imp_pose_equiv {p q : Pose} (re : p.rotR = -q.rotR) (rm1 : p.rotM₁ = q.rotM₁) (rm2 : p.rotM₂ = -q.rotM₂) : p.equiv q