Linear-algebra facts for dependent tensors.

The results here cover dot products, matrix-vector structure, and linearity facts used by autograd, runtime approximation, and model proofs.

theorem Spec.sum_spec_vec {n : ℕ} (v : TorchLean.Tensor ℝ [n]) : v.sumSpec = ∑ i : Fin n, v.getScalar i

sumSpec on a 1D tensor equals the Finset sum of its coordinates (getScalar).

theorem Spec.getScalar_mul_spec {n : ℕ} (a b : TorchLean.Tensor ℝ [n]) (i : Fin n) : (a.mulSpec b).getScalar i = a.getScalar i * b.getScalar i

getScalar of mulSpec is pointwise multiplication of coordinate functions.

theorem Spec.dot_vec_eq_sum {n : ℕ} (a b : TorchLean.Tensor ℝ [n]) : dot a b = ∑ i : Fin n, a.getScalar i * b.getScalar i

Dot product of vectors is the coordinate-wise sum ∑ i, a[i] * b[i].

theorem Spec.dot_mat_linear_adjoint {inDim outDim : ℕ} (W : TorchLean.Tensor ℝ [outDim, inDim]) (dLdy : TorchLean.Tensor ℝ [outDim]) (dx : TorchLean.Tensor ℝ [inDim]) : dot dLdy (matVecMulSpec W dx) = dot (vecMatMulSpec dLdy W) dx

Adjointness of matrix-vector and vector-matrix multiplication under the dot product: ⟪y, W x⟫ = ⟪y W, x⟫ (a.k.a. ⟪y, W x⟫ = ⟪Wᵀ y, x⟫ depending on conventions).

This is the algebraic heart of the linear-layer gradient rule.

theorem Spec.shapeOf_eq_shape {α : Type} [TorchLean.Storage α] {s : Shape} (t : TorchLean.Tensor α s) : shapeOf t = s

shapeOf recovers the shape already tracked in the tensor type.

This is a small bridge for proofs that move between value-level shape computations and type-indexed tensor operations.

Matrix and vector algebra

theorem Spec.mat_vec_assoc {m n p : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (B : TorchLean.Tensor ℝ [n, p]) (x : TorchLean.Tensor ℝ [p]) : matVecMulSpec A (matVecMulSpec B x) = matVecMulSpec (matMulSpec A B) x

Associativity of matrix-vector multiplication: A (B x) = (A B) x.

theorem Spec.get2_matrix_transpose_spec {m n : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (i : Fin n) (j : Fin m) : get2 (A.swapAdjacentAxes 0) i j = get2 A j i

Coordinate rule for the matrix transpose swapAdjacentAxes A 0: (Aᵀ)[i,j] = A[j,i].

theorem Spec.matrix_ext {m n : ℕ} {A B : TorchLean.Tensor ℝ [m, n]} : (∀ (i : Fin m) (j : Fin n), get2 A i j = get2 B i j) → A = B

Matrix extensionality: matrices are equal when all their entries are equal.

theorem Spec.matrix_transpose_involution {m n : ℕ} (A : TorchLean.Tensor ℝ [m, n]) : (A.swapAdjacentAxes 0).swapAdjacentAxes 0 = A

Matrix transpose is an involution.

theorem Spec.matrix_transpose_mul {m n p : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (B : TorchLean.Tensor ℝ [n, p]) : (matMulSpec A B).swapAdjacentAxes 0 = matMulSpec (B.swapAdjacentAxes 0) (A.swapAdjacentAxes 0)

Transpose of a product: (A ⬝ B)ᵀ = Bᵀ ⬝ Aᵀ.

Frobenius dot and matmul adjointness

theorem Spec.dot_mat_eq_sum {m n : ℕ} (A B : TorchLean.Tensor ℝ [m, n]) : dot A B = ∑ i : Fin m, ∑ j : Fin n, get2 A i j * get2 B i j

Expand the matrix dot-product as a double sum over entries (Frobenius inner product).

theorem Spec.dot_mat_mul_right_adjoint {m n p : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (B : TorchLean.Tensor ℝ [n, p]) (C : TorchLean.Tensor ℝ [m, p]) : dot (matMulSpec A B) C = dot A (matMulSpec C (B.swapAdjacentAxes 0))

Right-adjointness of matrix multiplication under the Frobenius dot-product.

Informally: ⟪A ⬝ B, C⟫ = ⟪A, C ⬝ Bᵀ⟫.

theorem Spec.dot_mat_transpose {m n : ℕ} (A B : TorchLean.Tensor ℝ [m, n]) : dot (A.swapAdjacentAxes 0) (B.swapAdjacentAxes 0) = dot A B

Transpose invariance of the Frobenius dot-product: ⟪Aᵀ, Bᵀ⟫ = ⟪A, B⟫.

theorem Spec.dot_mat_mul_left_adjoint {m n p : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (B : TorchLean.Tensor ℝ [n, p]) (C : TorchLean.Tensor ℝ [m, p]) : dot (matMulSpec A B) C = dot B (matMulSpec (A.swapAdjacentAxes 0) C)

Left-adjointness of matrix multiplication under the Frobenius dot-product.

Informally: ⟪A ⬝ B, C⟫ = ⟪B, Aᵀ ⬝ C⟫.

Entry rules for matrix-shaped tensor operations

theorem Spec.get2_identityTensorSpec {α : Type} [TorchLean.Storage α] [Zero α] [One α] {n : ℕ} (i j : Fin n) : get2 (identityTensorSpec n) i j = if i = j then 1 else 0

Entries of the identity matrix, in the get2 form the certificate proofs consume.

theorem Spec.get2_addSpec {α : Type} [TorchLean.Storage α] [Add α] {m n : ℕ} (A B : TorchLean.Tensor α [m, n]) (i : Fin m) (j : Fin n) : get2 (A.addSpec B) i j = get2 A i j + get2 B i j

Entry rule for matrix-shaped tensor addition.

theorem Spec.get2_scaleSpec {α : Type} [TorchLean.Storage α] [Mul α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (c : α) (i : Fin m) (j : Fin n) : get2 (A.scaleSpec c) i j = get2 A i j * c

Entry rule for matrix-shaped tensor scaling.

theorem Spec.get2_subSpec {α : Type} [TorchLean.Storage α] [Sub α] {m n : ℕ} (A B : TorchLean.Tensor α [m, n]) (i : Fin m) (j : Fin n) : get2 (A.subSpec B) i j = get2 A i j - get2 B i j

Entry rule for matrix-shaped tensor subtraction.

Real matrix identities

theorem Spec.matMulSpec_identityTensorSpec {m n : ℕ} (A : TorchLean.Tensor ℝ [m, n]) : matMulSpec A (identityTensorSpec n) = A

Right multiplication by the identity matrix leaves a real matrix unchanged.

theorem Spec.scaleSpec_one {m n : ℕ} (Q : TorchLean.Tensor ℝ [m, n]) : Q.scaleSpec 1 = Q

Scaling a real matrix by 1 returns the matrix.