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 1✓L∃∀N

Let S \in \mathbb{R}^3, let w \in \mathbb{R}^2 be a unit vector, 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,k \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 \|S\| \qquad\text{and}\qquad \left|\frac{\partial^3 f}{\partial x_i \partial x_j \partial x_k}(x_1,x_2,x_3)\right|\leq \|S\|.

The source reference normalizes f by 1/\|S\| and bounds the partials by 1; here f remains unnormalized and the bound carries \|S\|, which composes with Lemma 5.3 at M=\|S\|\leq1.

Lean code for Lemma5.2●1 theorem

theoremdefined in Noperthedron/Global/RotationPartials/SecondPartialInner.lean

complete

theorem GlobalTheorem.rotation_third_partials_bounded (S : Euc(3)) {w : Euc(2)}
  (w_unit : ‖w‖ = 1) :
  GlobalTheorem.third_partials_bounded (GlobalTheorem.rotproj_inner S w)
    ‖S‖

theorem GlobalTheorem.rotation_third_partials_bounded
  (S : Euc(3)) {w : Euc(2)}
  (w_unit : ‖w‖ = 1) :
  GlobalTheorem.third_partials_bounded
    (GlobalTheorem.rotproj_inner S w) ‖S‖

Proof for Lemma 5.2

uses 0

The second-partial bound is polyhedron.without.rupert, Lemma 19. For the third partials (and, in the formalization, every higher order at once) we argue by closure instead of enumeration: the family of functions \pm\langle (\pm R/R')(\alpha)(\partial_\theta^a\partial_\phi^b M)(\theta,\phi)S,w\rangle with a,b\le2 is closed under all three partial derivatives. An \alpha-derivative steps the head around its four-cycle R\to R'\to -R\to -R', and a \theta- or \phi-derivative bumps one grid index, folding back with a sign at the edge since \partial_\theta^3=-\partial_\theta and \partial_\phi^3=-\partial_\phi. Every member is bounded by \|S\| because each factor has operator norm at most one, so iterating the closure bounds all iterated partials.

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 1✓L∃∀N

Let f:\mathbb{R}^n\to \mathbb{R} be a C^3-function, let \varepsilon_1,\dots,\varepsilon_n \geq 0, and let x_1,\dots,x_n,y_1,\dots,y_n \in \mathbb{R} satisfy |x_i-y_i|\leq \varepsilon_i for all i. If, for some M\in\mathbb R, |\partial_{x_i}\partial_{x_j}\partial_{x_k}f(v)| \leq M for all i,j,k \in \{1,\dots,n\} and all v \in \mathbb{R}^n, then

|f(x)-f(y)|\leq \sum_{i=1}^n \varepsilon_i |\partial_{x_i} f(x)| + \frac{1}{2} \sum_{i=1}^n \sum_{j=1}^n \varepsilon_i \varepsilon_j |\partial_{x_i}\partial_{x_j} f(x)| + \frac{M}{6}\Big(\sum_{i=1}^n \varepsilon_i\Big)^3.

At M=1 and \varepsilon_1=\dots=\varepsilon_n=\varepsilon, this recovers the isotropic remainder \frac{n^3}{6}\varepsilon^3.

Lean code for Lemma5.3●1 theorem

theoremdefined in Noperthedron/Global/BoundedPartialsControlDifference.lean

complete

theorem GlobalTheorem.bounded_partials_control_difference2 {n : ℕ} (f : E n → ℝ)
  (fc : ContDiff ℝ 3 f) (x y : E n) (ε : Fin n → ℝ)
  (hε : ∀ (i : Fin n), 0 ≤ ε i)
  (hdiff : ∀ (i : Fin n), |x.ofLp i - y.ofLp i| ≤ ε i) {M : ℝ}
  (tpb : GlobalTheorem.third_partials_bounded f M) :
  |f x - f y| ≤
    ∑ i, ε i * |GlobalTheorem.nth_partial i f x| +
        1 / 2 *
          ∑ i,
            ∑ j,
              ε i * ε j *
                |GlobalTheorem.nth_partial i
                    (GlobalTheorem.nth_partial j f) x| +
      M * (∑ i, ε i) ^ 3 / 6

theorem GlobalTheorem.bounded_partials_control_difference2
  {n : ℕ} (f : E n → ℝ)
  (fc : ContDiff ℝ 3 f) (x y : E n)
  (ε : Fin n → ℝ)
  (hε : ∀ (i : Fin n), 0 ≤ ε i)
  (hdiff :
    ∀ (i : Fin n),
      |x.ofLp i - y.ofLp i| ≤ ε i)
  {M : ℝ}
  (tpb :
    GlobalTheorem.third_partials_bounded f
      M) :
  |f x - f y| ≤
    ∑ i,
          ε i *
            |GlobalTheorem.nth_partial i f
                x| +
        1 / 2 *
          ∑ i,
            ∑ j,
              ε i * ε j *
                |GlobalTheorem.nth_partial
                    i
                    (GlobalTheorem.nth_partial
                      j f)
                    x| +
      M * (∑ i, ε i) ^ 3 / 6

Proof for Lemma 5.3

uses 0

This strengthens polyhedron.without.rupert, Lemma 20, by one Taylor order and per-axis radii: expand g(t) = f((1-t)x + ty) to second order with Lagrange remainder, bound |g'(0)| by the first sum, |g''(0)|/2 by the second (the second partials are evaluated exactly at x, not bounded), and |g'''(c)| \leq M(\sum_i \varepsilon_i)^3 using the third-partial bound.

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, w\rangle and g(\theta,\phi) = \langle M(\theta,\phi) 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 S w)

theorem GlobalTheorem.rotation_partials_exist
  {S : Euc(3)} {w : Euc(2)} :
  ContDiff ℝ 3
    (GlobalTheorem.rotproj_inner 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 S w)

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

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper0 (pbar : Pose ℝ) (S : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 0 (GlobalTheorem.rotproj_inner S w)
      pbar.innerParams =
    inner ℝ (pbar.rotR' (pbar.rotM₁ S)) w

theorem GlobalTheorem.partials_helper0
  (pbar : Pose ℝ) (S : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 0
      (GlobalTheorem.rotproj_inner S w)
      pbar.innerParams =
    inner ℝ (pbar.rotR' (pbar.rotM₁ S)) w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper1 (pbar : Pose ℝ) (S : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 1 (GlobalTheorem.rotproj_inner S w)
      pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁θ S)) w

theorem GlobalTheorem.partials_helper1
  (pbar : Pose ℝ) (S : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 1
      (GlobalTheorem.rotproj_inner S w)
      pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁θ S)) w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper2 (pbar : Pose ℝ) (S : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 2 (GlobalTheorem.rotproj_inner S w)
      pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁φ S)) w

theorem GlobalTheorem.partials_helper2
  (pbar : Pose ℝ) (S : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 2
      (GlobalTheorem.rotproj_inner S w)
      pbar.innerParams =
    inner ℝ (pbar.rotR (pbar.rotM₁φ S)) w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper3 (pbar : Pose ℝ) (P : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 0 (GlobalTheorem.rotproj_outer P w)
      pbar.outerParams =
    inner ℝ (pbar.rotM₂θ P) w

theorem GlobalTheorem.partials_helper3
  (pbar : Pose ℝ) (P : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 0
      (GlobalTheorem.rotproj_outer P w)
      pbar.outerParams =
    inner ℝ (pbar.rotM₂θ P) w

theoremdefined in Noperthedron/Global.lean

complete

theorem GlobalTheorem.partials_helper4 (pbar : Pose ℝ) (P : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 1 (GlobalTheorem.rotproj_outer P w)
      pbar.outerParams =
    inner ℝ (pbar.rotM₂φ P) w

theorem GlobalTheorem.partials_helper4
  (pbar : Pose ℝ) (P : Euc(3))
  (w : Euc(2)) :
  GlobalTheorem.nth_partial 1
      (GlobalTheorem.rotproj_outer P w)
      pbar.outerParams =
    inner ℝ (pbar.rotM₂φ P) 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, let \epsilon_\alpha, \epsilon_{\theta_1}, \epsilon_{\phi_1}, \epsilon_{\theta_2}, \epsilon_{\phi_2} \geq 0 be per-axis radii, 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_\alpha|\langle R'(\alphab) \Mib S,w \rangle| - \epsilon_{\theta_1}|\langle R(\alphab) \Mib^\theta S,w \rangle| - \epsilon_{\phi_1}|\langle R(\alphab) \Mib^\phi S,w \rangle|\\ &- \frac{1}{2}\big(\epsilon_\alpha^2|\langle R(\alphab) \Mib S,w \rangle| + 2\epsilon_\alpha\epsilon_{\theta_1}|\langle R'(\alphab) \Mib^\theta S,w \rangle| + 2\epsilon_\alpha\epsilon_{\phi_1}|\langle R'(\alphab) \Mib^\phi S,w \rangle|\\ &\qquad\quad + \epsilon_{\theta_1}^2|\langle R(\alphab) \Mib^{\theta\theta} S,w \rangle| + 2\epsilon_{\theta_1}\epsilon_{\phi_1}|\langle R(\alphab) \Mib^{\theta\phi} S,w \rangle| + \epsilon_{\phi_1}^2|\langle R(\alphab) \Mib^{\phi\phi} S,w \rangle|\big)\\ &- \frac{(\epsilon_\alpha+\epsilon_{\theta_1}+\epsilon_{\phi_1})^3}{6},\\ H_P \coloneqq{}& \langle \Miib P,w \rangle + \epsilon_{\theta_2}|\langle \Miib^\theta P,w \rangle|+\epsilon_{\phi_2}|\langle \Miib^\varphi P,w \rangle|\\ &+ \frac{1}{2}\big(\epsilon_{\theta_2}^2|\langle \Miib^{\theta\theta} P,w \rangle| + 2\epsilon_{\theta_2}\epsilon_{\phi_2}|\langle \Miib^{\theta\phi} P,w \rangle| + \epsilon_{\phi_2}^2|\langle \Miib^{\phi\phi} P,w \rangle|\big) + \frac{(\epsilon_{\theta_2}+\epsilon_{\phi_2})^3}{6}, \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_{\theta_1}]\times[\phib_1\pm\epsilon_{\phi_1}]\times[\thetab_2\pm\epsilon_{\theta_2}]\times[\phib_2\pm\epsilon_{\phi_2}]\times[\alphab\pm\epsilon_\alpha] \subseteq \R^5.

This is a second-order, anisotropic strengthening of polyhedron.without.rupert, Theorem 17: the exact second partials at the center pose are charged with per-axis weights, and only the cubic Lagrange remainders are bounded via Lemma 5.2.

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.