7. Rational Versions🔗

Definition7.1

Group: Rational trigonometric approximations. (2)

Group member previews

Preview

Lemma 7.2

Loading preview

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

uses 0used by 1✓L∃∀N

Define \ssin, \scos : \mathbb{R} \to \mathbb{R} by truncated Taylor series:

\ssin(x) := x-\frac{x^3}{3!}+\frac{x^5}{5!}\mp\dots+\frac{x^{25}}{25!}
\scos(x) := 1-\frac{x^2}{2!}+\frac{x^4}{4!}\mp\dots+\frac{x^{24}}{24!}

Replacing \sin,\cos with \ssin,\scos defines R_\mathbb{Q}(\alpha), R'_\mathbb{Q}(\alpha), X_\mathbb{Q}(\theta,\phi), M_\mathbb{Q}(\theta,\phi), M^\theta_\mathbb{Q}(\theta,\varphi), M^\phi_\mathbb{Q}(\theta,\varphi).

Lean code for Definition7.1●2 definitions

defdefined in Noperthedron/RationalApprox/Basic.lean

complete

def RationalApprox.sinℚ {k : Type} [Field k] [LinearOrder k] [FloorRing k]
  (x : k) : k

def RationalApprox.sinℚ {k : Type} [Field k]
  [LinearOrder k] [FloorRing k] (x : k) :
  k

Sine partial sum $x - x^3/3! + x^5/5! - ⋯ + x^{25}/25!$, rounded down to a
multiple of `10⁻¹³` (see `round13`).

defdefined in Noperthedron/RationalApprox/Basic.lean

complete

def RationalApprox.cosℚ {k : Type} [Field k] [LinearOrder k] [FloorRing k]
  (x : k) : k

def RationalApprox.cosℚ {k : Type} [Field k]
  [LinearOrder k] [FloorRing k] (x : k) :
  k

Cosine partial sum $1 - x^2/2! + x^4/4! - ⋯ + x^{24}/24!$, rounded down to a
multiple of `10⁻¹³` (see `round13`).

Lemma7.2

Group: Rational trigonometric approximations. (2)

Group member previews

Preview

Definition 7.1

Loading preview

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

uses 1used by 1✓L∃∀N

|\ssin(x)-\sin(x)|\leq \frac{|x|^{27}}{27!} \qquad\text{and}\qquad |\scos(x)-\cos(x)|\leq \frac{|x|^{26}}{26!}.

Lean code for Lemma7.2●2 theorems

theoremdefined in Noperthedron/RationalApprox/TrigLemmas.lean

complete

theorem RationalApprox.sinℚ_approx (x : ℝ) :
  |Real.sin x - RationalApprox.sinℚ x| ≤
    |x| ^ 27 / ↑(Nat.factorial 27) + 1 / 10 ^ 13

theorem RationalApprox.sinℚ_approx (x : ℝ) :
  |Real.sin x - RationalApprox.sinℚ x| ≤
    |x| ^ 27 / ↑(Nat.factorial 27) +
      1 / 10 ^ 13

theoremdefined in Noperthedron/RationalApprox/TrigLemmas.lean

complete

theorem RationalApprox.cosℚ_approx (x : ℝ) :
  |Real.cos x - RationalApprox.cosℚ x| ≤
    |x| ^ 26 / ↑(Nat.factorial 26) + 1 / 10 ^ 13

theorem RationalApprox.cosℚ_approx (x : ℝ) :
  |Real.cos x - RationalApprox.cosℚ x| ≤
    |x| ^ 26 / ↑(Nat.factorial 26) +
      1 / 10 ^ 13

Proof for Lemma 7.2

uses 0

Appeal to Taylor series bounds, using the fact that all absolute values of higher derivatives of sine and cosine never exceed 1.

Lemma7.3

Group: Rational trigonometric approximations. (2)

Group member previews

Preview

Definition 7.1

Loading preview

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

uses 0used by 1✓L∃∀N

For every x\in [-4,4], |\ssin(x)-\sin(x)| \leq \kappa/7 and |\scos(x)-\cos(x)|\leq \kappa/7.

Lean code for Lemma7.3●2 theorems

theoremdefined in Noperthedron/RationalApprox/TrigLemmas.lean

complete

theorem RationalApprox.sinℚ_approx' (x : ℝ) (hx : x ∈ Set.Icc (-4) 4) :
  |Real.sin x - RationalApprox.sinℚ x| ≤ RationalApprox.κ / 7

theorem RationalApprox.sinℚ_approx' (x : ℝ)
  (hx : x ∈ Set.Icc (-4) 4) :
  |Real.sin x - RationalApprox.sinℚ x| ≤
    RationalApprox.κ / 7

theoremdefined in Noperthedron/RationalApprox/TrigLemmas.lean

complete

theorem RationalApprox.cosℚ_approx' (x : ℝ) (hx : x ∈ Set.Icc (-4) 4) :
  |Real.cos x - RationalApprox.cosℚ x| ≤ RationalApprox.κ / 7

theorem RationalApprox.cosℚ_approx' (x : ℝ)
  (hx : x ∈ Set.Icc (-4) 4) :
  |Real.cos x - RationalApprox.cosℚ x| ≤
    RationalApprox.κ / 7

Proof for Lemma 7.3

uses 1

Straightforward numerical calculation from Lemma Lemma 7.2.

Lemma7.4

Group: Matrix approximation error bounds. (4)

Group member previews

Preview

Lemma 7.5

Loading preview

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

uses 0used by 1✓L∃∀N

Let A = (a_{i,j})_{1 \leq i \leq m,\,1 \leq j \leq n} \in \mathbb{R}^{m \times n} and \delta >0. If |a_{i,j}| \leq \delta for all entries, then \|A\| \leq \delta \sqrt{mn}.

Lean code for Lemma7.4●1 theorem

theoremdefined in Noperthedron/RationalApprox/Lemma39.lean

complete

theorem RationalApprox.norm_le_delta_sqrt_dims {m n : ℕ} {δ : ℝ}
  (A : Matrix (Fin m) (Fin n) ℝ) (hδ : 0 < δ)
  (hle : ∀ (i : Fin m) (j : Fin n), |A i j| ≤ δ) :
  ‖LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin A)‖ ≤
    δ * √(↑m * ↑n)

theorem RationalApprox.norm_le_delta_sqrt_dims
  {m n : ℕ} {δ : ℝ}
  (A : Matrix (Fin m) (Fin n) ℝ)
  (hδ : 0 < δ)
  (hle :
    ∀ (i : Fin m) (j : Fin n),
      |A i j| ≤ δ) :
  ‖LinearMap.toContinuousLinearMap
        (Matrix.toEuclideanLin A)‖ ≤
    δ * √(↑m * ↑n)

[SY25] Lemma 39

Proof for Lemma 7.4

uses 0

For any v\in \R^n we have

\begin{align*} \|Av\|^2 &=\sum_{i=1}^m \left(\sum_{j=1}^na_{i,j}v_j\right)^2 \leq \sum_{i=1}^m\left(\sum_{j=1}^n \delta |v_j|\right)^2 = \delta^2 m\left(\sum_{j=1}^n |v_j|\right)^2 \leq \delta^2 m n \|v\|^2 \end{align*} $$

using the Cauchy-Schwarz inequality. Dividing by \|v\| and taking the square root proves the claim.

Lemma7.5

Group: Matrix approximation error bounds. (4)

Group member previews

Preview

Lemma 7.4

Loading preview

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

uses 0used by 1✓L∃∀N

Let A(x,y) be an m\times n matrix (1\le m,n\le 3) whose entries are products of terms in \{0,1,-1,\pm\sin(z),\pm\cos(z)\}. Let A_\mathbb{Q}(x,y) be obtained by replacing \sin,\cos with \ssin,\scos. Then for x,y\in[-4,4], \|A(x,y)-A_{\mathbb{Q}}(x,y)\|\leq\kappa.

Lean code for Lemma7.5●1 theorem

theoremdefined in Noperthedron/RationalApprox/ApproximableMatrices.lean

complete

theorem RationalApprox.norm_matrix_actual_approx_le_kappa
  {m n : ↥(Finset.Icc 1 3)}
  (A : Matrix (Fin ↑m) (Fin ↑n) RationalApprox.DistLeKappaEntry)
  (x y : ↑(Set.Icc (-4) 4)) :
  ‖RationalApprox.clinActual A ↑x ↑y -
        RationalApprox.clinApprox A ↑x ↑y‖ ≤
    RationalApprox.κ

theorem RationalApprox.norm_matrix_actual_approx_le_kappa
  {m n : ↥(Finset.Icc 1 3)}
  (A :
    Matrix (Fin ↑m) (Fin ↑n)
      RationalApprox.DistLeKappaEntry)
  (x y : ↑(Set.Icc (-4) 4)) :
  ‖RationalApprox.clinActual A ↑x ↑y -
        RationalApprox.clinApprox A ↑x
          ↑y‖ ≤
    RationalApprox.κ

[SY25] Lemma 40

Proof for Lemma 7.5

Proof uses 2

Proof dependency previews

Preview

Lemma 7.3

Loading preview

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

We've replaced the assumption a_i(z)\in \{0,1,-1,\pm\sin(z),\pm\cos(z)\} in Steininger and Yurkevich (2025)'s Lemma 40 with a_i(z)\in [-1,1].

By assumption, for fixed x,y every entry of A(x,y)-A_{\mathbb{Q}}(x,y) is of the form a b - \widetilde{a}\widetilde{b} for some a,b\in[-1,1] and |a-\widetilde{a}|,|b-\widetilde{b}|\leq \kappa/7 by Lemma 7.3. This implies that

\begin{align*} |ab-\widetilde{a}\widetilde{b}|&\leq |a b-a\widetilde{b}|+|a \widetilde{b}-\widetilde{a}\widetilde{b}| \\ &=|a|\cdot |b-\widetilde{b}|+|\widetilde{b}|\cdot |a-\widetilde{a}| \leq 1\cdot \kappa/7+(1+\kappa/7) \cdot \kappa/7 <\kappa/3. \end{align*} $$

So we can apply Lemma 7.4 and obtain that \|A(x,y)-A_{\Q}(x,y)\|<\kappa/3\cdot \sqrt{3\cdot 3}=\kappa.

Corollary7.6

Group: Matrix approximation error bounds. (4)

Group member previews

Preview

Lemma 7.4

Loading preview

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

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 7.8

Loading preview

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

✓L∃∀N

Let \alpha,\theta,\phi\in[-4,4]. Then \|R(\alpha)-R_\mathbb{Q}(\alpha)\|, \|R'(\alpha)-R'_\mathbb{Q}(\alpha)\|, \|X(\theta,\phi)-X_\mathbb{Q}(\theta,\phi)\|, \|M(\theta,\phi)-M_\mathbb{Q}(\theta,\phi)\|, \|M^\theta(\theta,\phi)-M^\theta_\mathbb{Q}(\theta,\phi)\|, \|M^\phi(\theta,\phi)-M^\phi_\mathbb{Q}(\theta,\phi)\|, \|M^{\theta\theta}(\theta,\phi)-M^{\theta\theta}_\mathbb{Q}(\theta,\phi)\|, \|M^{\theta\phi}(\theta,\phi)-M^{\theta\phi}_\mathbb{Q}(\theta,\phi)\|, and \|M^{\phi\phi}(\theta,\phi)-M^{\phi\phi}_\mathbb{Q}(\theta,\phi)\| are all at most \kappa. Moreover the corresponding rational matrices R_\mathbb{Q}, R'_\mathbb{Q}, M_\mathbb{Q}, M^\theta_\mathbb{Q}, M^\phi_\mathbb{Q}, M^{\theta\theta}_\mathbb{Q}, M^{\theta\phi}_\mathbb{Q}, and M^{\phi\phi}_\mathbb{Q} have norm at most 1+\kappa.

Lean code for Corollary7.6●17 theorems

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.R_difference_norm_bounded (α : ℝ)
  (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR α - RationalApprox.rotRℚℝ α‖ ≤ RationalApprox.κ

theorem RationalApprox.R_difference_norm_bounded
  (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR α - RationalApprox.rotRℚℝ α‖ ≤
    RationalApprox.κ

Proof of [SY25] Corollary 41

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.R'_difference_norm_bounded (α : ℝ)
  (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR' α - RationalApprox.rotR'ℚℝ α‖ ≤ RationalApprox.κ

theorem RationalApprox.R'_difference_norm_bounded
  (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR' α - RationalApprox.rotR'ℚℝ α‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.M_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotM θ φ - RationalApprox.rotMℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.M_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotM θ φ - RationalApprox.rotMℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mθ_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθ θ φ - RationalApprox.rotMθℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.Mθ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθ θ φ -
        RationalApprox.rotMθℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mφ_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMφ θ φ - RationalApprox.rotMφℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.Mφ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMφ θ φ -
        RationalApprox.rotMφℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mθθ_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθθ θ φ - RationalApprox.rotMθθℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.Mθθ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθθ θ φ -
        RationalApprox.rotMθθℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mθφ_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθφ θ φ - RationalApprox.rotMθφℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.Mθφ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθφ θ φ -
        RationalApprox.rotMθφℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mφφ_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMφφ θ φ - RationalApprox.rotMφφℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.Mφφ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMφφ θ φ -
        RationalApprox.rotMφφℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.X_difference_norm_bounded (θ φ : ℝ)
  (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖vecXL θ φ - RationalApprox.vecXLℚℝ θ φ‖ ≤ RationalApprox.κ

theorem RationalApprox.X_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖vecXL θ φ -
        RationalApprox.vecXLℚℝ θ φ‖ ≤
    RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Rℚ_norm_bounded (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotRℚℝ α‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Rℚ_norm_bounded (α : ℝ)
  (hα : α ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotRℚℝ α‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMℚℝ θ φ‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Mℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.R'ℚ_norm_bounded (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotR'ℚℝ α‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.R'ℚ_norm_bounded (α : ℝ)
  (hα : α ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotR'ℚℝ α‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mθℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθℚℝ θ φ‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Mθℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mφℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMφℚℝ θ φ‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Mφℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMφℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mθθℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθθℚℝ θ φ‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Mθθℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθθℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mθφℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθφℚℝ θ φ‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Mθφℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθφℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theoremdefined in Noperthedron/RationalApprox/MatrixBounds.lean

complete

theorem RationalApprox.Mφφℚ_norm_bounded {θ φ : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMφφℚℝ θ φ‖ ≤ 1 + RationalApprox.κ

theorem RationalApprox.Mφφℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMφφℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

Proof for Corollary 7.6

Proof uses 2

Proof dependency previews

Preview

Lemma 3.1

Loading preview

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

The first statement is a direct application of Lemma 7.5 and the second statement follows immediately after using Lemma 3.1 and the triangle inequality. The derivative norm bounds follow similarly, using that the operator norms of R', M^\theta, and M^\phi are at most 1.

Lemma7.7

Group: Matrix approximation error bounds. (4)

Group member previews

Preview

Lemma 7.4

Loading preview

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

uses 0

Used by 3

Reverse dependency previews

Preview

Lemma 7.8

Loading preview

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

✓L∃∀N

Lean code for Lemma7.7●1 theorem

theoremdefined in Noperthedron/RationalApprox/Lemma42.lean

complete

theorem RationalApprox.norm_sub_le_prod {n m : ℕ}
  (mv : RationalApprox.MatVec n m) (κ : ℝ) (κ_pos : κ > 0)
  (hκ : mv.DiffBoundedBy κ) :
  ‖mv.compA - mv.compB‖ ≤ ↑mv.size * κ * mv.maxNormList.prod

theorem RationalApprox.norm_sub_le_prod {n m : ℕ}
  (mv : RationalApprox.MatVec n m) (κ : ℝ)
  (κ_pos : κ > 0)
  (hκ : mv.DiffBoundedBy κ) :
  ‖mv.compA - mv.compB‖ ≤
    ↑mv.size * κ * mv.maxNormList.prod

[SY25] Lemma 42

Proof for Lemma 7.7

uses 0

See polyhedron.without.rupert, Lemma 42.

Lemma7.8

Group: Matrix approximation error bounds. (4)

Group member previews

Preview

Lemma 7.4

Loading preview

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

uses 0used by 1✓L∃∀N

Let \alpha, \theta, \phi \in [-4,4], P\in \R^3 with \|P\| \leq 1 and let \widetilde{P} be a \kappa-rational approximation of P. Set M = M(\theta, \phi) and M_{\Q} = M_{\Q}(\theta, \phi), M^\theta = M^\theta(\theta, \phi) and M^\theta_{\Q} = M^\theta_{\Q}(\theta, \phi), M^\phi = M^\phi(\theta, \phi) and M^\phi_{\Q} = M^\phi_{\Q}(\theta, \phi), as well as R = R(\alpha), R_{\Q} = R_{\Q}(\alpha), R' = R'(\alpha), R'_{\Q} = R'_{\Q}(\alpha). Finally let w \in \R^2 with \|w\| = 1. Then:

\begin{align} | \langle M P, w\rangle - \langle M_{\Q} \widetilde{P}, w\rangle | & \leq 3\kappa \\ | \langle M^\theta P, w\rangle - \langle M^\theta_{\Q} \widetilde{P}, w\rangle | & \leq 3\kappa,\\ | \langle M^\phi P, w\rangle - \langle M^\phi_{\Q} \widetilde{P}, w\rangle | & \leq 3\kappa,\\ | \langle R M P, w\rangle - \langle R_{\Q} M_{\Q} \widetilde{P}, w\rangle | & \leq 4\kappa \\ | \langle R' M P, w\rangle - \langle R'_{\Q} M_{\Q} \widetilde{P}, w\rangle | & \leq 4\kappa,\\ | \langle R M^\theta P, w\rangle - \langle R_{\Q} M^\theta_{\Q} \widetilde{P}, w\rangle | & \leq 4\kappa,\\ | \langle R M^\phi P, w\rangle - \langle R_{\Q} M^\phi_{\Q} \widetilde{P}, w\rangle | & \leq 4\kappa. \end{align} $$

The same bounds hold with M replaced by any of the second-derivative matrices M^{\theta\theta}, M^{\theta\phi}, or M^{\phi\phi} (at 3\kappa without a rotation factor and 4\kappa with R in front), and with R' in place of R in front of M^\theta and M^\phi.

Lean code for Lemma7.8●15 theorems

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_M {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotM ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤
    2 * RationalApprox.κ + RationalApprox.κ ^ 2

theorem RationalApprox.bounds_kappa_M {P : Euc(3)}
  {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotM ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    2 * RationalApprox.κ +
      RationalApprox.κ ^ 2

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_Mθ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤
    2 * RationalApprox.κ + RationalApprox.κ ^ 2

theorem RationalApprox.bounds_kappa_Mθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    2 * RationalApprox.κ +
      RationalApprox.κ ^ 2

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_Mφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMφℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤
    2 * RationalApprox.κ + RationalApprox.κ ^ 2

theorem RationalApprox.bounds_kappa_Mφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMφℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    2 * RationalApprox.κ +
      RationalApprox.κ ^ 2

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_RM {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotM ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α) ((RationalApprox.rotMℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_RM
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotM ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_R'M {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR' ↑↑α) ((rotM ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_R'M
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR' ↑↑α) ((rotM ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_RMθ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotMθ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_RMθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α) ((rotMθ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_RMφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotMφ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMφℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_RMφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α) ((rotMφ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMφℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_Mθθ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθθ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθθℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤
    2 * RationalApprox.κ + RationalApprox.κ ^ 2

theorem RationalApprox.bounds_kappa_Mθθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθθ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθθℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    2 * RationalApprox.κ +
      RationalApprox.κ ^ 2

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_Mθφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθφℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤
    2 * RationalApprox.κ + RationalApprox.κ ^ 2

theorem RationalApprox.bounds_kappa_Mθφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθφℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    2 * RationalApprox.κ +
      RationalApprox.κ ^ 2

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_Mφφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMφφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMφφℚ ↑θ ↑φ) P_ ⬝ᵥ w)‖ ≤
    2 * RationalApprox.κ + RationalApprox.κ ^ 2

theorem RationalApprox.bounds_kappa_Mφφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMφφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMφφℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    2 * RationalApprox.κ +
      RationalApprox.κ ^ 2

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_R'Mθ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR' ↑↑α) ((rotMθ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMθℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_R'Mθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR' ↑↑α)
            ((rotMθ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMθℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_R'Mφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR' ↑↑α) ((rotMφ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMφℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_R'Mφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR' ↑↑α)
            ((rotMφ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMφℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_RMθθ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotMθθ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθθℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_RMθθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α)
            ((rotMθθ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθθℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_RMθφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotMθφ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθφℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_RMθφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α)
            ((rotMθφ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθφℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theoremdefined in Noperthedron/RationalApprox/BoundsKappa.lean

complete

theorem RationalApprox.bounds_kappa_RMφφ {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)} {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx : ‖P - toR3 P_‖ ≤ RationalApprox.κ) (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotMφφ ↑↑θ ↑↑φ) P)) (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMφφℚ ↑θ ↑φ) P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ + 3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

theorem RationalApprox.bounds_kappa_RMφφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α)
            ((rotMφφ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMφφℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ +
        3 * RationalApprox.κ ^ 2 +
      RationalApprox.κ ^ 3

Proof for Lemma 7.8

Proof uses 2

Proof dependency previews

Preview

Corollary 7.6

Loading preview

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

See polyhedron.without.rupert, Lemma 44.

Theorem7.9

uses 0used by 1✓L∃∀N

Let \PPP be a pointsymmetric convex polyhedron with radius \rho =1 and \widetilde{\PPP} a \kappa-rational approximation. Let \widetilde{S} \in \widetilde{\PPP}. Further let \epsilon_\alpha, \epsilon_{\theta_1}, \epsilon_{\phi_1}, \epsilon_{\theta_2}, \epsilon_{\phi_2} \in \Q_{\geq 0} be per-axis radii and let \thetab_1,\phib_1,\thetab_2,\phib_2,\alphab \in \Q \cap [-4,4]. Let w\in\Q^2 be a unit vector. Denote \Mib \coloneqq M_{\Q}(\thetab_1, \phib_1), \Miib \coloneqq M_{\Q}(\thetab_2, \phib_2) as well as \Mib^{\theta} \coloneqq M_{\Q}^\theta(\thetab_1, \phib_1), \Mib^{\phi} \coloneqq M_{\Q}^\phi(\thetab_1, \phib_1) and analogously for \Miib^{\theta}, \Miib^{\phi}. Write E_1 \coloneqq \epsilon_\alpha + \epsilon_{\theta_1} + \epsilon_{\phi_1} and E_2 \coloneqq \epsilon_{\theta_2} + \epsilon_{\phi_2}, and set

\begin{align*} G^{\Q} \coloneqq{}& \langle R_{\Q}(\alphab) \Mib \widetilde{S},w \rangle - \epsilon_\alpha|\langle R_{\Q}'(\alphab) \Mib \widetilde{S},w \rangle| - \epsilon_{\theta_1}|\langle R_{\Q}(\alphab) \Mib^\theta \widetilde{S},w \rangle| - \epsilon_{\phi_1}|\langle R_{\Q}(\alphab) \Mib^\phi \widetilde{S},w \rangle| \\ &- \frac{1}{2}\big(\epsilon_\alpha^2|\langle R_{\Q}(\alphab) \Mib \widetilde{S},w \rangle| + 2\epsilon_\alpha\epsilon_{\theta_1}|\langle R_{\Q}'(\alphab) \Mib^\theta \widetilde{S},w \rangle| + 2\epsilon_\alpha\epsilon_{\phi_1}|\langle R_{\Q}'(\alphab) \Mib^\phi \widetilde{S},w \rangle|\\ &\qquad\quad + \epsilon_{\theta_1}^2|\langle R_{\Q}(\alphab) \Mib^{\theta\theta} \widetilde{S},w \rangle| + 2\epsilon_{\theta_1}\epsilon_{\phi_1}|\langle R_{\Q}(\alphab) \Mib^{\theta\phi} \widetilde{S},w \rangle| + \epsilon_{\phi_1}^2|\langle R_{\Q}(\alphab) \Mib^{\phi\phi} \widetilde{S},w \rangle|\big)\\ & \hspace{9cm}- \frac{E_1^3}{6} - 4\kappa \big( 1 + E_1 + \tfrac12 E_1^2\big),\\ H^{\Q}_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{E_2^3}{6} + 3\kappa\big( 1+E_2+\tfrac12 E_2^2\big). \end{align*} $$

If G^{\Q}>\max_{P\in \widetilde{\PPP}} H^{\Q}_P then there does not exist a solution to Rupert's condition to \PPP with

(\theta_1,\varphi_1,\theta_2,\varphi_2,\alpha) \in [\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]. $$

On the diagonal \epsilon_\alpha = \dots = \epsilon, the rational slack terms become 4\kappa(1+3\epsilon+\tfrac92\epsilon^2) and 3\kappa(1+2\epsilon+2\epsilon^2).

Lean code for Theorem7.9●1 theorem

theoremdefined in Noperthedron/RationalApprox/RationalGlobal.lean

complete

theorem RationalApprox.GlobalTheorem.rational_global {ι : Type} [Fintype ι]
  [Nonempty ι] (p : Pose ℚ) (εα εθ₁ εφ₁ εθ₂ εφ₂ : ℚ) (hεα : 0 ≤ εα)
  (hεθ₁ : 0 ≤ εθ₁) (hεφ₁ : 0 ≤ εφ₁) (hεθ₂ : 0 ≤ εθ₂) (hεφ₂ : 0 ≤ εφ₂)
  (poly : GoodPoly ι) (poly_ : Polyhedron ι (Fin 3 → ℚ))
  (happrox : RationalApprox.κApproxPoly poly.vertices poly_)
  (pc :
    RationalApprox.GlobalTheorem.RationalGlobalTheoremPrecondition poly_
      p εα εθ₁ εφ₁ εθ₂ εφ₂) :
  ¬∃ q,
      p.toReal.near (↑εα) (↑εθ₁) (↑εφ₁) (↑εθ₂) (↑εφ₂) q ∧
        RupertPose q poly.hull

theorem RationalApprox.GlobalTheorem.rational_global
  {ι : Type} [Fintype ι] [Nonempty ι]
  (p : Pose ℚ) (εα εθ₁ εφ₁ εθ₂ εφ₂ : ℚ)
  (hεα : 0 ≤ εα) (hεθ₁ : 0 ≤ εθ₁)
  (hεφ₁ : 0 ≤ εφ₁) (hεθ₂ : 0 ≤ εθ₂)
  (hεφ₂ : 0 ≤ εφ₂) (poly : GoodPoly ι)
  (poly_ : Polyhedron ι (Fin 3 → ℚ))
  (happrox :
    RationalApprox.κApproxPoly
      poly.vertices poly_)
  (pc :
    RationalApprox.GlobalTheorem.RationalGlobalTheoremPrecondition
      poly_ p εα εθ₁ εφ₁ εθ₂ εφ₂) :
  ¬∃ q,
      p.toReal.near (↑εα) (↑εθ₁) (↑εφ₁)
          (↑εθ₂) (↑εφ₂) q ∧
        RupertPose q poly.hull

[SY25] Theorem 43, with per-axis widths and a box conclusion in place of the
closed ball.

Proof for Theorem 7.9

Proof uses 2

Proof dependency previews

Preview

Theorem 5.5

Loading preview

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

Definition7.10

Group: Local theorem approximation bounds. (3)

Group member previews

Preview

Lemma 7.11

Loading preview

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

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 7.11

Loading preview

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

✓L∃∀N

Let \theta, \phi \in \Q \cap [-4,4] and M_{\Q} \coloneqq M_{\Q}(\theta, \phi). Three points \widetilde{P}_1, \widetilde{P}_2, \widetilde{P}_3 \in \Q^3 with \|\widetilde{P}_1\|, \|\widetilde{P}_2\|, \|\widetilde{P}_3\| \leq 1+\kappa are called \epsilon-\kappa-spanning for (\theta, \phi) if it holds that:

\begin{align*} \langle R(\pi/2) M_{\Q} \widetilde{P}_1,M_{\Q} \widetilde{P}_{2}\rangle > 2 \epsilon(\sqrt{2} + \epsilon) + 6\kappa,\\ \langle R(\pi/2) M_{\Q} \widetilde{P}_2,M_{\Q} \widetilde{P}_{3}\rangle > 2 \epsilon(\sqrt{2} + \epsilon) + 6\kappa,\\ \langle R(\pi/2) M_{\Q} \widetilde{P}_3,M_{\Q} \widetilde{P}_{1}\rangle > 2 \epsilon(\sqrt{2} + \epsilon) + 6\kappa. \end{align*} $$

Lean code for Definition7.10●1 definition

structure(2 fields)defined in Noperthedron/RationalApprox/EpsKapSpanning.lean

complete

structure Local.Triangle.κSpanning (P : Local.Triangle) (θ φ ε : ℝ) : Prop

structure Local.Triangle.κSpanning
  (P : Local.Triangle) (θ φ ε : ℝ) : Prop

[SY25] Definition 45. Note that the "+ 1" at the type Fin 3 wraps.
We don't include in this definition the constraint that θ, φ ∈ [-4, 4] or
that ‖P₁‖, ‖P₂‖, ‖P₃‖ ≤ 1 + κ.
If a user of this code wants to impose those, they'll have to separately.

Fields

pos : 0 < ε

lt : ∀ (i : Fin 3),
  2 * ε * (√2 + ε) + 6 * RationalApprox.κ <
    inner ℝ ((rotR (Real.pi / 2)) ((RationalApprox.rotMℚℝ θ φ) (P i))) ((RationalApprox.rotMℚℝ θ φ) (P (i + 1)))

Lemma7.11

Group: Local theorem approximation bounds. (3)

Group member previews

Preview

Definition 7.10

Loading preview

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

uses 1used by 1✓L∃∀N

Let P_1, P_2, P_3 \in \R^3 with \|P_i\| \leq 1 and \widetilde{P}_1, \widetilde{P}_2, \widetilde{P}_3 \in \Q^3 be their \kappa-rational approximations. Assume that \widetilde{P}_1, \widetilde{P}_2, \widetilde{P}_3 are \epsilon-\kappa-spanning for some \theta, \phi \in \Q \cap [-4,4], then P_1, P_2, P_3 are \epsilon-spanning for \theta, \phi.

Lean code for Lemma7.11●1 theorem

theoremdefined in Noperthedron/RationalApprox/EpsKapSpanning.lean

complete

theorem RationalApprox.ek_spanning_imp_e_spanning (P P' : Local.Triangle)
  (hk : RationalApprox.κApproxTri P P') (hP : ∀ (i : Fin 3), ‖P i‖ ≤ 1)
  {θ φ ε : ℝ} (hθ : θ ∈ Set.Icc (-4) 4) (hφ : φ ∈ Set.Icc (-4) 4)
  (hspan : P'.κSpanning θ φ ε) : P.Spanning θ φ ε

theorem RationalApprox.ek_spanning_imp_e_spanning
  (P P' : Local.Triangle)
  (hk : RationalApprox.κApproxTri P P')
  (hP : ∀ (i : Fin 3), ‖P i‖ ≤ 1)
  {θ φ ε : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4)
  (hspan : P'.κSpanning θ φ ε) :
  P.Spanning θ φ ε

Proof for Lemma 7.11

Proof uses 3

Proof dependency previews

Preview

Lemma 6.8

Loading preview

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

See polyhedron.without.rupert, Lemma 46.

Lemma7.12

Group: Local theorem approximation bounds. (3)

Group member previews

Preview

Definition 7.10

Loading preview

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

uses 0

Used by 2

Reverse dependency previews

Preview

Corollary 7.13

Loading preview

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

✓L∃∀N

Let P \in \mathbb{R}^3 with \|P\| \leq 1 and let \widetilde{P} be a \kappa-rational approximation of P. For \theta, \phi \in [-4,4], set X = X(\theta, \phi) and X_{\mathbb{Q}} = X_{\mathbb{Q}}(\theta, \phi). Then |\langle X, P \rangle - \langle X_{\mathbb{Q}}, \widetilde{P} \rangle| \leq 3\kappa.

The inner-product and norm bounds for M and M_{\mathbb{Q}} from Lemma 49 of polyhedron.without.rupert are formalized only in the generalized forms used by Corollary 7.13.

Lean code for Lemma7.12●1 theorem

theoremdefined in Noperthedron/RationalApprox/BoundsKappa3.lean

complete

theorem RationalApprox.bounds_kappa3_X {P P_ : Euc(3)} {θ φ : ↑(Set.Icc (-4) 4)}
  (hP : ‖P‖ ≤ 1) (Papprox : ‖P - P_‖ ≤ RationalApprox.κ) :
  ‖inner ℝ (vecX ↑θ ↑φ) P - inner ℝ (RationalApprox.vecXℚℝ ↑θ ↑φ) P_‖ ≤
    3 * RationalApprox.κ

theorem RationalApprox.bounds_kappa3_X
  {P P_ : Euc(3)}
  {θ φ : ↑(Set.Icc (-4) 4)} (hP : ‖P‖ ≤ 1)
  (Papprox :
    ‖P - P_‖ ≤ RationalApprox.κ) :
  ‖inner ℝ (vecX ↑θ ↑φ) P -
        inner ℝ
          (RationalApprox.vecXℚℝ ↑θ ↑φ)
          P_‖ ≤
    3 * RationalApprox.κ

Proof for Lemma 7.12

uses 1

See polyhedron.without.rupert, Lemma 49.

Corollary7.13

Group: Local theorem approximation bounds. (3)

Group member previews

Preview

Definition 7.10

Loading preview

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

uses 0used by 1✓L∃∀N

In the setting of Lemma 7.12, let \sqrt[+]{x} be an upper square-root function, i.e., \sqrt{x} \leq \sqrt[+]{x} for all real x \geq 0 with rational output on rational input. Set \|x\|_{+} \coloneqq \sqrt[+]{\|x\|^2}. Set

A = \frac{\langle M P, M(P-Q)\rangle - 2 \epsilon \|P-Q\| \cdot (\sqrt{2}+\varepsilon)}{ \big(\| M P\|+\sqrt{2} \varepsilon \big) \cdot \big(\|M(P-Q)\|+2 \sqrt{2} \varepsilon\big)} $$

as well as

A_{\Q} = \frac{\langle M_{\Q} \widetilde{P}, M_{\Q} (\widetilde{P}-\widetilde{Q})\rangle - 10\kappa - 2 \epsilon ( \|\widetilde{P}-\widetilde{Q}\| + 2 \kappa ) \cdot (\sqrt{2}+\varepsilon)}{ \big(\| M_{\Q} \widetilde{P}\|_{+}+\sqrt{2} \varepsilon + 3\kappa \big) \cdot \big(\|M_{\Q}(\widetilde{P}-\widetilde{Q})\|_{+}+2 \sqrt{2} \varepsilon + 6\kappa\big)}. $$

Assume that A \geq 0. Then A \geq A_{\mathbb{Q}}.

In the Lean formalization, each applied vector M_{\Q}\widetilde{x} in A_{\Q} is additionally rounded down componentwise to a multiple of 10^{-13} so that the checker's dot products and norms use small denominators; the resulting perturbation is absorbed into the existing slack terms.

Lean code for Corollary7.13●1 theorem

theoremdefined in Noperthedron/RationalApprox/BoundsKappa4.lean

complete

theorem RationalApprox.bounds_kappa4 (P Q : Euc(3)) (P_ Q_ : Fin 3 → ℚ)
  (p : Pose ℚ) (hθBound : ↑p.θ₂ ∈ Set.Icc (-4) 4)
  (hφBound : ↑p.φ₂ ∈ Set.Icc (-4) 4) (hP : ‖P‖ ≤ 1) (hQ : ‖Q‖ ≤ 1)
  (Papprox : ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (Qapprox : ‖Q - toR3 Q_‖ ≤ RationalApprox.κ) (ε : ℝ) (hε : 0 < ε)
  (s : RationalApprox.UpperSqrt)
  (hA_nonneg :
    0 ≤
      inner ℝ ((rotM ↑p.θ₂ ↑p.φ₂) P) ((rotM ↑p.θ₂ ↑p.φ₂) (P - Q)) -
        2 * ε * ‖P - Q‖ * (√2 + ε)) :
  RationalApprox.bounds_kappa4_Aℚ P_ Q_ p ε s ≤
    RationalApprox.bounds_kappa4_A P Q ⟨↑p.θ₂, hθBound⟩ ⟨↑p.φ₂, hφBound⟩
      ε

theorem RationalApprox.bounds_kappa4
  (P Q : Euc(3)) (P_ Q_ : Fin 3 → ℚ)
  (p : Pose ℚ)
  (hθBound : ↑p.θ₂ ∈ Set.Icc (-4) 4)
  (hφBound : ↑p.φ₂ ∈ Set.Icc (-4) 4)
  (hP : ‖P‖ ≤ 1) (hQ : ‖Q‖ ≤ 1)
  (Papprox :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (Qapprox :
    ‖Q - toR3 Q_‖ ≤ RationalApprox.κ)
  (ε : ℝ) (hε : 0 < ε)
  (s : RationalApprox.UpperSqrt)
  (hA_nonneg :
    0 ≤
      inner ℝ ((rotM ↑p.θ₂ ↑p.φ₂) P)
          ((rotM ↑p.θ₂ ↑p.φ₂) (P - Q)) -
        2 * ε * ‖P - Q‖ * (√2 + ε)) :
  RationalApprox.bounds_kappa4_Aℚ P_ Q_ p
      ε s ≤
    RationalApprox.bounds_kappa4_A P Q
      ⟨↑p.θ₂, hθBound⟩ ⟨↑p.φ₂, hφBound⟩ ε

[SY25] Corollary 51

Proof for Corollary 7.13

uses 1

See polyhedron.without.rupert, Corollary 51.

Theorem7.14

uses 1used by 1✓L∃∀N

Let \PPP be a polyhedron with radius \rho=1 and \widetilde{P}_i be a \kappa-rational approximation of P_i \in \PPP. Set \widetilde{\PPP} = \{\widetilde{P}_i \text{ for } P_i \in \PPP \}. Let P_1, P_2, P_3, Q_1, Q_2, Q_3 \in \PPP be not necessarily distinct and assume that P_1, P_2, P_3 and Q_1, Q_2, Q_3 are congruent. Let \epsilon>0 and \thetab_1,\phib_1,\thetab_2,\phib_2,\alphab \in \Q \cap [-4,4]. Set \Xib \coloneqq X_{\Q}(\thetab_1,\phib_1), \Xiib \coloneqq X_{\Q}(\thetab_2,\phib_2) as well as \Mib \coloneqq M_{\Q}(\thetab_1,\phib_1), \Miib \coloneqq M_{\Q}(\thetab_2,\phib_2). Assume that there exist \sigma_P, \sigma_Q \in \{0,1\} such that

(-1)^{\sigma_P} \langle \Xib,\widetilde{P}_i\rangle>\sqrt{2}\varepsilon + 3\kappa \quad \text{and} \quad (-1)^{\sigma_Q} \langle \Xiib , \widetilde{Q}_i\rangle>\sqrt{2}\varepsilon + 3\kappa, $$

for all i=1,2,3. Moreover, assume that \widetilde{P}_1,\widetilde{P}_2,\widetilde{P}_3 are \epsilon-\kappa-spanning for (\thetab_1,\phib_1) and that \widetilde{Q}_1,\widetilde{Q}_2,\widetilde{Q}_3 are \epsilon-\kappa-spanning for (\thetab_2,\phib_2). Let \sqrt[+]{x} and \sqrt[-]{x} be upper- and lower-square-root functions, then set \|Z\|_{+} \coloneqq \sqrt[+]{\|Z\|^2} and \|Z\|_{-} \coloneqq \sqrt[-]{\|Z\|^2} for Z \in \R^n. Finally, assume that for all i = 1,2,3 and any \widetilde{Q}_j \in \widetilde{\PPP} \setminus \widetilde{Q}_i it holds that the rational inequality (B^{\Q}_\epsilon) from the paper is satisfied, for some r >0 such that \min_{i=1,2,3}\| \Miib \widetilde{Q}_i \|_{-} > r + \sqrt{2} \epsilon + 3\kappa and for some \delta \in \R with

\delta \geq \max_{i=1,2,3}\left\|R_{\Q}(\alphab) \Mib \widetilde{P}_i-\Miib \widetilde{Q}_i\right\|_{+}/2 + 3\kappa. $$

Then there exists no solution to Rupert's problem R(\alpha) M(\theta_1,\phi_1)\PPP \subset M(\theta_2,\phi_2)\PPP^\circ with

(\theta_1, \phi_1, \theta_2, \phi_2, \alpha) \in [\thetab_1\pm\epsilon,\phib_1\pm\epsilon,\thetab_2\pm\epsilon,\phib_2\pm\epsilon,\alphab\pm\epsilon] \subseteq \R^5. $$

In the Lean formalization, the applied vector \Miib\widetilde Q_i in the r-condition is additionally rounded down componentwise to a multiple of 10^{-13}; the resulting perturbation is absorbed into the 3\kappa term.

Lean code for Theorem7.14●1 theorem

theoremdefined in Noperthedron/RationalApprox/RationalLocal.lean

complete

theorem RationalApprox.LocalTheorem.rational_local {ι : Type} [Fintype ι]
  [DecidableEq ι] [Nonempty ι] (poly : GoodPoly ι)
  (poly_ : Polyhedron ι (Fin 3 → ℚ))
  (hpoly : RationalApprox.κApproxPoly poly.vertices poly_) (p_ : Pose ℚ)
  (ε : ℚ)
  (pc :
    RationalApprox.LocalTheorem.RationalLocalTheoremPrecondition poly
      poly_ hpoly p_ ε) :
  ¬∃ p,
      p_.toReal.near (↑ε) (↑ε) (↑ε) (↑ε) (↑ε) p ∧ RupertPose p poly.hull

theorem RationalApprox.LocalTheorem.rational_local
  {ι : Type} [Fintype ι] [DecidableEq ι]
  [Nonempty ι] (poly : GoodPoly ι)
  (poly_ : Polyhedron ι (Fin 3 → ℚ))
  (hpoly :
    RationalApprox.κApproxPoly
      poly.vertices poly_)
  (p_ : Pose ℚ) (ε : ℚ)
  (pc :
    RationalApprox.LocalTheorem.RationalLocalTheoremPrecondition
      poly poly_ hpoly p_ ε) :
  ¬∃ p,
      p_.toReal.near (↑ε) (↑ε) (↑ε) (↑ε)
          (↑ε) p ∧
        RupertPose p poly.hull

[SY25] Theorem 48 "The Rational Local Theorem"

Proof for Theorem 7.14

Proof uses 4

Proof dependency previews

Preview

Theorem 6.14

Loading preview

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