5. The Global Theorem🔗

Lemma5.1

uses 0used by 1✓L∃∀N

Suppose V = V_1, \ldots, V_m \subseteq \mathbb{R}^n is a finite sequence of points, and let \hull V be its convex hull. If S \in \hull V and w \in \mathbb{R}^n, then

\langle S ,w \rangle \leq \max_i \langle V_i ,w\rangle.

Lean code for Lemma5.1●1 theorem

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.hull_scalar_prod {n : ℕ} (V : Finset (E n))
  (Vne : V.Nonempty) (S : E n) (hs : S ∈ (convexHull ℝ) ↑V) (w : E n) :
  inner ℝ w S ≤ (Finset.image (fun x ↦ inner ℝ w x) V).max' ⋯

theorem GlobalTheorem.hull_scalar_prod {n : ℕ}
  (V : Finset (E n)) (Vne : V.Nonempty)
  (S : E n) (hs : S ∈ (convexHull ℝ) ↑V)
  (w : E n) :
  inner ℝ w S ≤
    (Finset.image (fun x ↦ inner ℝ w x)
          V).max'
      ⋯

Proof for Lemma 5.1

uses 0

This is a mild generalization of Steininger and Yurkevich (2025), Lemma 18.

Since S \in \hull V, we have S = \sum_{j=1}^m \lambda_j V_j for some \lambda_1,\ldots,\lambda_m \in [0,1] with 1 = \sum_{j=1}^m \lambda_j. Therefore

\langle S ,w \rangle = \left\langle \sum_{j=1}^m \lambda_j V_j ,w \right\rangle = \sum_{j=1}^m \lambda_j \left\langle V_j ,w \right\rangle \le \sum_{j=1}^m \lambda_j \max_{i} \langle V_i ,w\rangle = \max_{i} \langle V_i ,w\rangle \sum_{j=1}^m \lambda_j = \max_{i} \langle V_i ,w\rangle $$

as required.

Lemma5.2

Group: Derivative bounds and approximation control for rotated projections. (2)

Group member previews

Preview

Lemma 5.3

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1XL∃∀N

Let S \in \mathbb{R}^3 and w \in \mathbb{R}^2 be unit vectors, and set f(x_1,x_2,x_3) = \langle R(x_3) M(x_1,x_2)S,w \rangle. Then for all x_1,x_2,x_3 \in \mathbb{R} and any i,j \in \{1,2,3\} it holds that

\left|\frac{\partial^2 f}{\partial x_i \partial x_j}(x_1,x_2,x_3)\right|\leq 1.

Proof for Lemma 5.2

uses 0

See polyhedron.without.rupert, Lemma 19.

Lemma5.3

Group: Derivative bounds and approximation control for rotated projections. (2)

Group member previews

Preview

Lemma 5.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1XL∃∀N

Let f:\mathbb{R}^n\to \mathbb{R} be a C^2-function and x_1,\dots,x_n,y_1,\dots,y_n \in \mathbb{R} such that |x_1-y_1|,\dots,|x_n-y_n|\leq \varepsilon. If |\partial_{x_i}\partial_{x_j}f(v)| \leq 1 for all i,j \in \{1,\dots,n\} and all v \in \mathbb{R}^n, then

|f(x_1,\dots,x_n)-f(y_1,\dots,y_n)|\leq \varepsilon \sum_{i=1}^n |\partial_{x_i} f(x_1,\dots,x_n)| + \frac{n^2}{2}\varepsilon^2.

Proof for Lemma 5.3

uses 0

See polyhedron.without.rupert, Lemma 20.

Lemma5.4

Group: Derivative bounds and approximation control for rotated projections. (2)

Group member previews

Preview

Lemma 5.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

The partial derivatives of all relevant rotations, projections, and inner products used in the Global Theorem are as expected. Specifically:

f^\alpha(\theta,\phi,\alpha) = \langle R'(\alpha) M(\theta, \phi) S, w \rangle
f^\theta(\theta,\phi,\alpha) = \langle R(\alpha) M^\theta(\theta, \phi) S, w \rangle
f^\phi(\theta,\phi,\alpha) = \langle R(\alpha) M^\phi(\theta, \phi) S, w \rangle
g^\theta(\theta,\phi) = \langle M^\theta(\theta, \phi) P, w \rangle
g^\phi(\theta,\phi) = \langle M^\phi(\theta, \phi) P, w \rangle

where f(\theta,\phi,\alpha) = \langle R(\alpha) M(\theta,\phi) S / \|S\|, w\rangle and g(\theta,\phi) = \langle M(\theta,\phi) P / \|P\|, w\rangle.

Lean code for Lemma5.4●7 theorems

theoremdefined in Noperthedron/Global/Definitions.lean

complete

theorem GlobalTheorem.rotation_partials_exist {S : Euc(3)} {w : Euc(2)} :
  ContDiff ℝ 3 (GlobalTheorem.rotproj_inner_unit S w)

theorem GlobalTheorem.rotation_partials_exist
  {S : Euc(3)} {w : Euc(2)} :
  ContDiff ℝ 3
    (GlobalTheorem.rotproj_inner_unit S w)

theoremdefined in Noperthedron/Global/Definitions.lean

complete

theorem GlobalTheorem.rotation_partials_exist_outer {S : Euc(3)} {w : Euc(2)} :
  ContDiff ℝ 3 (GlobalTheorem.rotproj_outer_unit S w)

theorem GlobalTheorem.rotation_partials_exist_outer
  {S : Euc(3)} {w : Euc(2)} :
  ContDiff ℝ 3
    (GlobalTheorem.rotproj_outer_unit S w)

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper0 {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition poly pbar εα εθ₁ εφ₁ εθ₂
      εφ₂) :
  ‖pc.S‖ * GlobalTheorem.nth_partial 0 pc.fu pbar.innerParams =
    inner ℝ (pbar.rotR' (pbar.rotM₁ pc.S)) pc.w

theorem GlobalTheorem.partials_helper0
  {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition
      poly pbar εα εθ₁ εφ₁ εθ₂ εφ₂) :
  ‖pc.S‖ *
      GlobalTheorem.nth_partial 0 pc.fu
        pbar.innerParams =
    inner ℝ (pbar.rotR' (pbar.rotM₁ pc.S))
      pc.w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper1 {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition poly pbar εα εθ₁ εφ₁ εθ₂
      εφ₂) :
  ‖pc.S‖ * GlobalTheorem.nth_partial 1 pc.fu pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁θ pc.S)) pc.w

theorem GlobalTheorem.partials_helper1
  {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition
      poly pbar εα εθ₁ εφ₁ εθ₂ εφ₂) :
  ‖pc.S‖ *
      GlobalTheorem.nth_partial 1 pc.fu
        pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁θ pc.S))
      pc.w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper2 {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition poly pbar εα εθ₁ εφ₁ εθ₂
      εφ₂) :
  ‖pc.S‖ * GlobalTheorem.nth_partial 2 pc.fu pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁φ pc.S)) pc.w

theorem GlobalTheorem.partials_helper2
  {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition
      poly pbar εα εθ₁ εφ₁ εθ₂ εφ₂) :
  ‖pc.S‖ *
      GlobalTheorem.nth_partial 2 pc.fu
        pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁φ pc.S))
      pc.w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper3 {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition poly pbar εα εθ₁ εφ₁ εθ₂
      εφ₂)
  (P : Euc(3)) :
  ‖P‖ *
      GlobalTheorem.nth_partial 0
        (GlobalTheorem.GlobalTheoremPrecondition.fu_outer P pc)
        pbar.outerParams =
    inner ℝ (pbar.rotM₂θ P) pc.w

theorem GlobalTheorem.partials_helper3
  {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition
      poly pbar εα εθ₁ εφ₁ εθ₂ εφ₂)
  (P : Euc(3)) :
  ‖P‖ *
      GlobalTheorem.nth_partial 0
        (GlobalTheorem.GlobalTheoremPrecondition.fu_outer
          P pc)
        pbar.outerParams =
    inner ℝ (pbar.rotM₂θ P) pc.w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper4 {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι] {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition poly pbar εα εθ₁ εφ₁ εθ₂
      εφ₂)
  (P : Euc(3)) :
  ‖P‖ *
      GlobalTheorem.nth_partial 1
        (GlobalTheorem.GlobalTheoremPrecondition.fu_outer P pc)
        pbar.outerParams =
    inner ℝ (pbar.rotM₂φ P) pc.w

theorem GlobalTheorem.partials_helper4
  {pbar : Pose ℝ} {εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ}
  {ι : Type} [Fintype ι] [Nonempty ι]
  {poly : GoodPoly ι}
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition
      poly pbar εα εθ₁ εφ₁ εθ₂ εφ₂)
  (P : Euc(3)) :
  ‖P‖ *
      GlobalTheorem.nth_partial 1
        (GlobalTheorem.GlobalTheoremPrecondition.fu_outer
          P pc)
        pbar.outerParams =
    inner ℝ (pbar.rotM₂φ P) pc.w

Proof for Lemma 5.4

uses 0

By basic properties of derivatives.

Theorem5.5

uses 0used by 1✓L∃∀N

Let \PPP be a pointsymmetric convex polyhedron with radius \rho =1 and let S \in \PPP. Further let \thetab_1,\phib_1,\thetab_2,\phib_2,\alphab \in \R and let w\in\R^2 be a unit vector. Denote \Mib \coloneqq M(\thetab_1, \phib_1), \Miib \coloneqq M(\thetab_2, \phib_2) as well as \Mib^{\theta} \coloneqq M^\theta(\thetab_1, \phib_1), \Mib^{\phi} \coloneqq M^\phi(\thetab_1, \phib_1) and analogously for \Miib^{\theta}, \Miib^{\phi}. Finally set

\begin{align*} G& \coloneqq \langle R(\alphab) \Mib S,w \rangle - \epsilon\cdot\big(|\langle R'(\alphab) \Mib S,w \rangle|+|\langle R(\alphab) \Mib^\theta S,w \rangle|+|\langle R(\alphab) \Mib^\phi S,w \rangle|\big)- 9\epsilon^2/2,\\ H_P & \coloneqq \langle \Miib P,w \rangle + \epsilon\cdot\big(|\langle \Miib^\theta P,w \rangle|+|\langle \Miib^\varphi P,w \rangle|\big) + 2\epsilon^2, \quad \text{ for } P \in \PPP. \end{align*} $$

If G>\max_{P\in \PPP} H_P then there does not exist a solution to Rupert's condition with

(\theta_1,\varphi_1,\theta_2,\varphi_2,\alpha) \in U \coloneqq [\thetab_1\pm\epsilon,\phib_1\pm\epsilon,\thetab_2\pm\epsilon,\phib_2\pm\epsilon,\alphab\pm\epsilon] \subseteq \R^5.

Lean code for Theorem5.5●1 theorem

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.global_theorem {ι : Type} [Fintype ι] [Nonempty ι]
  (pbar : Pose ℝ) (εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ) (hεα : 0 ≤ εα)
  (hεθ₁ : 0 ≤ εθ₁) (hεφ₁ : 0 ≤ εφ₁) (hεθ₂ : 0 ≤ εθ₂) (hεφ₂ : 0 ≤ εφ₂)
  (poly : GoodPoly ι)
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition poly pbar εα εθ₁ εφ₁ εθ₂
      εφ₂) :
  ¬∃ p, pbar.near εα εθ₁ εφ₁ εθ₂ εφ₂ p ∧ RupertPose p poly.hull

theorem GlobalTheorem.global_theorem {ι : Type}
  [Fintype ι] [Nonempty ι] (pbar : Pose ℝ)
  (εα εθ₁ εφ₁ εθ₂ εφ₂ : ℝ) (hεα : 0 ≤ εα)
  (hεθ₁ : 0 ≤ εθ₁) (hεφ₁ : 0 ≤ εφ₁)
  (hεθ₂ : 0 ≤ εθ₂) (hεφ₂ : 0 ≤ εφ₂)
  (poly : GoodPoly ι)
  (pc :
    GlobalTheorem.GlobalTheoremPrecondition
      poly pbar εα εθ₁ εφ₁ εθ₂ εφ₂) :
  ¬∃ p,
      pbar.near εα εθ₁ εφ₁ εθ₂ εφ₂ p ∧
        RupertPose p poly.hull

The Global Theorem, [SY25] Theorem 17, with a per-axis box in place of the
closed ball.

Proof for Theorem 5.5

Proof uses 4

Proof dependency previews

Preview

Lemma 5.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

See polyhedron.without.rupert, Section 4.2.