Tensor algebra proofs

Backend-generic algebraic lemmas for TorchLean's single packed tensor type. Proofs observe tensors through item, unstack, and typed indexing; they do not depend on the physical buffer selected by Storage.

def Proofs.TensorAlgebra.dot {α : Type} [TorchLean.Storage α] [Zero α] [Add α] [Mul α] {shape : Spec.Shape} : TorchLean.Tensor α shape → TorchLean.Tensor α shape → α

Multiply matching scalar entries and add them in row-major shape order.

Fold bridges

theorem Proofs.TensorAlgebra.add_finRange_foldl_add_zero {α : Type} [AddMonoid α] {n : ℕ} (f : Fin n → α) (accumulator : α) : accumulator + List.foldl (fun (sum : α) (i : Fin n) => sum + f i) 0 (List.finRange n) = List.foldl (fun (sum : α) (i : Fin n) => sum + f i) accumulator (List.finRange n)

Push an accumulator into an additive fold that starts at zero.

theorem Proofs.TensorAlgebra.foldl_tensorScalar_mulAdd {α : Type} [TorchLean.Storage α] [Add α] [Mul α] {n : ℕ} (columns values : Fin n → TorchLean.Tensor α Spec.Shape.scalar) (indices : List (Fin n)) (initial : α) : List.foldl (fun (accumulator : TorchLean.Tensor α Spec.Shape.scalar) (index : Fin n) => TorchLean.Tensor.scalar (accumulator.item + (columns index).item * (values index).item)) (TorchLean.Tensor.scalar initial) indices = TorchLean.Tensor.scalar (List.foldl (fun (accumulator : α) (index : Fin n) => accumulator + (columns index).item * (values index).item) initial indices)

A fold over scalar tensors is the corresponding fold over scalar values.

Dot-product algebra

@[simp]

theorem Proofs.TensorAlgebra.dot_scalar {α : Type} [TorchLean.Storage α] [CommSemiring α] (a b : α) : dot (TorchLean.Tensor.scalar a) (TorchLean.Tensor.scalar b) = a * b

The dot product of two scalars is their product: the base case of the recursion.

theorem Proofs.TensorAlgebra.dot_scale_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) (k : α) : dot a (b.scaleSpec k) = dot a b * k

Dot is multiplicative with scalar scaling in its right argument.

theorem Proofs.TensorAlgebra.dot_comm {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) : dot a b = dot b a

Dot is symmetric over a commutative semiring.

theorem Proofs.TensorAlgebra.dot_scale_left {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) (k : α) : dot (a.scaleSpec k) b = dot a b * k

Dot is multiplicative with scalar scaling in its left argument.

theorem Proofs.TensorAlgebra.dot_add_left {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (a b c : TorchLean.Tensor α s) : dot (a.addSpec b) c = dot a c + dot b c

Dot distributes over addition in its left argument.

theorem Proofs.TensorAlgebra.dot_add_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (a b c : TorchLean.Tensor α s) : dot a (b.addSpec c) = dot a b + dot a c

Dot distributes over addition in its right argument.

theorem Proofs.TensorAlgebra.dot_full_zero_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (a : TorchLean.Tensor α s) : dot a (TorchLean.Tensor.full s 0) = 0

The dot product with an all-zero tensor is zero.

theorem Proofs.TensorAlgebra.dot_vec_eq_sum {α : Type} [TorchLean.Storage α] [CommSemiring α] {n : ℕ} (a b : TorchLean.Tensor α [n]) : dot a b = ∑ index : Fin n, a.getScalar index * b.getScalar index

Vector dot is the ordinary finite sum of matching scalar coordinates.

Indexing and matrix/vector bridges

theorem Proofs.TensorAlgebra.get2_eq {α : Type} [TorchLean.Storage α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (i : Fin m) (j : Fin n) : Spec.get2 A i j = ((A.unstack i).unstack j).item

Matrix indexing is two successive packed leading-axis selections.

theorem Proofs.TensorAlgebra.get_eq {α : Type} [TorchLean.Storage α] {m : ℕ} {shape : Spec.Shape} (t : TorchLean.Tensor α (Spec.Shape.dim m shape)) (i : Fin m) : Spec.get t i = t.unstack i

Spec.get is the public spelling of packed leading-axis selection.

theorem Proofs.TensorAlgebra.foldl_matvec_scalar {α : Type} [TorchLean.Storage α] [CommSemiring α] {n : ℕ} (l : List (Fin n)) (a : α) (cols vals : Fin n → TorchLean.Tensor α Spec.Shape.scalar) : List.foldl (fun (accumulator : TorchLean.Tensor α Spec.Shape.scalar) (index : Fin n) => TorchLean.Tensor.scalar (accumulator.item + (cols index).item * (vals index).item)) (TorchLean.Tensor.scalar a) l = TorchLean.Tensor.scalar (List.foldl (fun (accumulator : α) (index : Fin n) => accumulator + (cols index).item * (vals index).item) a l)

Scalar-tensor multiply-add folds agree with their scalar-value folds.

theorem Proofs.TensorAlgebra.getScalar_mat_vec_mul_spec {α : Type} [TorchLean.Storage α] [CommSemiring α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (v : TorchLean.Tensor α [n]) (i : Fin m) : (Spec.matVecMulSpec A v).getScalar i = ∑ k : Fin n, Spec.get2 A i k * v.getScalar k

Coordinate expansion of matrix-vector multiplication.

theorem Proofs.TensorAlgebra.getScalar_vec_mat_mul_spec {α : Type} [TorchLean.Storage α] [CommSemiring α] {m n : ℕ} (v : TorchLean.Tensor α [m]) (A : TorchLean.Tensor α [m, n]) (j : Fin n) : (Spec.vecMatMulSpec v A).getScalar j = ∑ i : Fin m, v.getScalar i * Spec.get2 A i j

Coordinate expansion of vector-matrix multiplication.

theorem Proofs.TensorAlgebra.dot_mat_linear_adjoint {α : Type} [TorchLean.Storage α] [CommSemiring α] {inDim outDim : ℕ} (W : TorchLean.Tensor α [outDim, inDim]) (dLdy : TorchLean.Tensor α [outDim]) (dx : TorchLean.Tensor α [inDim]) : dot dLdy (Spec.matVecMulSpec W dx) = dot (Spec.vecMatMulSpec dLdy W) dx

Matrix-vector and vector-matrix multiplication are adjoint under dot.