Grace/Cumulus/Geometry/Vectors3.g17

Open in Workbench Download source

Imports

Rotation.Generators

Declarations

Source

1-- The zero vector, negation, scaling, and cross product of ℝ³ as graphs on2-- 3, with Lagrange's identity and the linearity of the matrix action3-- 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.Vectors39import Rotation.Generators1011-- The zero vector.12defgraph zeroVector (i ∈ 3) : ℝ := (0:R)13proof14  typecheck1516instance zeroVector.vector17  shows zeroVector : 3 → ℝ18proof19  exact zeroVector.function2021theorem zeroVector.entry (i : Set)22  requires index : i ∈ 323  shows zeroVector(i) = (0:R)24proof25  exact zeroVector.value with index2627instance zeroVector.space28  shows zeroVector ∈ ℝ³29proof30  exact ℝ³.of_function with zeroVector.vector3132theorem zeroVector.normSq33  shows normSq(zeroVector) = (0:R)34proof35  have e0 := zeroVector.entry at 0 with index.zero_mem36  have e1 := zeroVector.entry at 1 with index.one_mem37  have e2 := zeroVector.entry at 2 with index.two_mem38  rw [normSq.value, e0, e1, e2]39  ring4041-- The negation of a vector.42defgraph vectorNeg (v : Set) (i ∈ 3) : ℝ := -(v(i):R)43requires vector : v : 3 → ℝ44proof45  have component := vector.component_real at v, i with vector, member46  typecheck4748instance vectorNeg.vector (v : Set)49  requires vector : v : 3 → ℝ50  shows vectorNeg(v) : 3 → ℝ51proof52  exact vectorNeg.function with vector5354theorem vectorNeg.entry (v i : Set)55  requires vector : v : 3 → ℝ56  requires index : i ∈ 357  shows vectorNeg(v)(i) = -(v(i):R)58proof59  exact vectorNeg.value with vector, index6061instance vectorNeg.space (v : Set)62  requires member : v ∈ ℝ³63  shows vectorNeg(v) ∈ ℝ³64proof65  have vector := ℝ³.function with member66  have image := vectorNeg.vector with vector67  exact ℝ³.of_function with image6869theorem vectorNeg.normSq (v : Set)70  requires vector : v : 3 → ℝ71  shows normSq(vectorNeg(v)) = normSq(v)72proof73  have v0 := vector.component_real at v, 0 with vector, index.zero_mem74  have v1 := vector.component_real at v, 1 with vector, index.one_mem75  have v2 := vector.component_real at v, 2 with vector, index.two_mem76  have e0 := vectorNeg.entry at v, 0 with vector, index.zero_mem77  have e1 := vectorNeg.entry at v, 1 with vector, index.one_mem78  have e2 := vectorNeg.entry at v, 2 with vector, index.two_mem79  rw [normSq.value, normSq.value, e0, e1, e2]80  ring8182theorem vectorNeg.sphere (v : Set)83  requires member : v ∈ S²84  shows vectorNeg(v) ∈ S²85proof86  obtain ⟨inSpace, unit⟩ := S².membership.forward with member87  have vector := ℝ³.function with inSpace88  have negIn := vectorNeg.space with inSpace89  have norm := vectorNeg.normSq with vector90  have negUnit : normSq(vectorNeg(v)) = (1:R)91    rw norm92    exact unit93  exact S².membership.backward with ⟨negIn, negUnit⟩9495theorem vectorNeg.involutive (v : Set)96  requires vector : v : 3 → ℝ97  shows vectorNeg(vectorNeg(v)) = v98proof99  have inner := vectorNeg.vector with vector100  have outer := vectorNeg.vector with inner101  apply FunctionBetween.ext with outer, vector102  intros i hi103  have component := vector.component_real at v, i with vector, hi104  have first := vectorNeg.entry at vectorNeg(v), i with inner, hi105  have second := vectorNeg.entry at v, i with vector, hi106  rw [first, second]107  ring108109-- Scaling a vector by a real.110defgraph vectorScale (c v : Set) (i ∈ 3) : ℝ := (c:R) * (v(i):R)111requires scalar : c ∈ ℝ112requires vector : v : 3 → ℝ113proof114  have component := vector.component_real at v, i with vector, member115  typecheck116117instance vectorScale.vector (c v : Set)118  requires scalar : c ∈ ℝ119  requires vector : v : 3 → ℝ120  shows vectorScale(c, v) : 3 → ℝ121proof122  exact vectorScale.function with scalar, vector123124theorem vectorScale.entry (c v i : Set)125  requires scalar : c ∈ ℝ126  requires vector : v : 3 → ℝ127  requires index : i ∈ 3128  shows vectorScale(c, v)(i) = (c:R) * (v(i):R)129proof130  exact vectorScale.value with scalar, vector, index131132instance vectorScale.space (c v : Set)133  requires scalar : c ∈ ℝ134  requires member : v ∈ ℝ³135  shows vectorScale(c, v) ∈ ℝ³136proof137  have vector := ℝ³.function with member138  have image := vectorScale.vector with scalar, vector139  exact ℝ³.of_function with image140141theorem vectorScale.normSq (c v : Set)142  requires scalar : c ∈ ℝ143  requires vector : v : 3 → ℝ144  shows normSq(vectorScale(c, v)) = (c:R) * (c:R) * normSq(v)145proof146  have v0 := vector.component_real at v, 0 with vector, index.zero_mem147  have v1 := vector.component_real at v, 1 with vector, index.one_mem148  have v2 := vector.component_real at v, 2 with vector, index.two_mem149  have e0 := vectorScale.entry at c, v, 0 with scalar, vector, index.zero_mem150  have e1 := vectorScale.entry at c, v, 1 with scalar, vector, index.one_mem151  have e2 := vectorScale.entry at c, v, 2 with scalar, vector, index.two_mem152  rw [normSq.value, normSq.value, e0, e1, e2]153  ring154155theorem vectorScale.one (v : Set)156  requires vector : v : 3 → ℝ157  shows vectorScale((1:R), v) = v158proof159  have oneReal : (1:R) ∈ ℝ by typecheck160  have scaled := vectorScale.vector with oneReal, vector161  apply FunctionBetween.ext with scaled, vector162  intros i hi163  have component := vector.component_real at v, i with vector, hi164  have entry := vectorScale.entry at (1:R), v, i with oneReal, vector, hi165  rw entry166  ring167168theorem vectorScale.neg_one (v : Set)169  requires vector : v : 3 → ℝ170  shows vectorScale(-(1:R), v) = vectorNeg(v)171proof172  have negReal : -(1:R) ∈ ℝ by typecheck173  have scaled := vectorScale.vector with negReal, vector174  have negated := vectorNeg.vector with vector175  apply FunctionBetween.ext with scaled, negated176  intros i hi177  have component := vector.component_real at v, i with vector, hi178  have entry := vectorScale.entry at -(1:R), v, i with negReal, vector, hi179  have negEntry := vectorNeg.entry at v, i with vector, hi180  rw [entry, negEntry]181  ring182183-- The matrix action is linear: it commutes with negation and scaling.184theorem matrixVector.neg (M : realRing ^ 3 × 3) (v : Set)185  requires vector : v : 3 → ℝ186  shows M · vectorNeg(v) = vectorNeg(M · v)187proof188  have negated := vectorNeg.vector with vector189  have left := matrixVector.vector at M, vectorNeg(v) with *190  have image := matrixVector.vector at M, v with *191  have right := vectorNeg.vector with image192  apply FunctionBetween.ext with left, right193  intros i hi194  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi195  have v0 := vector.component_real at v, 0 with vector, index.zero_mem196  have v1 := vector.component_real at v, 1 with vector, index.one_mem197  have v2 := vector.component_real at v, 2 with vector, index.two_mem198  have leftEntry := matrixVector.entry at M, vectorNeg(v), i with *199  have rightEntry := vectorNeg.entry at M · v, i with image, hi200  have inner := matrixVector.entry at M, v, i with *201  have e0 := vectorNeg.entry at v, 0 with vector, index.zero_mem202  have e1 := vectorNeg.entry at v, 1 with vector, index.one_mem203  have e2 := vectorNeg.entry at v, 2 with vector, index.two_mem204  rw [leftEntry, rightEntry, inner, e0, e1, e2]205  ring206207theorem matrixVector.scale (M : realRing ^ 3 × 3) (c v : Set)208  requires scalar : c ∈ ℝ209  requires vector : v : 3 → ℝ210  shows M · vectorScale(c, v) = vectorScale(c, M · v)211proof212  have scaled := vectorScale.vector with scalar, vector213  have left := matrixVector.vector at M, vectorScale(c, v) with *214  have image := matrixVector.vector at M, v with *215  have right := vectorScale.vector with scalar, image216  apply FunctionBetween.ext with left, right217  intros i hi218  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi219  have v0 := vector.component_real at v, 0 with vector, index.zero_mem220  have v1 := vector.component_real at v, 1 with vector, index.one_mem221  have v2 := vector.component_real at v, 2 with vector, index.two_mem222  have leftEntry := matrixVector.entry at M, vectorScale(c, v), i with *223  have rightEntry := vectorScale.entry at c, M · v, i with scalar, image, hi224  have inner := matrixVector.entry at M, v, i with *225  have e0 := vectorScale.entry at c, v, 0 with scalar, vector, index.zero_mem226  have e1 := vectorScale.entry at c, v, 1 with scalar, vector, index.one_mem227  have e2 := vectorScale.entry at c, v, 2 with scalar, vector, index.two_mem228  rw [leftEntry, rightEntry, inner, e0, e1, e2]229  ring230231-- The cross product u × v, by its three coordinates.232defgraph cross (u v : Set) (i ∈ 3) : ℝ :=233  pick3((u(1):R) * (v(2):R) - (u(2):R) * (v(1):R),234    (u(2):R) * (v(0):R) - (u(0):R) * (v(2):R),235    (u(0):R) * (v(1):R) - (u(1):R) * (v(0):R), i)236requires vectorU : u : 3 → ℝ237requires vectorV : v : 3 → ℝ238proof239  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem240  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem241  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem242  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem243  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem244  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem245  have first : (u(1):R) * (v(2):R) - (u(2):R) * (v(1):R) ∈ ℝ by typecheck246  have second : (u(2):R) * (v(0):R) - (u(0):R) * (v(2):R) ∈ ℝ by typecheck247  have third : (u(0):R) * (v(1):R) - (u(1):R) * (v(0):R) ∈ ℝ by typecheck248  exact pick3.real with first, second, third, member249250instance cross.vector (u v : Set)251  requires vectorU : u : 3 → ℝ252  requires vectorV : v : 3 → ℝ253  shows cross(u, v) : 3 → ℝ254proof255  exact cross.function with vectorU, vectorV256257theorem cross.zero (u v : Set)258  requires vectorU : u : 3 → ℝ259  requires vectorV : v : 3 → ℝ260  shows cross(u, v)(0) = (u(1):R) * (v(2):R) - (u(2):R) * (v(1):R)261proof262  have value := cross.value at u, v, 0 with vectorU, vectorV, index.zero_mem263  rw [value, pick3.zero]264  rfl265266theorem cross.one (u v : Set)267  requires vectorU : u : 3 → ℝ268  requires vectorV : v : 3 → ℝ269  shows cross(u, v)(1) = (u(2):R) * (v(0):R) - (u(0):R) * (v(2):R)270proof271  have value := cross.value at u, v, 1 with vectorU, vectorV, index.one_mem272  rw [value, pick3.one]273  rfl274275theorem cross.two (u v : Set)276  requires vectorU : u : 3 → ℝ277  requires vectorV : v : 3 → ℝ278  shows cross(u, v)(2) = (u(0):R) * (v(1):R) - (u(1):R) * (v(0):R)279proof280  have value := cross.value at u, v, 2 with vectorU, vectorV, index.two_mem281  rw [value, pick3.two]282  rfl283284instance cross.space (u v : Set)285  requires memberU : u ∈ ℝ³286  requires memberV : v ∈ ℝ³287  shows cross(u, v) ∈ ℝ³288proof289  have vectorU := ℝ³.function with memberU290  have vectorV := ℝ³.function with memberV291  have image := cross.vector with vectorU, vectorV292  exact ℝ³.of_function with image293294-- The cross product is orthogonal to both factors, and Lagrange's295-- identity gives its squared norm.296theorem cross.dot_left (u v : Set)297  requires vectorU : u : 3 → ℝ298  requires vectorV : v : 3 → ℝ299  shows dot3(u, cross(u, v)) = (0:R)300proof301  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem302  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem303  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem304  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem305  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem306  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem307  have c0 := cross.zero with vectorU, vectorV308  have c1 := cross.one with vectorU, vectorV309  have c2 := cross.two with vectorU, vectorV310  rw [dot3.value, c0, c1, c2]311  ring312313theorem cross.dot_right (u v : Set)314  requires vectorU : u : 3 → ℝ315  requires vectorV : v : 3 → ℝ316  shows dot3(v, cross(u, v)) = (0:R)317proof318  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem319  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem320  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem321  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem322  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem323  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem324  have c0 := cross.zero with vectorU, vectorV325  have c1 := cross.one with vectorU, vectorV326  have c2 := cross.two with vectorU, vectorV327  rw [dot3.value, c0, c1, c2]328  ring329330theorem cross.normSq (u v : Set)331  requires vectorU : u : 3 → ℝ332  requires vectorV : v : 3 → ℝ333  shows normSq(cross(u, v)) = normSq(u) * normSq(v) - dot3(u, v) * dot3(u, v)334proof335  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem336  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem337  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem338  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem339  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem340  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem341  have c0 := cross.zero with vectorU, vectorV342  have c1 := cross.one with vectorU, vectorV343  have c2 := cross.two with vectorU, vectorV344  rw [normSq.value, normSq.value, normSq.value, dot3.value, c0, c1, c2]345  ring346