LinearAlgebraStarter

Finite dimensional linear algebra through the public subject import

Open in Workbench View on GitHub

1-- Finite dimensional linear algebra through the public subject import.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module LinearAlgebraStarter7import Grace.Cumulus.LinearAlgebra89theorem dot_is_symmetric (u v : Set, n : Nat)10  requires vectorsU : RealSequence(u)11  requires vectorsV : RealSequence(v)12  shows dotProduct(u, v, n) = dotProduct(v, u, n)13proof14  exact dotProduct.symmetric with vectorsU, vectorsV1516theorem dot_distributes (u v w : Set, n : Nat)17  requires vectorsU : RealSequence(u)18  requires vectorsV : RealSequence(v)19  requires vectorsW : RealSequence(w)20  shows dotProduct(u, addSequence(v, w), n) =21    (dotProduct(u, v, n):R) + (dotProduct(u, w, n):R)22proof23  exact dotProduct.add_right with vectorsU, vectorsV, vectorsW2425theorem squares_are_nonnegative (u : Set, n : Nat)26  requires vector : RealSequence(u)27  shows (0:R) ≤ (squaredNorm(u, n):R)28proof29  exact squaredNorm.nonnegative with vector3031theorem scaling_squares (u : Set, C : Real, n : Nat)32  requires vector : RealSequence(u)33  shows squaredNorm(mulSequence(constantSequence(C), u), n) =34    (C * C) * (squaredNorm(u, n):R)35proof36  exact squaredNorm.scale with vector3738theorem parallelogram_identity (u v : Set, n : Nat)39  requires vectorsU : RealSequence(u)40  requires vectorsV : RealSequence(v)41  shows (squaredNorm(addSequence(u, v), n):R) +42      (squaredNorm(subSequence(u, v), n):R) =43    (2:R) * (squaredNorm(u, n):R) +44      (2:R) * (squaredNorm(v, n):R)45proof46  exact squaredNorm.parallelogram with vectorsU, vectorsV4748theorem pythagorean_identity (u v : Set, n : Nat)49  requires vectorsU : RealSequence(u)50  requires vectorsV : RealSequence(v)51  requires perpendicular : Orthogonal(u, v, n)52  shows squaredNorm(addSequence(u, v), n) =53    (squaredNorm(u, n):R) + (squaredNorm(v, n):R)54proof55  exact squaredNorm.pythagorean at u, v, n with56    vectorsU, vectorsV, perpendicular5758-- A matrix is a function from pairs of natural indices to real entries.59-- The finite column cutoff n determines the part used by multiplication.60theorem matrix_entry_is_real (M : Set, i j : Nat)61  requires matrix : RealMatrix(M)62  shows Real(M[i, j])63proof64  exact RealMatrix.entry with matrix6566theorem matrix_times_sum (M u v : Set, n i : Nat)67  requires matrix : RealMatrix(M)68  requires vectorsU : RealSequence(u)69  requires vectorsV : RealSequence(v)70  shows matrixVectorProduct(M, addSequence(u, v), n)[i] =71    (matrixVectorProduct(M, u, n)[i]:R) +72    (matrixVectorProduct(M, v, n)[i]:R)73proof74  exact matrixVectorProduct.add with matrix, vectorsU, vectorsV7576theorem matrix_times_scalar (M u : Set, C : Real, n i : Nat)77  requires matrix : RealMatrix(M)78  requires vector : RealSequence(u)79  shows matrixVectorProduct(M, mulSequence(constantSequence(C), u), n)[i] =80    C * (matrixVectorProduct(M, u, n)[i]:R)81proof82  exact matrixVectorProduct.scale with matrix, vector8384theorem matrix_ignores_later_coordinates (M u v : Set, n i : Nat)85  requires matrix : RealMatrix(M)86  requires vectorsU : RealSequence(u)87  requires vectorsV : RealSequence(v)88  requires samePrefix : ∀ k ∈ ℕ, k < n → u[k] = v[k]89  shows matrixVectorProduct(M, u, n)[i] = matrixVectorProduct(M, v, n)[i]90proof91  exact matrixVectorProduct.eq_prefix at M, u, v, n, i with92    matrix, vectorsU, vectorsV, samePrefix9394theorem transpose_swaps_entries (M : Set, i j : Nat)95  requires matrix : RealMatrix(M)96  shows matrixTranspose(M)[i, j] = M[j, i]97proof98  exact matrixTranspose.entry with matrix99100theorem transpose_twice (M : Set, i j : Nat)101  requires matrix : RealMatrix(M)102  shows matrixTranspose(matrixTranspose(M))[i, j] = M[i, j]103proof104  exact matrixTranspose.involutive_entry with matrix105106theorem product_is_row_by_column (A B : Set, n i j : Nat)107  requires matricesA : RealMatrix(A)108  requires matricesB : RealMatrix(B)109  shows matrixProduct(A, B, n)[i, j] =110    dotProduct(matrixRow(A, i), matrixColumn(B, j), n)111proof112  exact matrixProduct.entry with matricesA, matricesB113114theorem product_transpose_reverses (A B : Set, n i j : Nat)115  requires matricesA : RealMatrix(A)116  requires matricesB : RealMatrix(B)117  shows matrixTranspose(matrixProduct(A, B, n))[i, j] =118    matrixProduct(matrixTranspose(B), matrixTranspose(A), n)[i, j]119proof120  exact matrixProduct.transpose_entry with matricesA, matricesB121122theorem matrix_sum_entry (A B : Set, i j : Nat)123  requires matricesA : RealMatrix(A)124  requires matricesB : RealMatrix(B)125  shows matrixAdd(A, B)[i, j] = (A[i, j]:R) + (B[i, j]:R)126proof127  exact matrixAdd.entry with matricesA, matricesB128129theorem transpose_distributes (A B : Set, i j : Nat)130  requires matricesA : RealMatrix(A)131  requires matricesB : RealMatrix(B)132  shows matrixTranspose(matrixAdd(A, B))[i, j] =133    matrixAdd(matrixTranspose(A), matrixTranspose(B))[i, j]134proof135  exact matrixTranspose.add_entry with matricesA, matricesB136137theorem matrix_action_distributes (A B u : Set, i n : Nat)138  requires matricesA : RealMatrix(A)139  requires matricesB : RealMatrix(B)140  requires vector : RealSequence(u)141  shows matrixVectorProduct(matrixAdd(A, B), u, n)[i] =142    (matrixVectorProduct(A, u, n)[i]:R) + (matrixVectorProduct(B, u, n)[i]:R)143proof144  exact matrixVectorProduct.add_matrix at A, B, u, i, n with145    matricesA, matricesB, vector146147theorem product_distributes (A B C : Set, i j n : Nat)148  requires matricesA : RealMatrix(A)149  requires matricesB : RealMatrix(B)150  requires matricesC : RealMatrix(C)151  shows matrixProduct(A, matrixAdd(B, C), n)[i, j] =152    matrixAdd(matrixProduct(A, B, n), matrixProduct(A, C, n))[i, j]153proof154  exact matrixProduct.add_right_entry at A, B, C, i, j, n with155    matricesA, matricesB, matricesC156157theorem identity_diagonal (n i : Nat)158  shows identityMatrix(n)[i, i] = (1:R)159proof160  exact identityMatrix.diagonal with assumption, assumption161162theorem identity_off_diagonal (n i j : Nat)163  requires different : i ≠ j164  shows identityMatrix(n)[i, j] = (0:R)165proof166  exact identityMatrix.off_diagonal at n, i, j with167    assumption, assumption, assumption, different168169theorem identity_acts_on_vector (u : Set, n i : Nat)170  requires vector : RealSequence(u)171  requires inRange : i < n172  shows matrixVectorProduct(identityMatrix(n), u, n)[i] = u[i]173proof174  exact identityMatrix.action with vector, inRange175176theorem identity_acts_on_left (A : Set, n i j : Nat)177  requires matrix : RealMatrix(A)178  requires inRange : i < n179  shows matrixProduct(identityMatrix(n), A, n)[i, j] = A[i, j]180proof181  exact matrixProduct.identity_left with matrix, inRange182183theorem identity_acts_on_right (A : Set, n i j : Nat)184  requires matrix : RealMatrix(A)185  requires inRange : j < n186  shows matrixProduct(A, identityMatrix(n), n)[i, j] = A[i, j]187proof188  exact matrixProduct.identity_right with matrix, inRange189190theorem product_distributes_on_left (A B C : Set, i j n : Nat)191  requires matricesA : RealMatrix(A)192  requires matricesB : RealMatrix(B)193  requires matricesC : RealMatrix(C)194  shows matrixProduct(matrixAdd(A, B), C, n)[i, j] =195    matrixAdd(matrixProduct(A, C, n), matrixProduct(B, C, n))[i, j]196proof197  exact matrixProduct.add_left_entry at A, B, C, i, j, n with198    matricesA, matricesB, matricesC199200theorem finite_double_sum_interchange (M : Set, n m : Nat)201  requires matrix : RealMatrix(M)202  shows realPartialSum(matrixRowTotals(M, m), n) =203    realPartialSum(matrixColumnTotals(M, n), m)204proof205  exact matrixTotals.interchange with matrix206207-- Exact rational elimination is available through the same subject import.208theorem exact_rational_pivot209  shows RationalCellOps.isZero(RationalMatrixOps.entry(210    RationalMatrixOps.firstRow(RationalEliminationExamples.reduced), 0)) = Bool.false211proof212  simp213214theorem exact_rational_row_swap215  shows RationalMatrixOps.entry(RationalMatrixOps.firstRow(216    RationalMatrixOps.forward(1, 0, RationalEliminationExamples.swapped)), 0) =217    RationalCell.fraction(1, 0, 1)218proof219  simp220221theorem exact_rational_reduced_solution222  shows RationalCellOps.sameValue(RationalMatrixOps.entry(223      RationalMatrixOps.firstRow(RationalEliminationExamples.completelyReduced), 2),224    RationalCell.fraction(2, 0, 1)) = Bool.true225proof226  simp227228-- The replayable row operations encode a worked augmented-system reduction.229theorem checked_row_trace230  shows RationalRowCertificates.replayChecked(RationalRowCertificates.twoEquationTrace,231    RationalEliminationExamples.system) =232    Option.some(RationalRowCertificates.twoEquationResult)233proof234  simp235236theorem checked_row_trace_solution237  shows RationalCellOps.sameValue(RationalMatrixOps.entry(238    RationalRowCertificates.rowAt(RationalRowCertificates.twoEquationResult, 1), 2),239    RationalCellOps.one) = Bool.true240proof241  simp242243theorem three_variable_pivot_and_solution244  shows BoolOps.and(RationalRowTraceExamples.hasFourValues(245    RationalRowCertificates.rowAt(RationalRowTraceExamples.threeResult, 0),246    RationalRowTraceExamples.cell(1), RationalRowTraceExamples.cell(0),247    RationalRowTraceExamples.cell(0), RationalRowTraceExamples.cell(1)),248    BoolOps.and(RationalRowTraceExamples.hasFourValues(249      RationalRowCertificates.rowAt(RationalRowTraceExamples.threeResult, 1),250      RationalRowTraceExamples.cell(0), RationalRowTraceExamples.cell(1),251      RationalRowTraceExamples.cell(0), RationalRowTraceExamples.cell(2)),252      RationalRowTraceExamples.hasFourValues(253        RationalRowCertificates.rowAt(RationalRowTraceExamples.threeResult, 2),254        RationalRowTraceExamples.cell(0), RationalRowTraceExamples.cell(0),255        RationalRowTraceExamples.cell(1), RationalRowTraceExamples.cell(3)))) = Bool.true256proof257  simp258259theorem inconsistent_system_detected260  shows RationalCellOps.isZero(RationalMatrixOps.entry(261    RationalRowCertificates.rowAt(RationalRowTraceExamples.inconsistentResult, 1), 2)) = Bool.false262proof263  simp264265theorem dependent_system_zero_row266  shows RationalCellOps.isZero(RationalMatrixOps.entry(267    RationalRowCertificates.rowAt(RationalRowTraceExamples.dependentResult, 1), 2)) = Bool.true268proof269  compute270