structure Pose (R : Type) : Type

• θ₁ : R
• θ₂ : R
• φ₁ : R
• φ₂ : R
• α : R

@[instance_reducible]

instance instDecidableEqPose {R✝ : Type} [DecidableEq R✝] : DecidableEq (Pose R✝)

Equations

• instDecidableEqPose = instDecidableEqPose.decEq

def instDecidableEqPose.decEq {R✝ : Type} [DecidableEq R✝] (x✝ x✝¹ : Pose R✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def instReprPose.repr {R✝ : Type} [Repr R✝] : Pose R✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance instReprPose {R✝ : Type} [Repr R✝] : Repr (Pose R✝)

Equations

• instReprPose = { reprPrec := instReprPose.repr }

@[instance_reducible]

instance instToStringPose {R : Type} [ToString R] : ToString (Pose R)

Equations

• One or more equations did not get rendered due to their size.

def Pose.equivPi {R : Type} : Pose R ≃ (Fin 5 → R)

Bijection between Pose R and Fin 5 → R, used to transfer the componentwise PartialOrder from the Pi type.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Pose.instPartialOrder {R : Type} [PartialOrder R] : PartialOrder (Pose R)

Equations

• Pose.instPartialOrder = PartialOrder.lift ⇑Pose.equivPi ⋯

theorem Pose.le_iff {R : Type} [PartialOrder R] (p q : Pose R) : p ≤ q ↔ p.θ₁ ≤ q.θ₁ ∧ p.θ₂ ≤ q.θ₂ ∧ p.φ₁ ≤ q.φ₁ ∧ p.φ₂ ≤ q.φ₂ ∧ p.α ≤ q.α

@[instance_reducible]

instance Pose.instDecidableLE {R : Type} [PartialOrder R] [DecidableLE R] : DecidableLE (Pose R)

Equations

• p.instDecidableLE q = decidable_of_iff (p.θ₁ ≤ q.θ₁ ∧ p.θ₂ ≤ q.θ₂ ∧ p.φ₁ ≤ q.φ₁ ∧ p.φ₂ ≤ q.φ₂ ∧ p.α ≤ q.α) ⋯

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.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.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.φ₂

@[instance_reducible]

noncomputable instance Pose.instPoseLikeReal : PoseLike (Pose ℝ)

The inner projection R(α) M(θ₁, φ₁) of [SY25] (5) and the outer projection M(θ₂, φ₂), as the PoseLike structure of a real pose.

Equations

• Pose.instPoseLikeReal = { inner := fun (p : Pose ℝ) => (↑(p.rotR ∘SL p.rotM₁)).toAffineMap, outer := fun (p : Pose ℝ) => (↑p.rotM₂).toAffineMap }

@[reducible, inline]

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

Equations

• p.inner = PoseLike.inner p

@[reducible, inline]

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

Equations

• p.outer = PoseLike.outer p

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.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_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_shadow_eq_RM (p : Pose ℝ) (S : Set Euc(3)) : innerShadow p S = ⇑(p.rotR ∘SL p.rotM₁) '' S

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

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.