Inner products under axis permutations

Moving an axis changes the order of a tensor's coordinates. It leaves the sum of coordinate products unchanged. These identities apply at every rank, including shapes with empty axes, and let a rowwise adjoint calculation pass through the permutations used by softmax.

theorem Proofs.dot_eq_sum_unstack {n : ℕ} {s : Spec.Shape} (x y : TorchLean.Tensor ℝ (Spec.Shape.dim n s)) : Spec.dot x y = ∑ i : Fin n, Spec.dot (x.unstack i) (y.unstack i)

A tensor inner product is the sum of the inner products of its leading slices.

theorem Proofs.dot_cast_shape {s t : Spec.Shape} (h : s = t) (x y : TorchLean.Tensor ℝ s) : Spec.dot (h ▸ x) (h ▸ y) = Spec.dot x y

Transporting both tensors through the same shape equality preserves their inner product.

theorem Proofs.dot_swapAdjacentAxes {s : Spec.Shape} (x y : TorchLean.Tensor ℝ s) (depth : ℕ) : Spec.dot (x.swapAdjacentAxes depth) (y.swapAdjacentAxes depth) = Spec.dot x y

Exchanging adjacent axes preserves the inner product at any depth.

theorem Proofs.dot_permuteByAdjacentSwaps {s : Spec.Shape} (x y : TorchLean.Tensor ℝ s) (swaps : List ℕ) : Spec.dot (x.permuteByAdjacentSwaps swaps) (y.permuteByAdjacentSwaps swaps) = Spec.dot x y

A sequence of adjacent swaps preserves the inner product, without a rank restriction.