Fold and reduction lemmas for dependent tensors.

This module packages the algebra needed to reason about tensor reductions, finite sums, and shape-indexed traversals.

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

Elementwise multiplication is associative (mul_spec is pointwise (*)).

theorem Spec.mul_spec_comm {s : Shape} (a b : Tensor ℝ s) : a.mulSpec b = b.mulSpec a

Elementwise multiplication is commutative (mul_spec is pointwise (*)).

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

Elementwise addition is commutative (add_spec is pointwise (+)).

theorem Spec.mul_spec_fill_zero {s : Shape} : (fill 0 s).mulSpec (fill 0 s) = fill 0 s

Elementwise multiplication of two all-zero tensors is the all-zero tensor.

Real dot product and fold bridges

noncomputable def Spec.dot {s : Shape} (a b : Tensor ℝ s) : ℝ

Real dot product for same-shape tensors, defined as the sum of elementwise products.

This matches the common PyTorch idiom (a * b).sum() for same-shape tensors. Citations: https://pytorch.org/docs/stable/generated/torch.sum.html

This is the Spec-namespace dot product used by real-analysis proofs. The backend-generic recursive dot product is Proofs.TensorAlgebra.dot.

theorem Spec.tensor_foldl_spec_go_of_lt {α β : Type} (f : β → α → β) {n : ℕ} {s : Shape} (values : Fin n → Tensor α s) {k : ℕ} (acc : β) (hk : k < n) : Tensor.tensorFoldlSpec.go f n s values k acc = Tensor.tensorFoldlSpec.go f n s values (k + 1) (Tensor.tensorFoldlSpec f acc (values ⟨k, hk⟩))

One-step unfolding of the internal tail-recursive helper tensor_foldl_spec.go when the loop condition holds (k < n).

This lemma is a proof tool: it lets proofs peel one loop step without using unfold directly.

theorem Spec.tensor_foldl_spec_go_of_not_lt {α β : Type} (f : β → α → β) {n : ℕ} {s : Shape} (values : Fin n → Tensor α s) {k : ℕ} (acc : β) (hk : ¬k < n) : Tensor.tensorFoldlSpec.go f n s values k acc = acc

One-step unfolding of the internal tail-recursive helper tensor_foldl_spec.go when the loop condition fails (¬ k < n), i.e. the loop terminates and returns the accumulator.

theorem Spec.tensor_foldl_spec_add_init {s : Shape} (acc : ℝ) (t : Tensor ℝ s) : Tensor.tensorFoldlSpec (fun (x1 x2 : ℝ) => x1 + x2) acc t = acc + t.sumSpec

Accumulator lemma for tensor_foldl_spec specialized to addition.

Informally: folding with (+) over a tensor adds sum_spec t to the initial accumulator. This is frequently used to move between “fold-style” specs and “sum-style” algebra.

theorem Spec.dot_mul_reassoc {s : Shape} (dLdy m dx : Tensor ℝ s) : dot dLdy (m.mulSpec dx) = dot (m.mulSpec dLdy) dx

Reassociate a dot over a pointwise product, using commutativity/associativity of mul_spec.

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

Unfolding lemma for get2 (2D tensor indexing).

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

Unfolding lemma for get on a Tensor.dim value.

theorem Spec.toVec_mat_vec_mul_spec {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (v : Tensor ℝ (Shape.dim n Shape.scalar)) (i : Fin m) : toVec (matVecMulSpec A v) i = ∑ k : Fin n, get2 A i k * toVec v k

Coordinate formula for mat_vec_mul_spec, converted from the spec's List.finRange fold to a Finset.univ.sum.

This is the “PyTorch-looking” statement of matvec: each output entry is a dot product of the corresponding row with the input vector.

theorem Spec.get2_mat_mul_spec {m n p : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (B : Tensor ℝ (Shape.dim n (Shape.dim p Shape.scalar))) (i : Fin m) (j : Fin p) : get2 (matMulSpec A B) i j = ∑ k : Fin n, get2 A i k * get2 B k j

Coordinate formula for mat_mul_spec (matrix-matrix multiplication).

This is the standard triple-sum identity: (A @ B)[i,j] = ∑ k, A[i,k] * B[k,j], matching the textbook/PyTorch view of matrix multiplication.

Citations: https://pytorch.org/docs/stable/generated/torch.matmul.html

theorem Spec.sum_spec_dim {n : ℕ} {s : Shape} (t : Tensor ℝ (Shape.dim n s)) : t.sumSpec = ∑ i : Fin n, (get t i).sumSpec

Sum over the outer dimension unfolds into a Finset.univ sum of inner sum_spec.

This is the tensor analogue of torch.sum reducing over a leading dimension.

theorem Spec.dot_eq_tensorAlgebra_dot {s : Shape} (a b : Tensor ℝ s) : dot a b = Proofs.TensorAlgebra.dot a b

The real-analysis Spec.dot agrees with the backend-generic recursive dot.

Spec.dot is defined as sumSpec (mulSpec a b), which is the proof-facing version of the PyTorch idiom (a * b).sum(). Proofs.TensorAlgebra.dot is recursive over the tensor shape so it works over arbitrary semiring-like scalar models. This bridge lets real proofs reuse generic algebra instead of repeating finite-sum rearrangements.