structure Pose (R : Type) : Type

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

@[implicit_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.

@[implicit_reducible]

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

Equations

• instReprPose = { reprPrec := instReprPose.repr }

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

Equations

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

@[implicit_reducible]

noncomputable instance instPoseLikePoseReal : PoseLike (Pose ℝ)

Equations

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

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

Bijection between Pose and Fin 5 → ℝ, used to transfer the (sup-norm) MetricSpace instance from the Pi type.

Equations

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

@[implicit_reducible]

instance Pose.instMetricSpace {R : Type} [MetricSpace R] : MetricSpace (Pose R)

Sup-norm transferred from Fin 5 → R.

Equations

• Pose.instMetricSpace = MetricSpace.induced ⇑Pose.equivPi ⋯ inferInstance

@[implicit_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.α

@[implicit_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.α) ⋯

theorem Pose.mem_closedBall_iff {R : Type} [MetricSpace R] {p q : Pose R} {ε : ℝ} : p ∈ Metric.closedBall q ε ↔ dist p.θ₁ q.θ₁ ≤ ε ∧ dist p.θ₂ q.θ₂ ≤ ε ∧ dist p.φ₁ q.φ₁ ≤ ε ∧ dist p.φ₂ q.φ₂ ≤ ε ∧ dist 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.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 {α : Type} [PoseLike α] (p1 p2 : α) : Prop

• on_the_nose {α : Type} [PoseLike α] {p1 p2 : α} : innerShadow p1 = innerShadow p2 ∧ outerShadow p1 = outerShadow p2 → equiv p1 p2
• off_by_neg {α : Type} [PoseLike α] {p1 p2 : α} : innerShadow p1 = -innerShadow p2 ∧ outerShadow p1 = -outerShadow p2 → equiv p1 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.pose_on_the_nose {p1 p2 : Pose ℝ} : p1.inner = p2.inner ∧ p1.outer = p2.outer → equiv p1 p2

theorem Pose.pose_off_by_neg {p1 p2 : Pose ℝ} : p1.inner = -p2.inner ∧ p1.outer = -p2.outer → equiv p1 p2

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 {P : Type} [PoseLike P] {p1 p2 : P} {S : Set Euc(3)} (e : equiv p1 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₂) : equiv p 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₂) : equiv p 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₂) : equiv p 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₂) : equiv p q