Shape-changing tensor operations

Flatten, unflatten, and reshape preserve the row-major scalar sequence. Since TorchLean.Tensor owns a contiguous certified buffer, these operations are zero-copy changes to the static shape proof.

theorem TorchLean.Tensor.size_toList_flatten (shape : Spec.Shape) : Internal.Shape.size shape.toList = Internal.Shape.size [shape.size]

The buffer and specification size functions agree on the flattened shape.

theorem TorchLean.Tensor.reshapeCoordEquiv_linearize_val {source target : Internal.Shape} (hSize : source.size = target.size) (coordinate : Internal.Coord target) : ↑((Internal.Rep.reshapeCoordEquiv hSize) coordinate).linearize = ↑coordinate.linearize

A reshape changes coordinates without changing their row-major index.

theorem TorchLean.Tensor.vectorCoordinate_linearize_val {n : ℕ} (index : Fin n) : ↑(Internal.Coord.linearize (index, PUnit.unit)) = ↑index

A one-axis coordinate linearizes to its sole finite index.

def TorchLean.Tensor.reverseAxis {α : Type} [Storage α] (axis : ℕ) {shape : Spec.Shape} : Tensor α shape → [_h : Spec.Shape.AxisInBounds axis shape] → Tensor α shape

Reverse the coordinates of an arbitrary statically valid axis.

def TorchLean.Tensor.flattenSpec {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) : Tensor α [shape.size]

Flatten a tensor into a one-dimensional row-major vector.

Execution reuses the original native buffer; only the certified static shape changes.

def TorchLean.Tensor.unflattenSpec {α : Type} [Storage α] (shape : Spec.Shape) (tensor : Tensor α [shape.size]) : Tensor α shape

Restore a row-major vector to a specified shape with the same element count.

Execution reuses the vector's native buffer.

theorem TorchLean.Tensor.ShapeChange.Internal.flattenSpec_dim_apply {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (values : Fin n → Tensor α shape) (outer : Fin n) (inner : Fin shape.size) (hIndex : ↑outer * shape.size + ↑inner < (Spec.Shape.dim n shape).size) : (dim values).flattenSpec.getScalar ⟨↑outer * shape.size + ↑inner, hIndex⟩ = (values outer).flattenSpec.getScalar inner

Flattening an outer dimension places each flattened slice in one contiguous row-major segment.

@[simp]

theorem TorchLean.Tensor.unflattenSpec_flattenSpec {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) : unflattenSpec shape tensor.flattenSpec = tensor

Unflattening a flattened tensor returns the original tensor.

@[simp]

theorem TorchLean.Tensor.flattenSpec_unflattenSpec {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α [shape.size]) : (unflattenSpec shape tensor).flattenSpec = tensor

Flattening an unflattened vector returns the original vector.

def TorchLean.Tensor.reshapeSpec {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (hSize : source.size = target.size) : Tensor α target

Reshape a tensor while preserving its row-major scalar sequence.

theorem TorchLean.Tensor.flatten_reshapeSpec {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (hSize : source.size = target.size) : (tensor.reshapeSpec hSize).flattenSpec = hSize ▸ tensor.flattenSpec

Flattening a reshape returns the original flat data, transported by the size equality.

@[simp]

theorem TorchLean.Tensor.reshapeSpec_roundtrip {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (hSize : source.size = target.size) : (tensor.reshapeSpec hSize).reshapeSpec ⋯ = tensor

Reshaping to an equal-size shape and back preserves every tensor entry.

def TorchLean.Tensor.sequenceFin {α : Type} [Storage α] {shape : Spec.Shape} {n : ℕ} (values : Fin n → Option (Tensor α shape)) : Option (Tensor α (Spec.Shape.dim n shape))

Collect optional tensor slices along a new leading axis.

Slices are evaluated once, in index order. A missing slice makes the whole result none; an empty family gives an empty tensor. The intermediate vector retains each successful slice so that the output can be assembled in one pass. Rebuilding the remaining tensor at every recursive step would copy earlier results repeatedly, making large batches and mixture models unnecessarily expensive.