Grace/Cumulus/LinearAlgebra/FiniteDimensional.g17

Open in Workbench Download source

Imports

Real.FiniteSum · Real.Squares

Declarations

Source

1-- Finite dimensional real linear algebra2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.LinearAlgebra.FiniteDimensional8import Real.FiniteSum9import Real.Squares1011-- Vectors are real sequences observed only below the dimension n. This12-- representation permits the same sequence to be reused at several sizes.13def dotProduct (u v : RealSequence, n : Nat) : Real :=14  realPartialSum(mulSequence(u, v), n)1516theorem dotProduct.real (u v : Set, n : Nat)17  requires sequenceU : RealSequence(u)18  requires sequenceV : RealSequence(v)19  shows Real(dotProduct(u, v, n))20proof21  have product := mulSequence.sequence with sequenceU, sequenceV22  unfold dotProduct23  exact realPartialSum.real with product2425theorem dotProduct.zero (u v : Set)26  shows dotProduct(u, v, 0) = (0:R)27proof28  unfold dotProduct29  exact realPartialSum.zero3031theorem dotProduct.succ (u v : Set, n : Nat)32  requires sequenceU : RealSequence(u)33  requires sequenceV : RealSequence(v)34  shows dotProduct(u, v, succ(n)) =35    (dotProduct(u, v, n):R) + (u[n]:R) * (v[n]:R)36proof37  have un := RealSequence.value with sequenceU38  have vn := RealSequence.value with sequenceV39  have value := mulSequence.value with sequenceU, sequenceV, un, vn40  unfold dotProduct41  rw [realPartialSum.succ, value]42  unfold realAddValue43  unfold call244  rfl4546theorem dotProduct.symmetric (u v : Set, n : Nat)47  requires sequenceU : RealSequence(u)48  requires sequenceV : RealSequence(v)49  shows dotProduct(u, v, n) = dotProduct(v, u, n)50proof51  induction n52  | zero =>53    rw [dotProduct.zero, dotProduct.zero]54    rfl55  | succ(k) using ih =>56    have uk := RealSequence.value with sequenceU57    have vk := RealSequence.value with sequenceV58    rw [dotProduct.succ, dotProduct.succ, ih]59    ring6061-- Only the first n coordinates are observed by an n-dimensional dot product.62theorem dotProduct.eq_prefix (u v w z : Set, n : Nat)63  requires sequenceU : RealSequence(u)64  requires sequenceV : RealSequence(v)65  requires sequenceW : RealSequence(w)66  requires sequenceZ : RealSequence(z)67  requires equalLeft : ∀ k ∈ ℕ, k < n → u[k] = w[k]68  requires equalRight : ∀ k ∈ ℕ, k < n → v[k] = z[k]69  shows dotProduct(u, v, n) = dotProduct(w, z, n)70proof71  have first := mulSequence.sequence with sequenceU, sequenceV72  have second := mulSequence.sequence with sequenceW, sequenceZ73  have equal : ∀ k ∈ ℕ, k < n →74      mulSequence(u, v)[k] = mulSequence(w, z)[k]75    intros k naturalK before76    have typedK := nat.omega.backward with naturalK77    have uk := RealSequence.value at u, k with sequenceU78    have vk := RealSequence.value at v, k with sequenceV79    have wk := RealSequence.value at w, k with sequenceW80    have zk := RealSequence.value at z, k with sequenceZ81    have firstValue := mulSequence.value with sequenceU, sequenceV, uk, vk82    have secondValue := mulSequence.value with sequenceW, sequenceZ, wk, zk83    have left := equalLeft with k, naturalK, before84    have right := equalRight with k, naturalK, before85    rw [firstValue, secondValue, left, right]86    rfl87  unfold dotProduct88  exact realPartialSum.eq_prefix with first, second, equal8990theorem dotProduct.add_right (u v w : Set, n : Nat)91  requires sequenceU : RealSequence(u)92  requires sequenceV : RealSequence(v)93  requires sequenceW : RealSequence(w)94  shows dotProduct(u, addSequence(v, w), n) =95    (dotProduct(u, v, n):R) + (dotProduct(u, w, n):R)96proof97  induction n98  | zero =>99    rw [dotProduct.zero, dotProduct.zero, dotProduct.zero]100    ring101  | succ(k) using ih =>102    have combined := addSequence.sequence with sequenceV, sequenceW103    have uk := RealSequence.value with sequenceU104    have vk := RealSequence.value with sequenceV105    have wk := RealSequence.value with sequenceW106    have vkPlusWk := RealSequence.value with combined107    have value := addSequence.value with sequenceV, sequenceW, vk, wk108    rw [dotProduct.succ, dotProduct.succ, dotProduct.succ, ih, value]109    ring110111theorem dotProduct.add_left (u v w : Set, n : Nat)112  requires sequenceU : RealSequence(u)113  requires sequenceV : RealSequence(v)114  requires sequenceW : RealSequence(w)115  shows dotProduct(addSequence(u, v), w, n) =116    (dotProduct(u, w, n):R) + (dotProduct(v, w, n):R)117proof118  have combined := addSequence.sequence with sequenceU, sequenceV119  have symmetryCombined := dotProduct.symmetric with combined, sequenceW120  have distributive := dotProduct.add_right with sequenceW, sequenceU, sequenceV121  have symmetryU := dotProduct.symmetric with sequenceW, sequenceU122  have symmetryV := dotProduct.symmetric with sequenceW, sequenceV123  rw [symmetryCombined, distributive, symmetryU, symmetryV]124  rfl125126theorem dotProduct.scale_right (u v : Set, C : Real, n : Nat)127  requires sequenceU : RealSequence(u)128  requires sequenceV : RealSequence(v)129  shows dotProduct(u, mulSequence(constantSequence(C), v), n) =130    C * (dotProduct(u, v, n):R)131proof132  induction n133  | zero =>134    rw [dotProduct.zero, dotProduct.zero]135    ring136  | succ(k) using ih =>137    have constants := constantSequence.sequence at C138    have scaled := mulSequence.sequence with constants, sequenceV139    have uk := RealSequence.value with sequenceU140    have vk := RealSequence.value with sequenceV141    have constantK := RealSequence.value with constants142    have scaledK := RealSequence.value with scaled143    have value := mulSequence.value with constants, sequenceV, constantK, vk144    have constant := constantSequence.value at C, k with *145    rw [dotProduct.succ, dotProduct.succ, ih, value, constant]146    ring147148theorem dotProduct.scale_left (u v : Set, C : Real, n : Nat)149  requires sequenceU : RealSequence(u)150  requires sequenceV : RealSequence(v)151  shows dotProduct(mulSequence(constantSequence(C), u), v, n) =152    C * (dotProduct(u, v, n):R)153proof154  have constants := constantSequence.sequence at C155  have scaled := mulSequence.sequence with constants, sequenceU156  have symmetricScaled := dotProduct.symmetric with scaled, sequenceV157  have right := dotProduct.scale_right with sequenceV, sequenceU158  have symmetric := dotProduct.symmetric with sequenceV, sequenceU159  rw [symmetricScaled, right, symmetric]160  rfl161162theorem dotProduct.sub_left (u v w : Set, n : Nat)163  requires sequenceU : RealSequence(u)164  requires sequenceV : RealSequence(v)165  requires sequenceW : RealSequence(w)166  shows dotProduct(subSequence(u, v), w, n) =167    (dotProduct(u, w, n):R) - (dotProduct(v, w, n):R)168proof169  induction n170  | zero =>171    simp [dotProduct.zero]172    ring173  | succ(k) using ih =>174    have difference := subSequence.sequence at u, v with *175    have uk := RealSequence.value at u, k with *176    have vk := RealSequence.value at v, k with *177    have wk := RealSequence.value at w, k with *178    have dk := RealSequence.value at subSequence(u, v), k with *179    simp [dotProduct.succ, subSequence.value]180    ring181182def squaredNorm (u : RealSequence, n : Nat) : Real := dotProduct(u, u, n)183184predicate Orthogonal (u v : Set, n : Nat) := dotProduct(u, v, n) = (0:R)185186theorem Orthogonal.symmetric (u v : Set, n : Nat)187  requires sequenceU : RealSequence(u)188  requires sequenceV : RealSequence(v)189  requires orthogonal : Orthogonal(u, v, n)190  shows Orthogonal(v, u, n)191proof192  unfold Orthogonal at orthogonal193  unfold Orthogonal194  have symmetry := dotProduct.symmetric with sequenceU, sequenceV195  rwa symmetry at orthogonal196197theorem squaredNorm.real (u : Set, n : Nat)198  requires sequence : RealSequence(u)199  shows Real(squaredNorm(u, n))200proof201  unfold squaredNorm202  exact dotProduct.real with sequence, sequence203204theorem squaredNorm.succ (u : Set, n : Nat)205  requires sequence : RealSequence(u)206  shows squaredNorm(u, succ(n)) =207    (squaredNorm(u, n):R) + (u[n]:R) * (u[n]:R)208proof209  unfold squaredNorm210  exact dotProduct.succ with sequence, sequence211212theorem squaredNorm.nonnegative (u : Set, n : Nat)213  requires sequence : RealSequence(u)214  shows (0:R) ≤ (squaredNorm(u, n):R)215proof216  induction n217  | zero =>218    unfold squaredNorm219    rw dotProduct.zero220    exact realLe.reflexive with realZero.real221  | succ(k) using ih =>222    have uk := RealSequence.value with sequence223    have prefix := squaredNorm.real with sequence224    have term := realMulValue.real with uk, uk225    have nonnegative := realMulValue.square_nonnegative with uk226    have added := realLe.add with realZero.real, prefix, realZero.real, term, ih, nonnegative227    have zero := realAddValue.zero_right with realZero.real228    rw zero at added229    unfold squaredNorm at added230    unfold squaredNorm231    rwa dotProduct.succ232233theorem squaredNorm.scale (u : Set, C : Real, n : Nat)234  requires sequence : RealSequence(u)235  shows squaredNorm(mulSequence(constantSequence(C), u), n) =236    (C * C) * (squaredNorm(u, n):R)237proof238  have constants := constantSequence.sequence at C239  have scaled := mulSequence.sequence with constants, sequence240  have first := dotProduct.scale_left with sequence, scaled241  have second := dotProduct.scale_right with sequence, sequence242  simp [squaredNorm]243  ring244245theorem squaredNorm.add (u v : Set, n : Nat)246  requires sequenceU : RealSequence(u)247  requires sequenceV : RealSequence(v)248  shows squaredNorm(addSequence(u, v), n) =249    (squaredNorm(u, n):R) +250      (2:R) * (dotProduct(u, v, n):R) +251        (squaredNorm(v, n):R)252proof253  have combined := addSequence.sequence with sequenceU, sequenceV254  have first := dotProduct.add_left with sequenceU, sequenceV, combined255  have second := dotProduct.add_right with sequenceU, sequenceU, sequenceV256  have third := dotProduct.add_right with sequenceV, sequenceU, sequenceV257  have symmetry := dotProduct.symmetric with sequenceV, sequenceU258  simp [squaredNorm]259  ring260261theorem squaredNorm.sub (u v : Set, n : Nat)262  requires sequenceU : RealSequence(u)263  requires sequenceV : RealSequence(v)264  shows squaredNorm(subSequence(u, v), n) =265    ((squaredNorm(u, n):R) -266      (2:R) * (dotProduct(u, v, n):R)) +267        (squaredNorm(v, n):R)268proof269  induction n270  | zero =>271    unfold squaredNorm272    rw [dotProduct.zero, dotProduct.zero, dotProduct.zero, dotProduct.zero]273    ring274  | succ(k) using ih =>275    have difference := subSequence.sequence with sequenceU, sequenceV276    have uk := RealSequence.value with sequenceU277    have vk := RealSequence.value with sequenceV278    have differenceK := RealSequence.value with difference279    have value := subSequence.value with sequenceU, sequenceV, uk, vk280    rw [squaredNorm.succ, squaredNorm.succ, squaredNorm.succ, dotProduct.succ, value, ih]281    ring282283theorem squaredNorm.parallelogram (u v : Set, n : Nat)284  requires sequenceU : RealSequence(u)285  requires sequenceV : RealSequence(v)286  shows (squaredNorm(addSequence(u, v), n):R) +287      (squaredNorm(subSequence(u, v), n):R) =288    (2:R) * (squaredNorm(u, n):R) +289      (2:R) * (squaredNorm(v, n):R)290proof291  have combined := addSequence.sequence with sequenceU, sequenceV292  have difference := subSequence.sequence with sequenceU, sequenceV293  have normU := squaredNorm.real with sequenceU294  have normV := squaredNorm.real with sequenceV295  have cross := dotProduct.real with sequenceU, sequenceV296  have plus := squaredNorm.add with sequenceU, sequenceV297  have minus := squaredNorm.sub with sequenceU, sequenceV298  have algebra : ∀ A ∈ ℝ, ∀ B ∈ ℝ, ∀ C ∈ ℝ,299      ((A:R) + B + C) + ((A - B) + C) =300        (2:R) * A + (2:R) * C301    intros A realA B realB C realC302    ring303  have memberNormU : squaredNorm(u, n) ∈ ℝ by exact normU304  have memberNormV : squaredNorm(v, n) ∈ ℝ by exact normV305  have memberCross : (2:R) * dotProduct(u, v, n) ∈ ℝ by typecheck306  have combinedAlgebra := algebra with squaredNorm(u, n), memberNormU,307    (2:R) * dotProduct(u, v, n), memberCross,308    squaredNorm(v, n), memberNormV309  calc310    (squaredNorm(addSequence(u, v), n):R) +311        (squaredNorm(subSequence(u, v), n):R) =312      ((squaredNorm(u, n):R) +313        (2:R) * (dotProduct(u, v, n):R) +314          (squaredNorm(v, n):R)) +315      (((squaredNorm(u, n):R) -316        (2:R) * (dotProduct(u, v, n):R)) +317          (squaredNorm(v, n):R)) := by cc318    _ = (2:R) * (squaredNorm(u, n):R) +319          (2:R) * (squaredNorm(v, n):R) := combinedAlgebra320321theorem squaredNorm.pythagorean (u v : Set, n : Nat)322  requires sequenceU : RealSequence(u)323  requires sequenceV : RealSequence(v)324  requires orthogonal : Orthogonal(u, v, n)325  shows squaredNorm(addSequence(u, v), n) =326    (squaredNorm(u, n):R) + (squaredNorm(v, n):R)327proof328  have expansion := squaredNorm.add with sequenceU, sequenceV329  unfold Orthogonal at orthogonal330  rw orthogonal at expansion331  calc332    squaredNorm(addSequence(u, v), n) =333        (squaredNorm(u, n):R) + (2:R) * (0:R) +334          (squaredNorm(v, n):R) := expansion335    _ = (squaredNorm(u, n):R) + (squaredNorm(v, n):R) := by ring336