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) : ℝ³ →L[ℝ] ℝ²

Equations

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

noncomputable def Pose.rotM₂ (p : Pose) : ℝ³ →L[ℝ] ℝ²

Equations

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

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

Equations

• p.rotR = rotR p.α

noncomputable def Pose.vecX₁ (p : Pose) : ℝ³

Equations

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

noncomputable def Pose.vecX₂ (p : Pose) : ℝ³

Equations

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

noncomputable def Pose.rotM₁θ (p : Pose) : ℝ³ →L[ℝ] ℝ²

Equations

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

noncomputable def Pose.rotM₂θ (p : Pose) : ℝ³ →L[ℝ] ℝ²

Equations

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

noncomputable def Pose.rotM₁φ (p : Pose) : ℝ³ →L[ℝ] ℝ²

Equations

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

noncomputable def Pose.rotM₂φ (p : Pose) : ℝ³ →L[ℝ] ℝ²

Equations

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

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

Equations

• p.rotR' = rotR' p.α

noncomputable def Pose.inner (p : Pose) : ℝ³ →ᵃ[ℝ] ℝ²

Equations

• p.inner = innerProj p

noncomputable def Pose.outer (p : Pose) : ℝ³ →ᵃ[ℝ] ℝ²

Equations

• p.outer = outerProj p

def Pose.innerParams (p : Pose) : ℝ³

Equations

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

theorem Pose.p_outer_eq_outer_shadow (p : Pose) (S : Set ℝ³) : ⇑p.outer '' S = outerShadow p S

theorem Pose.is_rupert_imp_inner_in_outer (p : Pose) (poly : Finset ℝ³) (h_rupert : RupertPose p ((convexHull ℝ) ↑poly)) (v : ℝ³) (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.