4. Preliminaries🔗

TODO: This whole chapter needs organization, it's just a grab bag of miscellaneous results for now.

4.1. Rupert Sets🔗

Theorem4.1.1

uses 0used by 1✓L∃∀N

The following are equivalent:

The convex polyhedron with vertex set v is Rupert.
The convex closure of v is a Rupert set.

Lean code for Theorem4.1.1●1 theorem

theoremdefined in Noperthedron/Rupert/Equivalences/RupertEquivRupertSet.lean

complete

theorem rupert_iff_rupert_set (v : Finset Euc(3)) :
  IsRupert v ↔ IsRupertSet ((convexHull ℝ) ↑v)

theorem rupert_iff_rupert_set
  (v : Finset Euc(3)) :
  IsRupert v ↔
    IsRupertSet ((convexHull ℝ) ↑v)

Proof for Theorem 4.1.1

uses 0

TODO: import this from the other repo

4.2. Poses🔗

TODO

Theorem4.2.1

uses 0used by 1✓L∃∀N

Given a pose with zero offset, there exists a 5-parameter pose that is equivalent to it.

Lean code for Theorem4.2.1●2 theorems

theoremdefined in Noperthedron/ConvertPose.lean

complete

theorem pose_of_matrix_pose (p : MatrixPose) :
  ∃ δ pp, pp.matrixPoseOfPose = p.zeroOffset.rotateBy δ

theorem pose_of_matrix_pose (p : MatrixPose) :
  ∃ δ pp,
    pp.matrixPoseOfPose =
      p.zeroOffset.rotateBy δ

For any MatrixPose p, after rotating by the right δ, there exists a Pose
that equals the rotated zeroOffset.

theoremdefined in Noperthedron/ConvertPose.lean

complete

theorem converted_pose_rupert_iff (v : Pose ℝ) (S : Set Euc(3)) :
  RupertPose v S ↔ RupertPose v.matrixPoseOfPose S

theorem converted_pose_rupert_iff (v : Pose ℝ)
  (S : Set Euc(3)) :
  RupertPose v S ↔
    RupertPose v.matrixPoseOfPose S

Proof for Theorem 4.2.1

uses 0

By putting the pose into a canonical form as a Z rotation followed by a Y followed by a Z.

4.3. Pointsymmetry and Rupertness🔗

Theorem4.3.1

uses 0used by 1✓L∃∀N

If a set is point symmetric and convex, then it being Rupert implies it being purely rotationally Rupert.

Lean code for Theorem4.3.1●1 theorem

theoremdefined in Noperthedron/CommonCenter.lean

complete

theorem rupert_implies_rot_rupert {S : Set Euc(3)} (s_sym : PointSym S)
  (s_convex : Convex ℝ S) (p : MatrixPose) (r : RupertPose p S) :
  RupertPose p.zeroOffset S

theorem rupert_implies_rot_rupert {S : Set Euc(3)}
  (s_sym : PointSym S)
  (s_convex : Convex ℝ S) (p : MatrixPose)
  (r : RupertPose p S) :
  RupertPose p.zeroOffset S

If a set is point symmetric and convex, then it being rupert implies
being purely rotationally rupert.

Proof for Theorem 4.3.1

uses 0

TODO: informalize proof

Theorem4.3.2

groupuses 0used by 1✓L∃∀N

Suppose S is a finite set of points in \R^n. The radius of the polyhedron S is r iff

there is a vector v \in S with \|v\| = r
all vectors v \in S have \|v\| \le r

Lean code for Theorem4.3.2●1 theorem

theoremdefined in Noperthedron/Basic.lean

complete

theorem Polyhedron.radius_iff {r : ℝ} {ι X : Type} [Fintype ι] [ne : Nonempty ι]
  [Norm X] (iv : Polyhedron ι X) :
  iv.radius = r ↔ (∃ i, ‖iv.v i‖ = r) ∧ ∀ (i : ι), ‖iv.v i‖ ≤ r

theorem Polyhedron.radius_iff {r : ℝ} {ι X : Type}
  [Fintype ι] [ne : Nonempty ι] [Norm X]
  (iv : Polyhedron ι X) :
  iv.radius = r ↔
    (∃ i, ‖iv.v i‖ = r) ∧
      ∀ (i : ι), ‖iv.v i‖ ≤ r

Proof for Theorem 4.3.2

uses 0

Immediate from definition.

Theorem4.3.3

groupuses 0used by 1XL∃∀N

Pointsymmetrization preserves radius.

Proof for Theorem 4.3.3

uses 1

Because the reflection of a point about the origin preserves its norm.