Tensor constructors (spec layer)

These are small, total constructors for building TorchLean.Tensor values directly.

They are used heavily inside the spec layer (models/layers) and in proofs, where we want:

• straightforward definitional unfolding, and
• no dependence on IO or dynamic shape checks.

For ordinary literals, in-memory conversion, reshape, and scalar casts, import NN.Tensor.

Design choice (why these are "total"):

• In the spec layer we would rather make edge cases explicit than throw runtime exceptions.
• If something is shape-invalid, we want Lean to reject it at elaboration time.
• Existing in-memory collections enter through the total Tensor.from conversion boundary.
• External parsers validate untrusted dimensions before constructing a tensor.

Constant tensors

def TorchLean.Tensor.full {α : Type} [Storage α] (shape : Spec.Shape) (value : α) : Tensor α shape

Fill a tensor of arbitrary shape with one value.

PyTorch analogy: torch.full(shape, value).

@[reducible, inline]

abbrev TorchLean.Tensor.zeros {α : Type} [Storage α] [Zero α] (shape : Spec.Shape) : Tensor α shape

Construct an all-zero tensor of arbitrary shape. Reducible, so lemmas about full apply.

@[reducible, inline]

abbrev TorchLean.Tensor.ones {α : Type} [Storage α] [One α] (shape : Spec.Shape) : Tensor α shape

Construct an all-one tensor of arbitrary shape. Reducible, so lemmas about full apply.

@[simp]

theorem TorchLean.Tensor.full_apply {α : Type} [Storage α] (shape : Spec.Shape) (value : α) (coordinate : shape.Coord) : Internal.Rep.get (full shape value) coordinate = value

Every coordinate of a filled tensor contains its fill value.

@[simp]

theorem TorchLean.Tensor.item_full_scalar {α : Type} [Storage α] (value : α) : (full Spec.Shape.scalar value).item = value

Reading a scalar filled tensor returns its fill value.

@[simp]

theorem TorchLean.Tensor.item_rep_const {α : Type} [Storage α] (value : α) : item (Internal.Rep.const value) = value

The item of an internally constant scalar tensor is the constant.

@[simp]

theorem TorchLean.Tensor.getScalar_rep_const {α : Type} [Storage α] {n : ℕ} (value : α) (i : Fin n) : getScalar (Internal.Rep.const value) i = value

Every entry of an internally constant vector is the constant.

@[simp]

theorem TorchLean.Tensor.replicate_scalar_apply {α : Type} [Storage α] (value : α) (shape : Spec.Shape) (coordinate : shape.Coord) : Internal.Rep.get (Spec.replicate (scalar value)) coordinate = value

Replicating a scalar tensor observes that scalar at every target coordinate.

@[simp]

theorem Spec.get_full {α : Type} [TorchLean.Storage α] (n : ℕ) (s : Shape) (value : α) (i : Fin n) : get (TorchLean.Tensor.full (Shape.dim n s) value) i = TorchLean.Tensor.full s value

Every outer coordinate of a filled tensor is the corresponding filled subtensor.

@[simp]

theorem Spec.get2_full {α : Type} [TorchLean.Storage α] (m n : ℕ) (value : α) (i : Fin m) (j : Fin n) : get2 (TorchLean.Tensor.full (Shape.dim m (Shape.dim n Shape.scalar)) value) i j = value

Every coordinate of a filled matrix contains its fill value.

def TorchLean.Tensor.generate {α : Type} [Storage α] (shape : Spec.Shape) (f : List ℕ → α) : Tensor α shape

Construct an arbitrary-rank tensor from a coordinate function.

At each coordinate, f receives one natural-number index per dimension, outermost first. The indices are in bounds by construction.

For example, Tensor.generate [2, 3] f has shape [2, 3], and its entry at row i and column j is f [i, j].

def TorchLean.Tensor.ofFn {α : Type} [Storage α] {n : ℕ} (values : Fin n → α) : Tensor α [n]

The buffer is filled directly from the index function, without building one scalar tensor per entry.

PyTorch analogy: torch.tensor([...]) with shape (n,), but our input is a function, not a list.

Example:

-- `torch.tensor([0.0, 1.0, 2.0, 3.0])`, except the entries arrive from a function on `Fin n` and
-- the length is part of the type.
def ramp : Tensor Float [4] := Tensor.ofFn fun index => index.val.toFloat

@[simp]

theorem TorchLean.Tensor.ofFn_apply {α : Type} [Storage α] {n : ℕ} (values : Fin n → α) (coordinate : Spec.Shape.Coord [n]) : Internal.Rep.get (ofFn values) coordinate = values coordinate.1

Evaluating ofFn at a coordinate returns the value supplied at its index.

@[simp]

theorem TorchLean.Tensor.unstack_ofFn {α : Type} [Storage α] {n : ℕ} (values : Fin n → α) (i : Fin n) : (ofFn values).unstack i = scalar (values i)

Every entry of ofFn is the scalar tensor of the supplied value.

@[simp]

theorem TorchLean.Tensor.getScalar_rep_ofFn {α : Type} [Storage α] {n : ℕ} (values : Spec.Shape.Coord [n] → α) (i : Fin n) : getScalar (Internal.Rep.ofFn values) i = values (i, PUnit.unit)

Reading a scalar entry of an internally generated vector evaluates the generator.

@[simp]

theorem TorchLean.Tensor.item_rep_ofFn {α : Type} [Storage α] (values : Spec.Shape.scalar.Coord → α) : item (Internal.Rep.ofFn values) = values PUnit.unit

The item of an internally generated scalar tensor is the generator's value.

@[simp]

theorem TorchLean.Tensor.unstack_rep_ofFn {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (values : (Spec.Shape.dim n shape).Coord → α) (i : Fin n) : unstack (Internal.Rep.ofFn values) i = Internal.Rep.ofFn fun (coordinate : Internal.Coord shape) => values (i, coordinate)

Slicing an internally generated tensor fixes the leading coordinate of the generator.

theorem TorchLean.Tensor.ofFn_eq_dim_scalar {α : Type} [Storage α] {n : ℕ} (values : Fin n → α) : ofFn values = dim fun (i : Fin n) => scalar (values i)

ofFn is extensionally the stack of its scalar entries.

@[simp]

theorem TorchLean.Tensor.getScalar_ofFn {α : Type} [Storage α] {n : ℕ} (values : Fin n → α) (i : Fin n) : (ofFn values).getScalar i = values i

Reading a coordinate from ofFn returns the value supplied at that coordinate.

@[simp]

theorem TorchLean.Tensor.ofFn_getScalar {α : Type} [Storage α] {n : ℕ} (t : Tensor α [n]) : (ofFn fun (i : Fin n) => t.getScalar i) = t

Rebuilding a vector from all of its coordinates returns the original vector.

def TorchLean.Tensor.matrix {α : Type} [Storage α] {m n : ℕ} (values : Fin m → Fin n → α) : Tensor α [m, n]

Construct a matrix from its row and column coordinate function.

PyTorch analogy: torch.tensor([...]).reshape(m, n) (again, function input rather than a list).

@[simp]

theorem TorchLean.Tensor.getScalar_full {α : Type} [Storage α] (n : ℕ) (value : α) (i : Fin n) : (full (Spec.Shape.dim n Spec.Shape.scalar) value).getScalar i = value

Every coordinate of a filled vector contains the fill value.

def Spec.singleton {α : Type} [TorchLean.Storage α] (x : α) : TorchLean.Tensor α [1]

A singleton vector.

PyTorch analogy: x.unsqueeze(0) for a scalar x.

def Spec.padLeft {α : Type} [TorchLean.Storage α] {n : ℕ} {s : Shape} (x : TorchLean.Tensor α s) : TorchLean.Tensor α (Shape.padLeft n s)

Pad a tensor with n leading dimensions of size 1.

This is the tensor-level companion of Shape.padLeft. The row-major buffer is unchanged, so the padding is a zero-copy reinterpretation of the static shape. Broadcasting uses it to align ranks before expanding singleton axes.

PyTorch analogy: repeated unsqueeze(0).

@[simp]

theorem Spec.padLeft_zero {α : Type} [TorchLean.Storage α] {s : Shape} (x : TorchLean.Tensor α s) : padLeft x = x

Padding with zero axes is the identity.

theorem Spec.padLeft_succ {α : Type} [TorchLean.Storage α] {n : ℕ} {s : Shape} (x : TorchLean.Tensor α s) : padLeft x = TorchLean.Tensor.dim fun (x_1 : Fin 1) => padLeft x

Padding one more axis stacks the padded tensor along a new singleton axis.

def TorchLean.Tensor.stackArray {α : Type} [Storage α] {n : ℕ} {s : Spec.Shape} (xs : Array (Tensor α s)) (_h : n = xs.size) : Tensor α (Spec.Shape.dim n s)

Stack an array of equal-shaped tensors along a new leading dimension.

The explicit size proof prevents silent truncation or padding. Taking tensors as array elements makes this constructor independent of rank: use scalar tensors for a vector, vectors for a matrix, or arbitrary inner tensors for higher-rank values.

theorem TorchLean.Tensor.forall_full {α : Type} [Storage α] {p : α → Prop} {s : Spec.Shape} {x : α} (hx : p x) : Forall p (full s x)

A filled tensor satisfies every pointwise property satisfied by its value.

def Spec.matrixFromRows? {α : Type} [TorchLean.Storage α] (rows : List (List α)) : Option (TorchLean.Tensor α [rows.length, (Option.map List.length rows.head?).getD 0])

Build a matrix when every row has the same length; reject ragged input.