TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.Tensor.Algebra

Tensor algebra proofs #

Backend-generic algebraic lemmas for TorchLean's single packed tensor type. Proofs observe tensors through item, unstack, and typed indexing; they do not depend on the physical buffer selected by Storage.

source
def Proofs.TensorAlgebra.dot {α : Type} [TorchLean.Storage α] [Zero α] [Add α] [Mul α] {shape : Spec.Shape} :
TorchLean.Tensor α shape → TorchLean.Tensor α shape → α

Multiply matching scalar entries and add them in row-major shape order.

Instances For

    Dot-product algebra #

    source
    @[simp]
    theorem Proofs.TensorAlgebra.dot_scalar {α : Type} [TorchLean.Storage α] [CommSemiring α] (a b : α) :
    dot (TorchLean.Tensor.scalar a) (TorchLean.Tensor.scalar b) = a * b

    The dot product of two scalars is their product: the base case of the recursion.

    source
    theorem Proofs.TensorAlgebra.dot_scale_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (left right : TorchLean.Tensor α s) (scalar : α) :
    dot left (right.scaleSpec scalar) = dot left right * scalar

    Dot is multiplicative with scalar scaling in its right argument.

    source
    theorem Proofs.TensorAlgebra.dot_comm {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (left right : TorchLean.Tensor α s) :
    dot left right = dot right left

    Dot is symmetric over a commutative semiring.

    source
    theorem Proofs.TensorAlgebra.dot_scale_left {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (left right : TorchLean.Tensor α s) (scalar : α) :
    dot (left.scaleSpec scalar) right = dot left right * scalar

    Dot is multiplicative with scalar scaling in its left argument.

    source
    theorem Proofs.TensorAlgebra.dot_add_left {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (left middle right : TorchLean.Tensor α s) :
    dot (left.addSpec middle) right = dot left right + dot middle right

    Dot distributes over addition in its left argument.

    source
    theorem Proofs.TensorAlgebra.dot_add_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (left middle right : TorchLean.Tensor α s) :
    dot left (middle.addSpec right) = dot left middle + dot left right

    Dot distributes over addition in its right argument.

    source
    theorem Proofs.TensorAlgebra.dot_full_zero_right {α : Type} [TorchLean.Storage α] [CommSemiring α] {s : Spec.Shape} (tensor : TorchLean.Tensor α s) :
    dot tensor (TorchLean.Tensor.full s 0) = 0

    The dot product with an all-zero tensor is zero.

    source
    theorem Proofs.TensorAlgebra.dot_vec_eq_sum {α : Type} [TorchLean.Storage α] [CommSemiring α] {n : ℕ} (a b : TorchLean.Tensor α [n]) :
    dot a b = ∑ index : Fin n, a.getScalar index * b.getScalar index

    Vector dot is the ordinary finite sum of matching scalar coordinates.

    Indexing and matrix/vector bridges #

    source
    theorem Proofs.TensorAlgebra.get2_eq {α : Type} [TorchLean.Storage α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (i : Fin m) (j : Fin n) :
    Spec.get2 A i j = ((A.unstack i).unstack j).item

    Matrix indexing is two successive packed leading-axis selections.

    source
    theorem Proofs.TensorAlgebra.get_eq {α : Type} [TorchLean.Storage α] {m : ℕ} {shape : Spec.Shape} (t : TorchLean.Tensor α (Spec.Shape.dim m shape)) (i : Fin m) :
    Spec.get t i = t.unstack i

    Spec.get is the public spelling of packed leading-axis selection.

    source
    theorem Proofs.TensorAlgebra.getScalar_mat_vec_mul_spec {α : Type} [TorchLean.Storage α] [CommSemiring α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (v : TorchLean.Tensor α [n]) (i : Fin m) :
    (Spec.matVecMulSpec A v).getScalar i = ∑ k : Fin n, Spec.get2 A i k * v.getScalar k

    Coordinate expansion of matrix-vector multiplication.

    source
    theorem Proofs.TensorAlgebra.getScalar_vec_mat_mul_spec {α : Type} [TorchLean.Storage α] [CommSemiring α] {m n : ℕ} (v : TorchLean.Tensor α [m]) (A : TorchLean.Tensor α [m, n]) (j : Fin n) :
    (Spec.vecMatMulSpec v A).getScalar j = ∑ i : Fin m, v.getScalar i * Spec.get2 A i j

    Coordinate expansion of vector-matrix multiplication.

    source
    theorem Proofs.TensorAlgebra.dot_mat_linear_adjoint {α : Type} [TorchLean.Storage α] [CommSemiring α] {inDim outDim : ℕ} (W : TorchLean.Tensor α [outDim, inDim]) (dLdy : TorchLean.Tensor α [outDim]) (dx : TorchLean.Tensor α [inDim]) :
    dot dLdy (Spec.matVecMulSpec W dx) = dot (Spec.vecMatMulSpec dLdy W) dx

    Matrix-vector and vector-matrix multiplication are adjoint under dot.