Tensor Algebra Lemmas

This file collects foundational algebraic lemmas for Spec.Tensor: extensionality, map/fold rewrites, and pointwise arithmetic facts used throughout the autograd and runtime-correctness proof stack.

theorem Spec.tensor_ext {α : Type} {s : Shape} {x y : Tensor α s} : (∀ (idxs : List ℕ), getSpec x idxs = getSpec y idxs) → x = y

Tensor extensionality over a generic element type: equal getSpec views imply equal tensors.

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

Elementwise addition is associative (over ℝ tensors).

theorem Spec.sub_spec_add_right {s : Shape} (a b c : 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 : 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 : 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 : 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 : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (x y : Tensor ℝ (Shape.dim n Shape.scalar)) : 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 : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (x : Tensor ℝ (Shape.dim n Shape.scalar)) (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 : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (x y : Tensor ℝ (Shape.dim n Shape.scalar)) (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.get_dim_scalar {n : ℕ} (f : Fin n → Tensor ℝ Shape.scalar) (i : Fin n) : get (Tensor.dim f) i = f i

Simplification lemmas for common patterns. Useful for automated proof tactics.

theorem Spec.option_zero_add (o : Option ℝ) : Option.map (fun (x : ℝ) => 0 + x) o = o

Mapping 0 + · over an Option is the identity.

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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