Grace/Cumulus/Rotation/Vectors.g17

Open in Workbench Download source

Imports

Real.Field · Real.Natural · Algebra.Ring.MatrixEntries

Declarations

Source

1-- Vectors of ℝ³: functions v : 3 → ℝ, the dot product and the squared2-- norm, the unit sphere S², entries of 3 × 3 real matrices as sums of3-- three terms, and the action M · v of a matrix on a vector4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Rotation.Vectors10import Real.Field11import Real.Natural12import Algebra.Ring.MatrixEntries1314-- The three indices of a vector or a row.15instance index.zero_mem16  shows 0 ∈ 317proof18  typecheck1920instance index.one_mem21  shows 1 ∈ 322proof23  typecheck2425instance index.two_mem26  shows 2 ∈ 327proof28  typecheck2930theorem index.zero_ne_one31  shows 0 ≠ 132proof33  intro equal34  arith3536theorem index.zero_ne_two37  shows 0 ≠ 238proof39  intro equal40  arith4142theorem index.one_ne_two43  shows 1 ≠ 244proof45  intro equal46  arith4748theorem index.one_ne_zero49  shows 1 ≠ 050proof51  intro equal52  arith5354theorem index.two_ne_zero55  shows 2 ≠ 056proof57  intro equal58  arith5960theorem index.two_ne_one61  shows 2 ≠ 162proof63  intro equal64  arith6566theorem index.cases (i : Set)67  requires member : i ∈ 368  shows i = 0 ∨ i = 1 ∨ i = 269proof70  have natural := natural.member_natural at 3 with i, member71  have below := Less.of_membership at i, 3 with member72  have le2 : i ≤ 2 by arith73  have split := LessEqual.cases at i, 2 with le274  cases split with lt2 | eq275  . have le1 : i ≤ 1 by arith76    have split1 := LessEqual.cases at i, 1 with le177    cases split1 with lt1 | eq178    . left79      have le0 : i ≤ 0 by arith80      exact LessEqual.eq_zero with le081    . right82      left83      exact eq184  . right85    right86    exact eq28788-- ℝ³ is the set of functions 3 → ℝ.89def ℝ³ : Set := functionSpace(3, ℝ)9091theorem ℝ³.membership (v : Set)92  shows v ∈ ℝ³ ↔ v : 3 → ℝ93proof94  simp [ℝ³, functionSpace.mem_iff]9596theorem ℝ³.function (v : Set)97  requires member : v ∈ ℝ³98  shows v : 3 → ℝ99proof100  exact ℝ³.membership.forward with member101102instance ℝ³.of_function (v : Set)103  requires vector : v : 3 → ℝ104  shows v ∈ ℝ³105proof106  exact ℝ³.membership.backward with vector107108instance vector.component_real (v i : Set)109  requires vector : v : 3 → ℝ110  requires index : i ∈ 3111  shows v(i) ∈ ℝ112proof113  exact FunctionBetween.apply_closed with vector, index114115-- The dot product and the squared norm.116def dot3 (u v : Set) : Set :=117  (u(0):R) * (v(0):R) + (u(1):R) * (v(1):R) + (u(2):R) * (v(2):R)118119def normSq (v : Set) : Set := dot3(v, v)120121theorem dot3.value (u v : Set)122  shows dot3(u, v) = (u(0):R) * (v(0):R) + (u(1):R) * (v(1):R) + (u(2):R) * (v(2):R)123proof124  simp [dot3]125126theorem normSq.value (v : Set)127  shows normSq(v) = (v(0):R) * (v(0):R) + (v(1):R) * (v(1):R) + (v(2):R) * (v(2):R)128proof129  simp [normSq, dot3]130131instance dot3.real (u v : Set)132  requires vectorU : u : 3 → ℝ133  requires vectorV : v : 3 → ℝ134  shows dot3(u, v) ∈ ℝ135proof136  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem137  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem138  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem139  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem140  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem141  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem142  rw dot3.value143  typecheck144145instance normSq.real (v : Set)146  requires vector : v : 3 → ℝ147  shows normSq(v) ∈ ℝ148proof149  unfold normSq150  exact dot3.real with vector, vector151152theorem dot3.symmetric (u v : Set)153  requires vectorU : u : 3 → ℝ154  requires vectorV : v : 3 → ℝ155  shows dot3(u, v) = dot3(v, u)156proof157  have u0 := vector.component_real at u, 0 with vectorU, index.zero_mem158  have u1 := vector.component_real at u, 1 with vectorU, index.one_mem159  have u2 := vector.component_real at u, 2 with vectorU, index.two_mem160  have v0 := vector.component_real at v, 0 with vectorV, index.zero_mem161  have v1 := vector.component_real at v, 1 with vectorV, index.one_mem162  have v2 := vector.component_real at v, 2 with vectorV, index.two_mem163  rw [dot3.value, dot3.value]164  ring165166-- The unit sphere.167def S² : Set := { v ∈ ℝ³ | normSq(v) = (1:R) }168169theorem S².subset170  shows S² ⊆ ℝ³171proof172  intros v hv173  have parts := S².membership.forward with hv174  exact parts.left175176theorem S².function (v : Set)177  requires member : v ∈ S²178  shows v : 3 → ℝ179proof180  have parts := S².membership.forward with member181  exact ℝ³.function with parts.left182183-- Entries of a 3 × 3 real matrix are real.184instance Matrix.real_entry (M : realRing ^ 3 × 3) (i j : Set)185  requires row : i ∈ 3186  requires column : j ∈ 3187  shows M[i, j] ∈ ℝ188proof189  have entry := Matrix.entry at M, realRing, 3, i, j with *190  rw realRing.carrierOf at entry191  exact entry192193theorem Matrix.row_real (M : realRing ^ 3 × 3) (i : Set)194  requires row : i ∈ 3195  shows M[i, 0] ∈ ℝ ∧ M[i, 1] ∈ ℝ ∧ M[i, 2] ∈ ℝ196proof197  have e0 := Matrix.real_entry at M, i, 0 with *198  have e1 := Matrix.real_entry at M, i, 1 with *199  have e2 := Matrix.real_entry at M, i, 2 with *200  exact ⟨e0, e1, e2⟩201202-- The operations of realRing are the real operations.203theorem realRing.add_value (x y : Set)204  shows call2(Ring.add(realRing), x, y) = (x:R) + (y:R)205proof206  simp [realRing, Ring.mk.add]207208theorem realRing.mul_value (x y : Set)209  shows call2(Ring.mul(realRing), x, y) = (x:R) * (y:R)210proof211  simp [realRing, Ring.mk.mul]212213theorem realRing.zero_value214  shows Ring.zero(realRing) = (0:R)215proof216  simp [realRing, Ring.mk.zero]217218theorem realRing.one_value219  shows Ring.one(realRing) = (1:R)220proof221  simp [realRing, Ring.mk.one]222223-- A finite sum over the index set 3 is the sum of its three terms.224theorem finiteRingSum.three (A add zero neg mul one w : Set)225  requires ring : IsCommRing(A, add, zero, neg, mul, one)226  requires weights : w : 3 → A227  shows finiteRingSum(3, A, add, zero, neg, mul, one, w) =228    call2(add, call2(add, w(0), w(1)), w(2))229proof230  have three : 3 = insert(2, 2) := natural.successor_as_insert at 2 with *231  have two : 2 = insert(1, 1) := natural.successor_as_insert at 1 with *232  have one : 1 = insert(0, 0) := natural.successor_as_insert at 0 with *233  have finite2 := Finite.natural at 2234  have finite1 := Finite.natural at 1235  have finite0 := Finite.natural at 0236  have fresh2 := membership.irreflexive at 2237  have fresh1 := membership.irreflexive at 1238  have fresh0 := membership.irreflexive at 0239  have sub2 : 2 ⊆ 3240    intros x hx241    exact membership.into_successor at x, 2 with hx242  have sub1 : 1 ⊆ 2243    intros x hx244    exact membership.into_successor at x, 1 with hx245  have closed2 : ∀ x ∈ 2, w(x) ∈ A246    intros x hx247    exact FunctionBetween.apply_closed with weights, (sub2 with x, hx)248  have weights2 := restrict.function at w, 3, A, 2, A with *249  have closed1 : ∀ x ∈ 1, restrict(w, 2)(x) ∈ A250    intros x hx251    exact FunctionBetween.apply_closed with weights2, (sub1 with x, hx)252  have weights1 := restrict.function at restrict(w, 2), 2, A, 1, A with *253  have closed0 : ∀ x ∈ 0, restrict(restrict(w, 2), 1)(x) ∈ A254    intros x hx255    exfalso256    settle with nat.zero, set.empty257  have sub0 : 0 ⊆ 1258    intros x hx259    exact membership.into_successor at x, 0 with hx260  have weights0 := restrict.function at restrict(restrict(w, 2), 1), 1, A, 0, A with *261  have weights3i : w : insert(2, 2) → A262    rw ← three263    exact weights264  have step3 := finiteRingSum.insert at 2, A, add, zero, neg, mul, one, w, 2265    with ring, finite2, weights3i, fresh2266  rw ← three at step3267  have weights2i : restrict(w, 2) : insert(1, 1) → A268    rw ← two269    exact weights2270  have step2 := finiteRingSum.insert at 1, A, add, zero, neg, mul, one, restrict(w, 2), 1271    with ring, finite1, weights2i, fresh1272  rw ← two at step2273  have weights1i : restrict(restrict(w, 2), 1) : insert(0, 0) → A274    rw ← one275    exact weights1276  have step1 := finiteRingSum.insert at 0, A, add, zero, neg, mul, one,277    restrict(restrict(w, 2), 1), 0 with ring, finite0, weights1i, fresh0278  rw ← one at step1279  have value1 := restrict.apply at w, 3, A, 2, A, 1 with *280  have value0 := restrict.apply at w, 3, A, 2, A, 0 with *281  have value00 := restrict.apply at restrict(w, 2), 2, A, 1, A, 0 with *282  have weightsE : restrict(restrict(restrict(w, 2), 1), 0) : ∅ → A283    rw ← nat.zero284    exact weights0285  have step0 := finiteRingSum.empty at A, add, zero, neg, mul, one,286    restrict(restrict(restrict(w, 2), 1), 0) with ring, weightsE287  rw ← nat.zero at step0288  have w0 := FunctionBetween.apply_closed at w, 3, A, 0 with *289  have ordinary := IsCommRing.ring with ring290  have identity := IsRing.add_left_identity at A, add, zero, neg, mul, one, w(0)291    with ordinary, w0292  rw [step3, step2, step1, step0, value1, value00, value0, identity]293  rfl294295-- An entry of a product of 3 × 3 real matrices is the sum of three terms.296theorem matrixRing.mul_entry_three (M N : realRing ^ 3 × 3) (i j : Set)297  requires row : i ∈ 3298  requires column : j ∈ 3299  shows (M * N)[i, j] =300    (M[i, 0]:R) * (N[0, j]:R) + (M[i, 1]:R) * (N[1, j]:R) + (M[i, 2]:R) * (N[2, j]:R)301proof302  have comm := realRing.comm_ring303  have parts := CommRing.parts with comm304  have entry := matrixRing.mul_entry at realRing, 3, M, N, i, j with *305  have squareM := Matrix.square at M, realRing, 3 with *306  have squareN := Matrix.square at N, realRing, 3 with *307  have shapeM := squareMatrices.membership.forward with squareM308  have shapeN := squareMatrices.membership.forward with squareN309  have weights := matrixProductWeights.function at 3, Ring.carrier(realRing),310    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing),311    Ring.one(realRing), M, N, i, j with *312  have three := finiteRingSum.three at Ring.carrier(realRing), Ring.add(realRing),313    Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing), Ring.one(realRing),314    matrixProductWeights(3, Ring.carrier(realRing), Ring.add(realRing),315      Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing), Ring.one(realRing),316      M, N, i, j) with parts, weights317  have w0 := matrixProductWeights.value at 3, Ring.carrier(realRing),318    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing),319    Ring.one(realRing), M, N, i, j, 0 with *320  have w1 := matrixProductWeights.value at 3, Ring.carrier(realRing),321    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing),322    Ring.one(realRing), M, N, i, j, 1 with *323  have w2 := matrixProductWeights.value at 3, Ring.carrier(realRing),324    Ring.add(realRing), Ring.zero(realRing), Ring.neg(realRing), Ring.mul(realRing),325    Ring.one(realRing), M, N, i, j, 2 with *326  rw entry327  unfold matrixProductEntry328  simp [realRing.mul_value, realRing.add_value]329330-- The action of a 3 × 3 real matrix on a vector, M · v.331defgraph matrixVector (M v : Set) (i ∈ 3) : ℝ :=332  (M[i, 0]:R) * (v(0):R) + (M[i, 1]:R) * (v(1):R) + (M[i, 2]:R) * (v(2):R)333requires matrix : M : realRing ^ 3 × 3334requires vector : v : 3 → ℝ335proof336  have m0 := Matrix.real_entry at M, i, 0 with matrix, member, index.zero_mem337  have m1 := Matrix.real_entry at M, i, 1 with matrix, member, index.one_mem338  have m2 := Matrix.real_entry at M, i, 2 with matrix, member, index.two_mem339  have v0 := vector.component_real at v, 0 with vector, index.zero_mem340  have v1 := vector.component_real at v, 1 with vector, index.one_mem341  have v2 := vector.component_real at v, 2 with vector, index.two_mem342  typecheck343344notation infixl 72 "·" => matrixVector345346theorem matrixVector.entry (M v i : Set)347  requires matrix : M : realRing ^ 3 × 3348  requires vector : v : 3 → ℝ349  requires index : i ∈ 3350  shows (M · v)(i) = (M[i, 0]:R) * (v(0):R) + (M[i, 1]:R) * (v(1):R) + (M[i, 2]:R) * (v(2):R)351proof352  exact matrixVector.value with *353354instance matrixVector.vector (M v : Set)355  requires matrix : M : realRing ^ 3 × 3356  requires vector : v : 3 → ℝ357  shows M · v : 3 → ℝ358proof359  exact matrixVector.function with *360361-- The ring of 3 × 3 real matrices, as a closed instance, so that its362-- numerals matrixRing(realRing, 3)[0] and matrixRing(realRing, 3)[1] read.363instance matrixRing.real_ring364  shows Ring(matrixRing(realRing, 3))365proof366  have comm := realRing.comm_ring367  exact matrixRing.ring at realRing, 3 with comm368369-- Products of matrices are square matrices, and the identity is one.370instance Matrix.mul_matrix (M N : realRing ^ 3 × 3)371  shows M * N : realRing ^ 3 × 3372proof373  have comm := realRing.comm_ring374  have ring := matrixRing.real_ring375  have memberM := Matrix.mem_ring at M, realRing, 3 with assumption376  have memberN := Matrix.mem_ring at N, realRing, 3 with assumption377  have product := Ring.mul_mem at matrixRing(realRing, 3), M, N with *378  exact Matrix.of_mem with product379380instance Matrix.one_matrix381  shows matrixRing(realRing, 3)[1] : realRing ^ 3 × 3382proof383  have comm := realRing.comm_ring384  have ring := matrixRing.real_ring385  have unit := Ring.one_mem at matrixRing(realRing, 3) with ring386  apply Matrix.of_mem387  exact unit388389-- The identity matrix acts trivially and a product acts by composition.390theorem matrixVector.one (v : Set)391  requires vector : v : 3 → ℝ392  shows matrixRing(realRing, 3)[1] · v = v393proof394  have comm := realRing.comm_ring395  have one := Matrix.one_matrix396  have zeroIn : Ring.zero(realRing) ∈ Ring.carrier(realRing) := Ring.zero_mem with *397  have oneIn : Ring.one(realRing) ∈ Ring.carrier(realRing) := Ring.one_mem with *398  have image := matrixVector.vector at matrixRing(realRing, 3)[1], v with *399  have v0 := vector.component_real at v, 0 with vector, index.zero_mem400  have v1 := vector.component_real at v, 1 with vector, index.one_mem401  have v2 := vector.component_real at v, 2 with vector, index.two_mem402  apply FunctionBetween.ext with image, vector403  intros i hi404  have entry := matrixVector.entry at matrixRing(realRing, 3)[1], v, i with one, vector, hi405  rw entry406  have e0 := matrixRing.one_entry at realRing, 3, i, 0 with *407  have e1 := matrixRing.one_entry at realRing, 3, i, 1 with *408  have e2 := matrixRing.one_entry at realRing, 3, i, 2 with *409  rw [e0, e1, e2]410  have alternatives := index.cases with hi411  rcases alternatives with at0 | at1 | at2412  . rw at0413    have s0 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),414      Ring.one(realRing), 0, 0 with *415    have s1 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),416      Ring.one(realRing), 1, 0 with zeroIn, oneIn, index.zero_ne_one417    have s2 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),418      Ring.one(realRing), 2, 0 with zeroIn, oneIn, index.zero_ne_two419    rw [s0, s1, s2, realRing.zero_value, realRing.one_value]420    ring421  . rw at1422    have same1 : 1 = 1 by rfl423    have s0 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),424      Ring.one(realRing), 0, 1 with zeroIn, oneIn, index.one_ne_zero425    have s1 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),426      Ring.one(realRing), 1, 1 with zeroIn, oneIn, same1427    have s2 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),428      Ring.one(realRing), 2, 1 with zeroIn, oneIn, index.one_ne_two429    rw [s0, s1, s2, realRing.zero_value, realRing.one_value]430    ring431  . rw at2432    have same2 : 2 = 2 by rfl433    have s0 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),434      Ring.one(realRing), 0, 2 with zeroIn, oneIn, index.two_ne_zero435    have s1 := singleValue.other at Ring.carrier(realRing), Ring.zero(realRing),436      Ring.one(realRing), 1, 2 with zeroIn, oneIn, index.two_ne_one437    have s2 := singleValue.same at Ring.carrier(realRing), Ring.zero(realRing),438      Ring.one(realRing), 2, 2 with zeroIn, oneIn, same2439    rw [s0, s1, s2, realRing.zero_value, realRing.one_value]440    ring441442theorem matrixVector.mul (M N : realRing ^ 3 × 3) (v : Set)443  requires vector : v : 3 → ℝ444  shows (M * N) · v = M · (N · v)445proof446  have product := Matrix.mul_matrix at M, N with *447  have inner := matrixVector.vector at N, v with *448  have left := matrixVector.vector at M * N, v with *449  have right := matrixVector.vector at M, N · v with *450  apply FunctionBetween.ext with left, right451  intros i hi452  have leftEntry := matrixVector.entry at M * N, v, i with *453  have rightEntry := matrixVector.entry at M, N · v, i with *454  have c0 := matrixRing.mul_entry_three at M, N, i, 0 with *455  have c1 := matrixRing.mul_entry_three at M, N, i, 1 with *456  have c2 := matrixRing.mul_entry_three at M, N, i, 2 with *457  have n0 := matrixVector.entry at N, v, 0 with *458  have n1 := matrixVector.entry at N, v, 1 with *459  have n2 := matrixVector.entry at N, v, 2 with *460  obtain ⟨m0, m1, m2⟩ := Matrix.row_real at M, i with hi461  obtain ⟨n00, n01, n02⟩ := Matrix.row_real at N, 0 with index.zero_mem462  obtain ⟨n10, n11, n12⟩ := Matrix.row_real at N, 1 with index.one_mem463  obtain ⟨n20, n21, n22⟩ := Matrix.row_real at N, 2 with index.two_mem464  have v0 := vector.component_real at v, 0 with vector, index.zero_mem465  have v1 := vector.component_real at v, 1 with vector, index.one_mem466  have v2 := vector.component_real at v, 2 with vector, index.two_mem467  rw [leftEntry, rightEntry, c0, c1, c2, n0, n1, n2]468  ring469