6. The Local Theorem🔗

Lemma6.1

Group: Linear-algebra lemmas for local geometry. (5)

Group member previews

Preview

Definition 6.2

Loading preview

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

uses 0used by 1✓L∃∀N

For any P \in \mathbb{R}^3 one has \|M(\theta, \phi) P\|^2=\|P\|^2-\langle X(\theta,\varphi),P\rangle^2.

Lean code for Lemma6.1●1 theorem

theoremdefined in Noperthedron/Local/Prelims.lean

complete

theorem Local.pythagoras {θ φ : ℝ} (P : Euc(3)) :
  ‖(rotM θ φ) P‖ ^ 2 = ‖P‖ ^ 2 - inner ℝ (vecX θ φ) P ^ 2

theorem Local.pythagoras {θ φ : ℝ} (P : Euc(3)) :
  ‖(rotM θ φ) P‖ ^ 2 =
    ‖P‖ ^ 2 - inner ℝ (vecX θ φ) P ^ 2

[SY25] Lemma 21.

`rotM θ φ` consists of the first two rows of a rotation whose third row is
`vecX θ φ`, so this is Parseval for that rotated orthonormal basis.

Proof for Lemma 6.1

uses 0

See polyhedron.without.rupert, Lemma 21.

Definition6.2

Group: Linear-algebra lemmas for local geometry. (5)

Group member previews

Preview

Lemma 6.1

Loading preview

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

uses 0used by 1✓L∃∀N

Given v_1, \dots, v_n \in \R^n write \mathrm{span}^+(v_1,\dots,v_n) for the set (simplicial cone) in \R^n defined by

\mathrm{span}^+(v_1,\dots,v_n) = \Big\{ w \in \R^n \colon \exists \lambda_1,\dots,\lambda_n > 0 \text{ s.t. } w = \sum_{i=1}^n \lambda_i v_i \Big\}, $$

which is the natural restriction of \mathrm{span}(v_1,\dots,v_n) to positive weights.

Lean code for Definition6.2●1 definition

defdefined in Noperthedron/Local/Spanp.lean

complete

def Local.Spanp {n : ℕ} (v : Fin n → Euc(n)) : Set Euc(n)

def Local.Spanp {n : ℕ} (v : Fin n → Euc(n)) :
  Set Euc(n)

The positive cone of a finite collection of vectors

Lemma6.3

Group: Linear-algebra lemmas for local geometry. (5)

Group member previews

Preview

Lemma 6.1

Loading preview

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

uses 0used by 1✓L∃∀N

Let V_1,V_2,V_3,Y,Z \in \mathbb{R}^3 with \|Y \|=\| Z \| and Z \in \mathrm{span}^+(V_1,V_2,V_3). Then there exists an i with \langle V_i, Y \rangle \leq \langle V_i, Z \rangle.

Lean code for Lemma6.3●1 theorem

theoremdefined in Noperthedron/Local/Spanp.lean

complete

theorem Local.langles {Y Z : Euc(3)} {V : Fin 3 → Euc(3)} (hYZ : ‖Y‖ = ‖Z‖)
  (hZ : Z ∈ Local.Spanp V) : ∃ i, inner ℝ (V i) Y ≤ inner ℝ (V i) Z

theorem Local.langles {Y Z : Euc(3)}
  {V : Fin 3 → Euc(3)} (hYZ : ‖Y‖ = ‖Z‖)
  (hZ : Z ∈ Local.Spanp V) :
  ∃ i, inner ℝ (V i) Y ≤ inner ℝ (V i) Z

[SY25] Lemma 23, with the unnecessary assumption `Y ∈ Spanp V` removed.
Only `Z` needs a positive expansion: strict inequalities at every generator would
force `⟪Z, Z⟫ < ⟪Z, Y⟫`, contradicting Cauchy–Schwarz and equality of norms.

Proof for Lemma 6.3

uses 0

Write Z=\sum_i c_iV_i with all c_i>0. If every claimed inequality failed, then \langle Z,Z\rangle<\langle Z,Y\rangle by taking the positive weighted sum. But Cauchy--Schwarz gives \langle Z,Y\rangle\leq\|Z\|\|Y\|=\|Z\|^2, a contradiction. Thus the assumption that Y also lies in the positive cone in Lemma 23 of polyhedron.without.rupert is unnecessary.

Lemma6.4

Group: Linear-algebra lemmas for local geometry. (5)

Group member previews

Preview

Lemma 6.1

Loading preview

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

uses 0used by 1✓L∃∀N

For A,\overline{A},B,\overline{B}\in \mathbb{R}^{m\times n} and P_1,P_2\in \mathbb{R}^n it holds that

|\langle AP_1,BP_2\rangle-\langle \overline{A}P_1,\overline{B}P_2\rangle| \leq \|P_1\|\,\|P_2\|\,\big( \|A-\overline{A}\|\,\|\overline{B}\| + \|\overline{A}\|\,\|B-\overline{B}\|+\|A-\overline{A}\|\,\|B-\overline{B}\|\big).

Lean code for Lemma6.4●1 theorem

theoremdefined in Noperthedron/Local/Prelims.lean

complete

theorem Local.abs_sub_inner_bars_le {m n : ℕ} (A B A_ B_ : Euc(m) →L[ℝ] Euc(n))
  (P₁ P₂ : Euc(m)) :
  |inner ℝ (A P₁) (B P₂) - inner ℝ (A_ P₁) (B_ P₂)| ≤
    ‖P₁‖ * ‖P₂‖ *
      (‖A - A_‖ * ‖B_‖ + ‖A_‖ * ‖B - B_‖ + ‖A - A_‖ * ‖B - B_‖)

theorem Local.abs_sub_inner_bars_le {m n : ℕ}
  (A B A_ B_ : Euc(m) →L[ℝ] Euc(n))
  (P₁ P₂ : Euc(m)) :
  |inner ℝ (A P₁) (B P₂) -
        inner ℝ (A_ P₁) (B_ P₂)| ≤
    ‖P₁‖ * ‖P₂‖ *
      (‖A - A_‖ * ‖B_‖ + ‖A_‖ * ‖B - B_‖ +
        ‖A - A_‖ * ‖B - B_‖)

[SY25] Lemma 24

Proof for Lemma 6.4

uses 0

See polyhedron.without.rupert, Lemma 24.

Lemma6.5

Group: Linear-algebra lemmas for local geometry. (5)

Group member previews

Preview

Lemma 6.1

Loading preview

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

uses 0used by 1✓L∃∀N

For A,B\in \mathbb{R}^{m\times n} and P_1,P_2\in \mathbb{R}^n one has

|\langle AP_1,AP_2\rangle-\langle BP_1,BP_2\rangle| \leq \|P_1\|\,\|P_2\|\,\|A-B\|\,(\|A\|+\|B\| + \|A-B\|).

Lean code for Lemma6.5●1 theorem

theoremdefined in Noperthedron/Local/Prelims.lean

complete

theorem Local.abs_sub_inner_le {m n : ℕ} (A B : Euc(m) →L[ℝ] Euc(n))
  (P₁ P₂ : Euc(m)) :
  |inner ℝ (A P₁) (A P₂) - inner ℝ (B P₁) (B P₂)| ≤
    ‖P₁‖ * ‖P₂‖ * ‖A - B‖ * (‖A‖ + ‖B‖ + ‖A - B‖)

theorem Local.abs_sub_inner_le {m n : ℕ}
  (A B : Euc(m) →L[ℝ] Euc(n))
  (P₁ P₂ : Euc(m)) :
  |inner ℝ (A P₁) (A P₂) -
        inner ℝ (B P₁) (B P₂)| ≤
    ‖P₁‖ * ‖P₂‖ * ‖A - B‖ *
      (‖A‖ + ‖B‖ + ‖A - B‖)

[SY25] Lemma 25

Proof for Lemma 6.5

uses 0

See polyhedron.without.rupert, Lemma 25.

Lemma6.6

Group: Linear-algebra lemmas for local geometry. (5)

Group member previews

Preview

Lemma 6.1

Loading preview

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

uses 0used by 1✓L∃∀N

Let A,B,C\in \mathbb{R}^2 be such that \langle R(\pi/2) A,B\rangle, \langle R(\pi/2) B,C\rangle, \langle R(\pi/2) C,A\rangle > 0. Then the origin lies strictly in triangle ABC.

Lean code for Lemma6.6●1 theorem

theoremdefined in Noperthedron/Local/OriginInTriangle.lean

complete

theorem Local.origin_in_triangle {A B C : Euc(2)}
  (hA : 0 < inner ℝ ((rotR (Real.pi / 2)) A) B)
  (hB : 0 < inner ℝ ((rotR (Real.pi / 2)) B) C)
  (hC : 0 < inner ℝ ((rotR (Real.pi / 2)) C) A) :
  ∃ a b c, 0 < a ∧ 0 < b ∧ 0 < c ∧ a • A + b • B + c • C = 0

theorem Local.origin_in_triangle {A B C : Euc(2)}
  (hA :
    0 <
      inner ℝ ((rotR (Real.pi / 2)) A) B)
  (hB :
    0 <
      inner ℝ ((rotR (Real.pi / 2)) B) C)
  (hC :
    0 <
      inner ℝ ((rotR (Real.pi / 2)) C)
        A) :
  ∃ a b c,
    0 < a ∧
      0 < b ∧
        0 < c ∧ a • A + b • B + c • C = 0

[SY25] Lemma 26

Proof for Lemma 6.6

uses 0

See polyhedron.without.rupert, Lemma 26.

Definition6.7

groupuses 0used by 1✓L∃∀N

Owner

David RenshawEffortmediumPriorityhighTagslocalspanningsetup

Let \theta, \varphi \in \mathbb{R}, \varepsilon > 0, and set M := M(\theta, \varphi). Three points P_1, P_2, P_3 \in \mathbb{R}^3 with \|P_1\|, \|P_2\|, \|P_3\| \leq 1 are called \varepsilon-spanning for (\theta, \varphi) if:

\langle R(\pi/2) M P_1,M P_{2}\rangle > 2 \epsilon(\sqrt{2} + \varepsilon)
\langle R(\pi/2) M P_2,M P_{3}\rangle > 2 \epsilon(\sqrt{2} + \varepsilon)
\langle R(\pi/2) M P_3,M P_{1}\rangle > 2 \epsilon(\sqrt{2} + \varepsilon)

Lean code for Definition6.7●1 definition

structure(2 fields)defined in Noperthedron/Local/EpsSpanning.lean

complete

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

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

[SY25] Definition 27. Note that the "+ 1" at the type Fin 3 wraps.

Fields

pos : 0 < ε

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

Lemma6.8

group

Statement uses 2

Statement dependency previews

Preview

Definition 6.2

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 6.14

Loading preview

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

✓L∃∀N

Owner

Jason ReedEffortmediumPriorityhighTagslocalspanningproof

Let P_1, P_2, P_3 \in \mathbb{R}^3 with \|P_1\|,\|P_2\|,\|P_3\| \leq 1 be \epsilon-spanning for (\bar\theta, \bar\phi) and let \theta, \phi \in \mathbb{R} satisfy |\theta - \bar{\theta}|, |\phi - \bar{\phi}| \leq \epsilon. If \langle X(\theta, \phi), P_i \rangle > 0 for i=1,2,3, then X(\theta, \phi) \in \spanp(P_1, P_2, P_3).

Lean code for Lemma6.8●1 theorem

theoremdefined in Noperthedron/Local/EpsSpanning.lean

complete

theorem Local.vecX_spanning {ε θ θ_ φ φ_ : ℝ} (P : Local.Triangle)
  (hθ : |θ - θ_| ≤ ε) (hφ : |φ - φ_| ≤ ε)
  (hSpanning : P.Spanning θ_ φ_ ε) (hP : ∀ (i : Fin 3), ‖P i‖ ≤ 1)
  (hX : ∀ (i : Fin 3), 0 < inner ℝ (vecX θ φ) (P i)) :
  vecX θ φ ∈ Local.Spanp P

theorem Local.vecX_spanning {ε θ θ_ φ φ_ : ℝ}
  (P : Local.Triangle) (hθ : |θ - θ_| ≤ ε)
  (hφ : |φ - φ_| ≤ ε)
  (hSpanning : P.Spanning θ_ φ_ ε)
  (hP : ∀ (i : Fin 3), ‖P i‖ ≤ 1)
  (hX :
    ∀ (i : Fin 3),
      0 < inner ℝ (vecX θ φ) (P i)) :
  vecX θ φ ∈ Local.Spanp P

[SY25] Lemma 28

Proof for Lemma 6.8

Proof uses 3

Proof dependency previews

Preview

Lemma 3.4

Loading preview

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

See polyhedron.without.rupert, Lemma 28.

Lemma6.9

Group: Distance and local-maximality sector estimates. (3)

Group member previews

Preview

Definition 6.10

Loading preview

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

uses 0used by 1✓L∃∀N

Let P, Q \in \mathbb{R}^3 with \|P\|, \|Q\| \leq 1. Let \epsilon>0 and \bar\theta_1,\bar\phi_1,\bar\theta_2,\bar\phi_2,\bar\alpha \in \mathbb{R} satisfy

\|R(\bar\alpha) M(\bar\theta_1, \bar\phi_1) P - M(\bar\theta_2, \bar\phi_2) Q\| \leq 2\delta.

If |\bar\theta_1-\theta_1|, |\bar\phi_1-\phi_1|, |\bar\theta_2-\theta_2|, |\bar\phi_2-\phi_2|, |\bar\alpha - \alpha| \leq \epsilon, then \|R(\alpha)M(\theta_1, \phi_1) P - M(\theta_2, \phi_2) Q\| < 2(\delta + \sqrt{5} \epsilon).

Lean code for Lemma6.9●1 theorem

theoremdefined in Noperthedron/Local.lean

complete

theorem Local.inCirc {δ ε θ₁ θ₁_ θ₂ θ₂_ φ₁ φ₁_ φ₂ φ₂_ α α_ : ℝ} {P Q : Euc(3)}
  (hP : ‖P‖ ≤ 1) (hQ : ‖Q‖ ≤ 1) (hε : 0 < ε) (hθ₁ : |θ₁ - θ₁_| ≤ ε)
  (hφ₁ : |φ₁ - φ₁_| ≤ ε) (hθ₂ : |θ₂ - θ₂_| ≤ ε) (hφ₂ : |φ₂ - φ₂_| ≤ ε)
  (hα : |α - α_| ≤ ε)
  (hδ : ‖(rotR α_) ((rotM θ₁_ φ₁_) P) - (rotM θ₂_ φ₂_) Q‖ ≤ 2 * δ) :
  ‖(rotR α) ((rotM θ₁ φ₁) P) - (rotM θ₂ φ₂) Q‖ < 2 * (δ + √5 * ε)

theorem Local.inCirc
  {δ ε θ₁ θ₁_ θ₂ θ₂_ φ₁ φ₁_ φ₂ φ₂_ α α_ :
    ℝ}
  {P Q : Euc(3)} (hP : ‖P‖ ≤ 1)
  (hQ : ‖Q‖ ≤ 1) (hε : 0 < ε)
  (hθ₁ : |θ₁ - θ₁_| ≤ ε)
  (hφ₁ : |φ₁ - φ₁_| ≤ ε)
  (hθ₂ : |θ₂ - θ₂_| ≤ ε)
  (hφ₂ : |φ₂ - φ₂_| ≤ ε)
  (hα : |α - α_| ≤ ε)
  (hδ :
    ‖(rotR α_) ((rotM θ₁_ φ₁_) P) -
          (rotM θ₂_ φ₂_) Q‖ ≤
      2 * δ) :
  ‖(rotR α) ((rotM θ₁ φ₁) P) -
        (rotM θ₂ φ₂) Q‖ <
    2 * (δ + √5 * ε)

[SY25] Lemma 30, with the two disc memberships around the midpoint T combined
into a single bound on the distance between the two shadow points.

Proof for Lemma 6.9

Proof uses 2

Proof dependency previews

Preview

Lemma 3.4

Loading preview

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

See polyhedron.without.rupert, Lemma 30, which states that both points lie in the disc of radius \delta + \sqrt{5}\epsilon around their midpoint at the reference pose; here the two memberships are combined into a single bound on the distance between the two points.

Definition6.10

Group: Distance and local-maximality sector estimates. (3)

Group member previews

Preview

Lemma 6.9

Loading preview

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

uses 0used by 1✓L∃∀N

Let \PP \subset \R^2 be a convex polygon and Q \in \PP one of its vertices. Define \Sect_\delta(Q) \coloneqq \Circ_{\delta}(Q) \cap \PP^\circ as the intersection between \Circ_{\delta}(Q) and the interior of the convex hull of \PP.

Moreover, Q \in \PP is called \delta-locally maximally distant (\delta-LMD) if for all A \in \Sect_\delta(Q) it holds that \|Q\| > \|A\|.

This centers the disc at Q itself; its radius plays the role of twice the radius in Definition 31 of polyhedron.without.rupert.

Lean code for Definition6.10●1 definition

defdefined in Noperthedron/Local/LocallyMaximallyDistant.lean

complete

def Local.LocallyMaximallyDistant (δ : ℝ) (Q : Euc(2)) (P : Finset Euc(2)) :
  Prop

def Local.LocallyMaximallyDistant (δ : ℝ)
  (Q : Euc(2)) (P : Finset Euc(2)) : Prop

[SY25] Definition 31, simplified: the paper's "Q is δ-LMD with respect to Q_"
uses a ball around an auxiliary center Q_ with ‖Q - Q_‖ < δ, whose only role is
to bound ‖A - Q‖ < 2δ for A in that ball. We center the ball at Q itself, so
the radius here corresponds to the paper's 2δ.

Lemma6.11

Group: Distance and local-maximality sector estimates. (3)

Group member previews

Preview

Lemma 6.9

Loading preview

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

uses 1used by 1✓L∃∀N

Let \mathbf{P} be a convex polygon and Q \in \mathbf{P} a vertex, and let \delta>0. Assume there exists r > 0 with \|Q\| > r such that

\frac{\langle Q, Q - P_j \rangle}{\|Q\|\|Q - P_j\|} \geq \delta/r

for all other vertices P_j \in \mathbf{P} \setminus Q. Then Q is 2\delta-locally maximally distant.

Lean code for Lemma6.11●1 theorem

theoremdefined in Noperthedron/Local/LocallyMaximallyDistant.lean

complete

theorem Local.inner_ge_implies_LMD {P : Finset Euc(2)} {Q : Euc(2)} {δ r : ℝ}
  (hQ : Q ∈ P) (hr : 0 < r) (hrQ : r < ‖Q‖)
  (hle :
    ∀ Pᵢ ∈ P, Pᵢ ≠ Q → δ / r ≤ inner ℝ Q (Q - Pᵢ) / (‖Q‖ * ‖Q - Pᵢ‖)) :
  Local.LocallyMaximallyDistant (2 * δ) Q P

theorem Local.inner_ge_implies_LMD
  {P : Finset Euc(2)} {Q : Euc(2)}
  {δ r : ℝ} (hQ : Q ∈ P) (hr : 0 < r)
  (hrQ : r < ‖Q‖)
  (hle :
    ∀ Pᵢ ∈ P,
      Pᵢ ≠ Q →
        δ / r ≤
          inner ℝ Q (Q - Pᵢ) /
            (‖Q‖ * ‖Q - Pᵢ‖)) :
  Local.LocallyMaximallyDistant (2 * δ) Q
    P

[SY25] Lemma 32, adapted to the Q-centered `LocallyMaximallyDistant`: the ball
of radius 2δ around Q contains the paper's ball of radius δ around any Q_ with
‖Q - Q_‖ < δ, and the cosine bound δ/r is unchanged.

Proof for Lemma 6.11

uses 0

See polyhedron.without.rupert, Lemma 32: the disc of radius 2\delta around Q contains the paper's disc of radius \delta around any \overline Q with \|Q-\overline Q\|<\delta (cf. Definition).

Lemma6.12

Group: Distance and local-maximality sector estimates. (3)

Group member previews

Preview

Lemma 6.9

Loading preview

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

uses 0used by 1✓L∃∀N

Let \epsilon>0 and \theta,\bar\theta, \phi, \bar\phi \in \mathbb{R} with |\theta - \bar{\theta}|, |\phi - \bar{\phi}| \leq \epsilon. Define M = M(\theta, \phi) and \overline{M} = M(\bar\theta, \bar\phi), and let P, Q \in \mathbb{R}^3 with \|P\|, \|Q\| \leq 1. Assume that

\frac{\langle \overline{M} P,\overline{M} (P-Q)\rangle - 2 \epsilon \|P-Q\| \cdot (\sqrt{2}+\varepsilon)}{ \big(\|\overline{M} P\|+\sqrt{2} \varepsilon \big) \cdot \big(\|\overline{M}(P-Q)\|+2 \sqrt{2} \varepsilon\big)} > 0. $$

Then:

\frac{\langle MP,M(P-Q)\rangle}{\|MP\|\,\|M(P-Q)\|} \geq \frac{\langle \overline{M} P,\overline{M} (P-Q)\rangle - 2 \epsilon \|P-Q\| \cdot (\sqrt{2}+\varepsilon)}{ (\|\overline{M} P\|+\sqrt{2} \varepsilon ) \cdot (\|\overline{M}(P-Q)\|+2 \sqrt{2} \varepsilon)}.

Lean code for Lemma6.12●1 theorem

theoremdefined in Noperthedron/Local/Coss.lean

complete

theorem Local.coss {ε θ θ_ φ φ_ : ℝ} {P Q : Euc(3)} (hP : ‖P‖ ≤ 1)
  (hQ : ‖Q‖ ≤ 1) (hε : 0 < ε) (hθ : |θ - θ_| ≤ ε) (hφ : |φ - φ_| ≤ ε) :
  have M := rotM θ φ;
  have M_ := rotM θ_ φ_;
  0 <
      (inner ℝ (M_ P) (M_ (P - Q)) - 2 * ε * ‖P - Q‖ * (√2 + ε)) /
        ((‖M_ P‖ + √2 * ε) * (‖M_ (P - Q)‖ + 2 * √2 * ε)) →
    (inner ℝ (M_ P) (M_ (P - Q)) - 2 * ε * ‖P - Q‖ * (√2 + ε)) /
        ((‖M_ P‖ + √2 * ε) * (‖M_ (P - Q)‖ + 2 * √2 * ε)) ≤
      inner ℝ (M P) (M (P - Q)) / (‖M P‖ * ‖M (P - Q)‖)

theorem Local.coss {ε θ θ_ φ φ_ : ℝ}
  {P Q : Euc(3)} (hP : ‖P‖ ≤ 1)
  (hQ : ‖Q‖ ≤ 1) (hε : 0 < ε)
  (hθ : |θ - θ_| ≤ ε)
  (hφ : |φ - φ_| ≤ ε) :
  have M := rotM θ φ;
  have M_ := rotM θ_ φ_;
  0 <
      (inner ℝ (M_ P) (M_ (P - Q)) -
          2 * ε * ‖P - Q‖ * (√2 + ε)) /
        ((‖M_ P‖ + √2 * ε) *
          (‖M_ (P - Q)‖ + 2 * √2 * ε)) →
    (inner ℝ (M_ P) (M_ (P - Q)) -
          2 * ε * ‖P - Q‖ * (√2 + ε)) /
        ((‖M_ P‖ + √2 * ε) *
          (‖M_ (P - Q)‖ + 2 * √2 * ε)) ≤
      inner ℝ (M P) (M (P - Q)) /
        (‖M P‖ * ‖M (P - Q)‖)

[SY25] Lemma 33

Proof for Lemma 6.12

Proof uses 2

Proof dependency previews

Preview

Lemma 3.4

Loading preview

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

See polyhedron.without.rupert, Lemma 33.

Lemma6.13

uses 0used by 1✓L∃∀N

Owner

Jason ReedEffortsmallPrioritymediumTagslocalcongruence

Let P_1,P_2,P_3, Q_1,Q_2,Q_3 \in \mathbb{R}^3. Define P := (P_1|P_2|P_3) and Q := (Q_1|Q_2|Q_3) and assume Q is invertible. Then P_1, P_2, P_3 and Q_1, Q_2, Q_3 are congruent iff P^t P = Q^t Q.

Lean code for Lemma6.13●1 theorem

theoremdefined in Noperthedron/Local/Congruent.lean

complete

theorem Local.congruent_iff_sym_matrix_eq (P Q : Local.Triangle)
  (hQ : Invertible Q.toMatrix) :
  P.Congruent Q ↔ P.toSymMatrix = Q.toSymMatrix

theorem Local.congruent_iff_sym_matrix_eq
  (P Q : Local.Triangle)
  (hQ : Invertible Q.toMatrix) :
  P.Congruent Q ↔
    P.toSymMatrix = Q.toSymMatrix

[SY25] Lemma 35. Map the basis `Q` to the vectors `P`; equality of their Gram
matrices makes this linear map preserve inner products.

Proof for Lemma 6.13

uses 0

An isometry preserves inner products, so congruence implies equality of the Gram matrices. Conversely, since the Q_i form a basis, define a linear map L by L(Q_i)=P_i. The equality P^t P=Q^t Q says that \langle L(Q_i),L(Q_j)\rangle=\langle Q_i,Q_j\rangle for every i,j. Expanding arbitrary vectors in this basis shows that L preserves all inner products, and hence is the required linear isometry.

For the same construction in matrix form, if a congruence L is given then \langle P_i,P_j\rangle=\langle LQ_i,LQ_j\rangle=\langle Q_i,Q_j\rangle, so P^tP=Q^tQ. Conversely, with L\coloneqq PQ^{-1}, we have L^tL=(PQ^{-1})^t(PQ^{-1})=(Q^t)^{-1}P^tPQ^{-1}=\mathrm{Id} and LQ=PQ^{-1}Q=P, so LQ_i=P_i for each i.

Theorem6.14

uses 0used by 1✓L∃∀N

Owner

David RenshawEffortlargePriorityhighTagslocalmain-theorem

Let \PPP be a polyhedron with radius \rho=1 and P_1, P_2, P_3, Q_1, Q_2, Q_3 \in \PPP be not necessarily distinct. 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 \R, then set \Xib \coloneqq X(\thetab_1,\phib_1), \Xiib \coloneqq X(\thetab_2,\phib_2) as well as \Mib \coloneqq M(\thetab_1,\phib_1), \Miib \coloneqq M(\thetab_2,\phib_2). Assume that there exist \sigma_P, \sigma_Q \in \{0,1\} such that

(-1)^{\sigma_P} \langle \Xib,P_i\rangle>\sqrt{2}\varepsilon \quad \text{and} \quad (-1)^{\sigma_Q} \langle \Xiib , Q_i\rangle>\sqrt{2}\varepsilon, $$

for all i=1,2,3. Moreover, assume that P_1,P_2,P_3 are \epsilon-spanning for (\thetab_1,\phib_1) and that Q_1,Q_2,Q_3 are \epsilon-spanning for (\thetab_2,\phib_2). Finally, assume that for all i = 1,2,3 and any Q_j \in \PPP \setminus Q_i it holds that

\frac{\langle \Miib Q_i,\Miib (Q_i-Q_j)\rangle - 2 \epsilon \|Q_i-Q_j\| \cdot (\sqrt{2}+\varepsilon)}{ \big(\|\Miib Q_i\|+\sqrt{2} \varepsilon \big) \cdot \big(\|\Miib(Q_i-Q_j)\|+2 \sqrt{2} \varepsilon\big)} > \frac{\sqrt{5} \epsilon + \delta}{r}, $$

for some r >0 such that \min_{i=1,2,3}\| \Miib Q_i \| > r + \sqrt{2} \epsilon and for some \delta \in \R with

\delta \geq \max_{i=1,2,3}\left\|R(\alphab) \Mib P_i - \Miib Q_i\right\|/2. $$

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] \coloneqq U \subseteq \R^5.

Lean code for Theorem6.14●1 theorem

theoremdefined in Noperthedron/Local.lean

complete

theorem Local.local_theorem {ι : Type} [Fintype ι] [Nonempty ι]
  (poly : GoodPoly ι) (p_ : Pose ℝ) (ε : ℝ)
  (pc : Local.LocalTheoremPrecondition poly p_ ε) :
  ¬∃ p, p_.near ε ε ε ε ε p ∧ RupertPose p poly.hull

theorem Local.local_theorem {ι : Type} [Fintype ι]
  [Nonempty ι] (poly : GoodPoly ι)
  (p_ : Pose ℝ) (ε : ℝ)
  (pc :
    Local.LocalTheoremPrecondition poly p_
      ε) :
  ¬∃ p,
      p_.near ε ε ε ε ε p ∧
        RupertPose p poly.hull

[SY25] Theorem 36

Proof for Theorem 6.14

Proof uses 8

Proof dependency previews

Preview

Lemma 3.5

Loading preview

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

See polyhedron.without.rupert, Theorem 36.