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.getScalar_vec_mat_mul_spec {m n : ℕ} (v : TorchLean.Tensor ℝ [m]) (A : TorchLean.Tensor ℝ [m, n]) (j : Fin n) : (vecMatMulSpec v A).getScalar j = ∑ i : Fin m, v.getScalar i * get2 A i j

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

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.

theorem Spec.get_preserves_inner_shape {n : ℕ} {s : Shape} (t : TorchLean.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 : TorchLean.Tensor ℝ s) : TorchLean.Tensor.mapSpec id t = t

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

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

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

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

A scalar additivity law lifts pointwise through mapSpec and addSpec.

theorem Spec.map2_spec_comm {s : Shape} (f : ℝ → ℝ → ℝ) (a b : TorchLean.Tensor ℝ s) (h : ∀ (x y : ℝ), f x y = f y x) : TorchLean.Tensor.map2Spec f a b = TorchLean.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 : 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ᵀ.

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⟫.

theorem Spec.outer_product_transpose {m n : ℕ} (a : TorchLean.Tensor ℝ [m]) (b : TorchLean.Tensor ℝ [n]) : (outerProductSpec a b).swapAdjacentAxes 0 = outerProductSpec b a

Outer product properties. Essential for proving weight gradient correctness.

Reductions and aggregation