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 : Tensor ℝ (Shape.dim n Shape.scalar)) : v.sumSpec = ∑ i : Fin n, toVec v i

sum_spec on a 1D tensor equals the Finset sum of its coordinates (toVec).

theorem Spec.toVec_mul_spec {n : ℕ} (a b : Tensor ℝ (Shape.dim n Shape.scalar)) (i : Fin n) : toVec (a.mulSpec b) i = toVec a i * toVec b i

toVec of mul_spec is pointwise multiplication of coordinate functions.

theorem Spec.dot_vec_eq_sum {n : ℕ} (a b : Tensor ℝ (Shape.dim n Shape.scalar)) : dot a b = ∑ i : Fin n, toVec a i * toVec b i

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

theorem Spec.toVec_vec_mat_mul_spec {m n : ℕ} (v : Tensor ℝ (Shape.dim m Shape.scalar)) (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (j : Fin n) : toVec (vecMatMulSpec v A) j = ∑ i : Fin m, toVec v i * get2 A i j

Coordinate formula for vec_mat_mul_spec as a Finset sum: (v @ A)[j] = ∑ i, v[i] * A[i,j].

theorem Spec.dot_mat_linear_adjoint {inDim outDim : ℕ} (W : Tensor ℝ (Shape.dim outDim (Shape.dim inDim Shape.scalar))) (dLdy : Tensor ℝ (Shape.dim outDim Shape.scalar)) (dx : Tensor ℝ (Shape.dim inDim Shape.scalar)) : 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} {s : Shape} (t : 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.

theorem Spec.get_preserves_inner_shape {n : ℕ} {s : Shape} (t : Tensor ℝ (Shape.dim n s)) (i : Fin n) : shapeOf (get t i) = s

Indexing the outer dimension of a tensor exposes a subtensor with the declared inner shape.

Map and elementwise operation laws

theorem Spec.map_spec_id {s : Shape} (t : Tensor ℝ s) : Tensor.mapSpec id t = t

Functor identity law for map_spec: mapping id is a no-op.

theorem Spec.map_spec_comp {s : Shape} (f g : ℝ → ℝ) (t : Tensor ℝ s) : Tensor.mapSpec f (Tensor.mapSpec g t) = Tensor.mapSpec (f ∘ g) t

Functor law for map_spec: mapping g then f equals mapping f ∘ g.

theorem Spec.map_spec_add_distrib {s : Shape} (f : ℝ → ℝ) (a b : Tensor ℝ s) (h : ∀ (x y : ℝ), f (x + y) = f x + f y) : Tensor.mapSpec f (a.addSpec b) = (Tensor.mapSpec f a).addSpec (Tensor.mapSpec f b)

A scalar additivity law lifts pointwise through map_spec and add_spec.

theorem Spec.map2_spec_comm {s : Shape} (f : ℝ → ℝ → ℝ) (a b : Tensor ℝ s) (h : ∀ (x y : ℝ), f x y = f y x) : Tensor.map2Spec f a b = Tensor.map2Spec f b a

Commutativity transfer: if f is commutative, then map2_spec f is commutative on tensors.

Matrix and vector algebra

theorem Spec.mat_vec_assoc {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (x : Tensor ℝ (Shape.dim p Shape.scalar)) : matVecMulSpec A (matVecMulSpec B x) = matVecMulSpec (matMulSpec A B) x

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

theorem Spec.matrix_transpose_involution {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) : A.matrixTransposeSpec.matrixTransposeSpec = A

Matrix transpose is an involution.

theorem Spec.get2_matrix_transpose_spec {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (i : Fin n) (j : Fin m) : get2 A.matrixTransposeSpec i j = get2 A j i

Coordinate rule for matrix_transpose_spec: (Aᵀ)[i,j] = A[j,i].

theorem Spec.matrix_ext {m n : ℕ} {A B : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))} : (∀ (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_mul {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) : (matMulSpec A B).matrixTransposeSpec = matMulSpec B.matrixTransposeSpec A.matrixTransposeSpec

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

theorem Spec.dot_mat_eq_sum {m n : ℕ} (A B : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) : 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 : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (C : Tensor ℝ (Shape.dim m (Shape.dim p Shape.scalar))) : dot (matMulSpec A B) C = dot A (matMulSpec C B.matrixTransposeSpec)

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 : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) : dot A.matrixTransposeSpec B.matrixTransposeSpec = 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 : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (C : Tensor ℝ (Shape.dim m (Shape.dim p Shape.scalar))) : dot (matMulSpec A B) C = dot B (matMulSpec A.matrixTransposeSpec C)

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

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

theorem Spec.outer_product_transpose {m n : ℕ} (a : Tensor ℝ (Shape.dim m Shape.scalar)) (b : Tensor ℝ (Shape.dim n Shape.scalar)) : (outerProductSpec a b).matrixTransposeSpec = outerProductSpec b a

Outer product properties. Essential for proving weight gradient correctness.

Reductions and aggregation