Tensor Algebra Proofs

Backend-generic algebraic tensor lemmas.

This file provides the semiring-level dot-product API and supporting fold/sum lemmas used by autograd and tape soundness proofs. The point of this file is to avoid baking ℝ, topology, or calculus assumptions into algebra that only needs addition, multiplication, and finite sums.

NN.Proofs.Tensor.Basic imports this file and adds the ℝ-specialized spec-facing toolkit (norms, shape facts, Frobenius identities, and convenience lemmas for analysis proofs). Keeping this file generic lets correctness theorems reuse the same algebra over exact rationals, real numbers, or other semiring-like scalar models.

PyTorch correspondence / citations

• Elementwise product + sum (“flattened dot” for same-shape tensors): (a * b).sum(). https://pytorch.org/docs/stable/generated/torch.sum.html
• 1D dot product: torch.dot(a, b) (for real tensors). https://pytorch.org/docs/stable/generated/torch.dot.html

Vector views

def Proofs.TensorAlgebra.toVec {α : Type} {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : Fin n → α

View a 1D tensor of shape (n,) as a function Fin n → α.

Informally: this is the spec-level analogue of PyTorch indexing t[i] for a vector.

def Proofs.TensorAlgebra.ofVec {α : Type} {n : ℕ} (v : Fin n → α) : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)

Build a 1D tensor of shape (n,) from a function Fin n → α.

ofVec is the inverse direction of toVec (up to definitional equality).

@[simp]

theorem Proofs.TensorAlgebra.toVec_ofVec {α : Type} {n : ℕ} (v : Fin n → α) : toVec (ofVec v) = v

theorem Proofs.TensorAlgebra.ofVec_toVec {α : Type} {n : ℕ} (t : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : ofVec (toVec t) = t

Recursive same-shape dot product

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

Dot product for tensors of the same shape: multiply elementwise and sum over all scalar leaves.

For shape (n,) this matches torch.dot (over a commutative semiring, i.e. ignoring complex conjugation). More generally it matches the common PyTorch idiom (a * b).sum() for same-shape tensors.

List-fold helpers

theorem Proofs.TensorAlgebra.foldl_add_distrib2 {α β : Type} [AddCommMonoid α] (l : List β) (g1 g2 : β → α) (a1 a2 : α) : List.foldl (fun (s : α) (x : β) => s + (g1 x + g2 x)) (a1 + a2) l = List.foldl (fun (s : α) (x : β) => s + g1 x) a1 l + List.foldl (fun (s : α) (x : β) => s + g2 x) a2 l

Distribute a fold of g1 x + g2 x into the sum of two folds.

This is a general “sum splits over addition” lemma used to prove bilinearity-like properties of dot.

From executable folds to proof-friendly sums

theorem Proofs.TensorAlgebra.finRange_foldl_add_eq_finset_sum {α : Type} [AddCommMonoid α] {n : ℕ} (f : Fin n → α) : List.foldl (fun (s : α) (i : Fin n) => s + f i) 0 (List.finRange n) = Finset.univ.sum f

Rewrite the spec-style fold over List.finRange n into a proof-friendly Finset.univ.sum.

Many spec definitions use List.foldl (it is definitional and convenient for computation), while proofs often prefer Finset.sum so they can use standard big-operator lemmas.

Dot-product algebra

@[simp]

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

Scaling

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

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

Symmetry of dot (commutativity) over a commutative semiring.

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

Left-scaling: dot (k • a) b = k * dot a b.

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

Additivity in the left argument: dot (a + b) c = dot a c + dot b c.

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

Additivity in the right argument: dot a (b + c) = dot a b + dot a c.

theorem Proofs.TensorAlgebra.dot_fill_zero_right {α : Type} [CommSemiring α] {s : Spec.Shape} (a : Spec.Tensor α s) : dot a (Spec.fill 0 s) = 0

dot a 0 = 0 (where 0 is the all-zeros tensor via fill).

theorem Proofs.TensorAlgebra.dot_vec_eq_sum {α : Type} [CommSemiring α] {n : ℕ} (a b : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) : dot a b = ∑ i : Fin n, toVec a i * toVec b i

For vectors (n,), dot can be expressed as an explicit Finset.univ.sum.

This is the bridge between the recursive dot definition and “PyTorch-looking” summation formulas.

Matrix/vector adjointness: ⟪y, W x⟫ = ⟪y W, x⟫

theorem Proofs.TensorAlgebra.get2_eq {α : Type} {m n : ℕ} (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (i : Fin m) (j : Fin n) : Spec.get2 A i j = match Spec.get A i with | Spec.Tensor.dim row => match row j with | Spec.Tensor.scalar v => v

theorem Proofs.TensorAlgebra.get_eq {α : Type} {m : ℕ} {s : Spec.Shape} (t : Spec.Tensor α (Spec.Shape.dim m s)) (i : Fin m) : Spec.get t i = match t with | Spec.Tensor.dim f => f i

theorem Proofs.TensorAlgebra.foldl_matvec_scalar {α : Type} [CommSemiring α] {n : ℕ} (l : List (Fin n)) (a : α) (cols vals : Fin n → Spec.Tensor α Spec.Shape.scalar) : List.foldl (fun (acc : Spec.Tensor α Spec.Shape.scalar) (k : Fin n) => match acc, cols k, vals k with | Spec.Tensor.scalar s, Spec.Tensor.scalar ak, Spec.Tensor.scalar vk => Spec.Tensor.scalar (s + ak * vk)) (Spec.Tensor.scalar a) l = Spec.Tensor.scalar (List.foldl (fun (s : α) (k : Fin n) => match cols k, vals k with | Spec.Tensor.scalar ak, Spec.Tensor.scalar vk => s + ak * vk) a l)

theorem Proofs.TensorAlgebra.toVec_mat_vec_mul_spec {α : Type} [CommSemiring α] {m n : ℕ} (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (v : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin m) : toVec (Spec.matVecMulSpec A v) i = ∑ k : Fin n, Spec.get2 A i k * toVec v k

Matrix-vector multiply coordinate expansion.

This is a spec-to-proof bridge: it turns the List.finRange fold in mat_vec_mul_spec into a Finset.univ.sum formula, matching the textbook / PyTorch view of matvec as a dot product.

theorem Proofs.TensorAlgebra.toVec_vec_mat_mul_spec {α : Type} [CommSemiring α] {m n : ℕ} (v : Spec.Tensor α (Spec.Shape.dim m Spec.Shape.scalar)) (A : Spec.Tensor α (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (j : Fin n) : toVec (Spec.vecMatMulSpec v A) j = ∑ i : Fin m, toVec v i * Spec.get2 A i j

Vector-matrix multiply coordinate expansion.

This is the right-adjoint analogue of toVec_mat_vec_mul_spec.

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

Adjointness identity for matvec under dot.

Informally: ⟨dLdy, W dx⟩ = ⟨dLdy W, dx⟩, i.e. the transpose-adjoint relationship between matrix-vector and vector-matrix multiplication.

In PyTorch this corresponds to the familiar identity (dLdyᵀ @ (W @ dx)) = ((dLdyᵀ @ W) @ dx), written with explicit sums.