TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.Tensor.Basic.Core

Tensor Coordinate and Shape Bridges #

Coordinate formulas for real vector addition and scaling, together with row-major flattening and constant-tensor reshape rules for any storage scalar. Shape.Coord.equivFin identifies shaped coordinates with flat indices, including empty shapes with a zero-length dimension.

The generic matrix/vector indexing helpers are re-exported from NN.Proofs.Tensor.Algebra into Spec. General fold lemmas retain their canonical List names.

The shape conventions match PyTorch flatten and reshape. Spec.Shape.size corresponds to numel.

Vector coordinates #

source
theorem Spec.getScalar_add_spec {n : ℕ} (x y : TorchLean.Tensor ℝ [n]) :
(x.addSpec y).getScalar = fun (i : Fin n) => x.getScalar i + y.getScalar i

getScalar distributes over pointwise addition (addSpec).

source
theorem Spec.getScalar_scale_spec {n : ℕ} (x : TorchLean.Tensor ℝ [n]) (c : ℝ) :
(x.scaleSpec c).getScalar = fun (i : Fin n) => x.getScalar i * c

getScalar distributes over pointwise scaling (scaleSpec).

source
def Spec.Shape.Coord.equivFin (s : Shape) :
s.Coord ≃ Fin s.size

Row-major equivalence between the coordinates of a shape and flat indices. Its forward map is Shape.Coord.linearize and its inverse is Shape.Coord.unlinearize.

Instances For
    source
    theorem Spec.Shape.Coord.equivFin_apply {s : Shape} (c : s.Coord) :
    (equivFin s) c = c.linearize

    The forward map of Shape.Coord.equivFin is row-major linearization.

    source
    theorem Spec.getScalar_flattenSpec_linearize {α : Type} [TorchLean.Storage α] {s : Shape} (x : TorchLean.Tensor α s) (c : s.Coord) :
    x.flattenSpec.getScalar c.linearize = TorchLean.Tensor.Internal.Rep.get x c

    Reading a flattened tensor at the row-major position of a coordinate returns that entry.

    source
    theorem Spec.getScalar_flattenSpec {α : Type} [TorchLean.Storage α] {shape : Shape} (tensor : TorchLean.Tensor α shape) (index : Fin shape.size) :
    tensor.flattenSpec.getScalar index = TorchLean.Tensor.Internal.Rep.get tensor (((TorchLean.Tensor.Internal.Coord.equivFin shape).trans (finCongr ⋯)).symm index)

    A scalar in the flattened tensor is read at its row-major shaped coordinate.

    source
    theorem Spec.reshapeSpec_full {α : Type} [TorchLean.Storage α] {s t : Shape} (a : α) (h : s.size = t.size) :
    (TorchLean.Tensor.full s a).reshapeSpec h = TorchLean.Tensor.full t a

    A shape change preserves a constant tensor's fill value.