Grace/Cumulus/Geometry/Euclid/Ball.g17

Open in Workbench Download source

Imports

Motions

Declarations

• unitBall def
• puncturedBall def
• puncturedBall.graph theorem derivation
• unitBall.subset theorem derivation
• unitBall.function theorem derivation
• puncturedBall.membership theorem derivation
• puncturedBall.subset theorem derivation
• puncturedBall.subset_space theorem derivation
• zeroVector.in_ball theorem derivation
• sphere.subset_ball theorem derivation
• sphere.subset_punctured theorem derivation
• unitBall.rotate theorem derivation
• matrixVector.eq_zero theorem derivation
• puncturedBall.rotate theorem derivation
• puncturedBall.invariant theorem derivation

Source

1-- The closed unit ball of ℝ³ and the punctured ball, which every rotation2-- carries into itself3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Geometry.Euclid.Ball9import Motions1011def unitBall : Set := { v ∈ ℝ³ | normSq(v) ≤ (1:R) }12def puncturedBall : Set := unitBall ∖ {zeroVector}1314theorem puncturedBall.graph15  shows puncturedBall = unitBall ∖ {zeroVector}16proof17  simp [puncturedBall]1819theorem unitBall.subset20  shows unitBall ⊆ ℝ³21proof22  intros v hv23  have parts := unitBall.membership.forward with hv24  exact parts.left2526theorem unitBall.function (v : Set)27  requires member : v ∈ unitBall28  shows v : 3 → ℝ29proof30  exact ℝ³.function with (unitBall.subset with v, member)3132theorem puncturedBall.membership (v : Set)33  shows v ∈ puncturedBall ↔ v ∈ unitBall ∧ v ≠ zeroVector34proof35  rw puncturedBall.graph36  constructor37  . intro hv38    obtain ⟨inBall, notZero⟩ := difference.membership.forward with hv39    refine ⟨inBall, ?_⟩40    intro equal41    apply notZero42    rw equal43    exact singleton.self44  . intro hv45    obtain ⟨inBall, notZero⟩ := hv46    apply difference.membership.backward47    refine ⟨inBall, ?_⟩48    intro inSingleton49    exact notZero with (singleton.membership.forward with inSingleton)5051theorem puncturedBall.subset52  shows puncturedBall ⊆ unitBall53proof54  rw puncturedBall.graph55  exact difference.subset_left at unitBall, {zeroVector}5657theorem puncturedBall.subset_space58  shows puncturedBall ⊆ ℝ³59proof60  exact Subset.transitive with puncturedBall.subset, unitBall.subset6162theorem zeroVector.in_ball63  shows zeroVector ∈ unitBall64proof65  have zeroIn : zeroVector ∈ ℝ³ := ℝ³.of_function with zeroVector.vector66  have bound : normSq(zeroVector) ≤ (1:R)67    rw zeroVector.normSq68    linarith69  exact unitBall.membership.backward with ⟨zeroIn, bound⟩7071-- The sphere lies in the punctured ball.72theorem sphere.subset_ball73  shows S² ⊆ unitBall74proof75  intros v hv76  obtain ⟨inSpace, unit⟩ := S².membership.forward with hv77  have bound : normSq(v) ≤ (1:R)78    rw unit79    linarith80  exact unitBall.membership.backward with ⟨inSpace, bound⟩8182theorem sphere.subset_punctured83  shows S² ⊆ puncturedBall84proof85  intros v hv86  obtain ⟨inSpace, unit⟩ := S².membership.forward with hv87  have inBall := sphere.subset_ball with v, hv88  have notZero : v ≠ zeroVector89    intro equal90    rw [equal, zeroVector.normSq] at unit91    linarith92  exact puncturedBall.membership.backward with ⟨inBall, notZero⟩9394-- A rotation preserves the ball and misses the origin only at the origin.95theorem unitBall.rotate (M : realRing ^ 3 × 3) (v : Set)96  requires hM : M ∈ so3Matrices97  requires hv : v ∈ unitBall98  shows M · v ∈ unitBall99proof100  obtain ⟨inSpace, bound⟩ := unitBall.membership.forward with hv101  have vector := ℝ³.function with inSpace102  have orthogonal := so3Matrices.orthogonal with hM103  have image := matrixVector.vector at M, v with *104  have imageIn := ℝ³.of_function with image105  have norm := Orthogonal.normSq with orthogonal, vector106  have imageBound : normSq(M · v) ≤ (1:R)107    rw norm108    exact bound109  exact unitBall.membership.backward with ⟨imageIn, imageBound⟩110111theorem matrixVector.eq_zero (M : realRing ^ 3 × 3) (v : Set)112  requires hM : M ∈ so3Matrices113  requires vector : v : 3 → ℝ114  requires zero : M · v = zeroVector115  shows v = zeroVector116proof117  have transposed := transpose.matrix at M with *118  have orthogonal := so3Matrices.orthogonal with hM119  have left := Orthogonal.left with orthogonal120  have composed := matrixVector.mul at transpose(M), M, v with vector121  have unit := matrixVector.one at v with vector122  have killed := matrixVector.zero_vector at transpose(M) with *123  rw [left, unit, zero, killed] at composed124  exact composed125126theorem puncturedBall.rotate (M : realRing ^ 3 × 3) (v : Set)127  requires hM : M ∈ so3Matrices128  requires hv : v ∈ puncturedBall129  shows M · v ∈ puncturedBall130proof131  obtain ⟨inBall, notZero⟩ := puncturedBall.membership.forward with hv132  have vector := unitBall.function with inBall133  have imageIn := unitBall.rotate with hM, inBall134  have imageNotZero : M · v ≠ zeroVector135    intro zero136    exact notZero with (matrixVector.eq_zero with hM, vector, zero)137  exact puncturedBall.membership.backward with ⟨imageIn, imageNotZero⟩138139theorem puncturedBall.invariant140  shows ∀ M ∈ Group.carrier(SO3), ∀ v ∈ puncturedBall, spaceAction(M,141      v) ∈ puncturedBall142proof143  intros M hM v hv144  rw SO3.carrierOf at hM145  have matrixM := so3Matrices.matrix with hM146  have inSpace := puncturedBall.subset_space with v, hv147  have value := spaceAction.apply with hM, inSpace148  rw value149  exact puncturedBall.rotate with hM, hv150