Tensor Algebra Lemmas

This file collects foundational algebraic lemmas for TorchLean.Tensor over ℝ: pointwise arithmetic identities, linearity of matrix-vector multiplication, and the scalar-fold bridge used throughout the autograd and runtime-correctness proof files.

theorem Spec.add_spec_assoc {s : Shape} (a b c : TorchLean.Tensor ℝ s) : (a.addSpec b).addSpec c = a.addSpec (b.addSpec c)

Elementwise addition is associative (over $\mathbb R$ tensors).

theorem Spec.sub_spec_add_right {s : Shape} (a b c : TorchLean.Tensor ℝ s) : a.subSpec (b.addSpec c) = (a.subSpec b).addSpec c.negSpec

Elementwise subtraction distributes over addition on the right.

theorem Spec.mul_spec_add_right {s : Shape} (a b c : TorchLean.Tensor ℝ s) : a.mulSpec (b.addSpec c) = (a.mulSpec b).addSpec (a.mulSpec c)

Elementwise multiplication distributes over addition on the right.

theorem Spec.mul_spec_add_left {s : Shape} (a b c : TorchLean.Tensor ℝ s) : (a.addSpec b).mulSpec c = (a.mulSpec c).addSpec (b.mulSpec c)

Elementwise multiplication distributes over addition on the left.

theorem Spec.sub_spec_bias_cancel {s : Shape} (a b c : TorchLean.Tensor ℝ s) : (a.addSpec c).subSpec (b.addSpec c) = a.subSpec b

Bias cancellation for tensor subtraction: (a + c) - (b + c) = a - b.

theorem Spec.mat_vec_add {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x y : TorchLean.Tensor ℝ [n]) : matVecMulSpec W (x.addSpec y) = (matVecMulSpec W x).addSpec (matVecMulSpec W y)

Linearity of matrix-vector multiplication in the vector argument (addition).

theorem Spec.mat_vec_scale {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x : TorchLean.Tensor ℝ [n]) (c : ℝ) : matVecMulSpec W (x.scaleSpec c) = (matVecMulSpec W x).scaleSpec c

Linearity of matrix-vector multiplication in the vector argument (scaling).

theorem Spec.mat_vec_linear_combination {m n : ℕ} (W : TorchLean.Tensor ℝ [m, n]) (x y : TorchLean.Tensor ℝ [n]) (a b : ℝ) : matVecMulSpec W ((x.scaleSpec a).addSpec (y.scaleSpec b)) = ((matVecMulSpec W x).scaleSpec a).addSpec ((matVecMulSpec W y).scaleSpec b)

Full linearity of matrix-vector multiplication in the vector argument.

@[simp]

theorem Spec.add_spec_zero_left {s : Shape} (t : TorchLean.Tensor ℝ s) : (TorchLean.Tensor.full s 0).addSpec t = t

Left identity for addSpec: adding the all-zero tensor does nothing.

@[simp]

theorem Spec.add_spec_zero_right {s : Shape} (t : TorchLean.Tensor ℝ s) : t.addSpec (TorchLean.Tensor.full s 0) = t

Right identity for addSpec: adding the all-zero tensor does nothing.

@[simp]

theorem Spec.mul_spec_one_left {s : Shape} (t : TorchLean.Tensor ℝ s) : (TorchLean.Tensor.full s 1).mulSpec t = t

Left identity for mulSpec: multiplying by the all-ones tensor does nothing.

@[simp]

theorem Spec.mul_spec_one_right {s : Shape} (t : TorchLean.Tensor ℝ s) : t.mulSpec (TorchLean.Tensor.full s 1) = t

Right identity for mulSpec: multiplying by the all-ones tensor does nothing.

theorem Spec.foldl_add_scalar {ι : Type} (values : ι → TorchLean.Tensor ℝ Shape.scalar) (items : List ι) (initial : ℝ) : List.foldl (fun (total : TorchLean.Tensor ℝ Shape.scalar) (item : ι) => total + values item) (TorchLean.Tensor.scalar initial) items = TorchLean.Tensor.scalar (List.foldl (fun (total : ℝ) (item : ι) => total + (values item).item) initial items)

Adding scalar tensors in a left fold agrees with folding their scalar values.