Core tensor datatype (TorchLean.Tensor)

TorchLean has one shape-indexed tensor representation for proofs and execution: Tensor α shape.

Every tensor owns one contiguous row-major buffer. The scalar type selects the physical buffer through Storage: arbitrary proof scalar types such as Real use Array, while executable types with specialized instances use packed storage (FloatArray for Float, ByteArray for UInt8).

The scalar and dim functions preserve TorchLean's proof-facing construction API. They are smart constructors over packed storage, not physical recursive constructors. Proofs eliminate tensors through typed lookup, scalarEquiv, dimEquiv, and extensionality.

@[reducible, inline]

abbrev TorchLean.Tensor (α : Type) (shape : Spec.Shape) [Storage α] : Type

The single tensor representation used by TorchLean proofs and execution.

The public shape is Spec.Shape, which is the same type as the shape carried by the buffer, so this alias only reorders arguments. The implementation is one certified contiguous row-major buffer selected by Storage.

def TorchLean.delabTensorRep : Lean.PrettyPrinter.Delaborator.Delab

Render executable internal tensors with explicit dimensions through the canonical public type name in editor information and #check output.

Universe-polymorphic proof tensors and genuinely computed shape expressions retain their exact internal spelling.

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

Construct a rank-zero tensor from one scalar value.

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

Construct an outer dimension from its shape-indexed entries.

def TorchLean.Tensor.item {α : Type} [Storage α] (tensor : Tensor α Spec.Shape.scalar) : α

Return the value stored in a scalar tensor.

@[simp]

theorem TorchLean.Tensor.item_scalar {α : Type} [Storage α] (value : α) : (scalar value).item = value

Reading back the value a scalar tensor was built from returns that value.

@[simp]

theorem TorchLean.Tensor.scalar_apply {α : Type} [Storage α] (value : α) : Internal.Rep.get (scalar value) PUnit.unit = value

A scalar tensor evaluates to its sole scalar value.

def TorchLean.Tensor.unstack {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (tensor : Tensor α (Spec.Shape.dim n shape)) (index : Fin n) : Tensor α shape

Select one leading-axis slice from a tensor.

theorem TorchLean.Tensor.eq_of_data_eq {α : Type} [Storage α] {s : Spec.Shape} {a b : Tensor α s} (h : Internal.Rep.data a = Internal.Rep.data b) : a = b

Tensors with equal row-major data arrays are equal.

The packed representation is a storage buffer together with a size proof, and buffers are determined by their array observation (Storage.toArray_injective).

@[simp]

theorem TorchLean.Tensor.unstack_dim {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (values : Fin n → Tensor α shape) (index : Fin n) : (dim values).unstack index = values index

Slicing the outer axis of a stacked tensor returns the slice that was stacked.

@[simp]

theorem TorchLean.Tensor.dim_unstack {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (tensor : Tensor α (Spec.Shape.dim n shape)) : dim tensor.unstack = tensor

Restacking every slice of a tensor returns the tensor.

Together with unstack_dim this is what makes dim and unstack an isomorphism rather than merely a pair of functions, which is why proofs can eliminate a tensor by rw [← dim_unstack] and then reason slice by slice.

def TorchLean.Tensor.default {α : Type} [Storage α] [Inhabited α] {shape : Spec.Shape} : Tensor α shape

Default tensor value for any shape.

@[reducible]

instance TorchLean.Tensor.inhabited {α : Type} [Storage α] [Inhabited α] {shape : Spec.Shape} : Inhabited (Tensor α shape)

Every shape is inhabited when the scalar type is: take the all-default tensor.

@[simp]

theorem TorchLean.Tensor.scalar_item {α : Type} [Storage α] (tensor : Tensor α Spec.Shape.scalar) : scalar tensor.item = tensor

Rebuilding a scalar tensor from its item returns the original tensor.

theorem TorchLean.Tensor.ext_scalar {α : Type} [Storage α] {left right : Tensor α Spec.Shape.scalar} (h : left.item = right.item) : left = right

Two scalar tensors agreeing on their item are equal.

theorem TorchLean.Tensor.ext_scalar_iff {α : Type} [Storage α] {left right : Tensor α Spec.Shape.scalar} : left = right ↔ left.item = right.item

def TorchLean.Tensor.scalarEquiv (α : Type) [Storage α] : Tensor α Spec.Shape.scalar ≃ α

Scalar tensors and scalar values are equivalent.

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

An outer axis is equivalent to a finite family of inner tensors.

inductive TorchLean.Tensor.View (α : Type) [Storage α] : Spec.Shape → Type

Proof-facing eliminator for the familiar scalar/dimension cases.

View does not own tensor data and is not a second tensor representation. It only exposes the outer shape of an already packed tensor.

• scalar {α : Type} [Storage α] (value : α) : View α Spec.Shape.scalar
• dim {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (values : Fin n → Tensor α shape) : View α (Spec.Shape.dim n shape)

def TorchLean.Tensor.view {α : Type} [Storage α] {shape : Spec.Shape} : Tensor α shape → View α shape

Observe the outer constructor of a packed tensor for shape-recursive proofs.

Pointwise algebra

Every algebraic operation on tensors is the corresponding scalar operation applied coordinatewise. The instances (Zero, Add, Neg, Sub, SMul, AddCommMonoid, AddCommGroup, Module) live on the native representation in NN.Tensor.Internal.Representation.Basic.Pointwise, so they apply uniformly to Tensor α shape whether the shape is a variable or a literal such as [n]. The coordinate lemmas below are the simp normal forms; add_apply is restated here under the public tensor namespace.

@[simp]

theorem TorchLean.Tensor.add_apply {α : Type} [Storage α] [Add α] {shape : Spec.Shape} (x y : Tensor α shape) (i : shape.Coord) : Internal.Rep.get (x + y) i = Internal.Rep.get x i + Internal.Rep.get y i

Tensor addition is coordinatewise scalar addition.

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

Vectors and finite scalar functions are equivalent.

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

Cast a tensor along an equality of shapes.

@[simp]

theorem TorchLean.Tensor.cast_shape_rfl {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) : tensor.castShape ⋯ = tensor

Casting along rfl is the identity, and holds by rfl itself.

@[simp]

theorem TorchLean.Tensor.cast_shape_self {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) (h : shape = shape) : tensor.castShape h = tensor

Casting along any proof of shape = shape is the identity.

cast_shape_rfl does not cover this: after Shape.ofList normalization the proof in hand is often some derived term rather than the literal rfl, and simp needs to discharge those too.

@[simp]

theorem TorchLean.Tensor.cast_shape_trans {α : Type} [Storage α] {s₁ s₂ s₃ : Spec.Shape} (tensor : Tensor α s₁) (h₁₂ : s₁ = s₂) (h₂₃ : s₂ = s₃) : (tensor.castShape h₁₂).castShape h₂₃ = tensor.castShape ⋯

Two casts in a row collapse into one along the composed equality.

theorem TorchLean.Tensor.cast_shape_proof_irrel {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) {p q : source = target} : tensor.castShape p = tensor.castShape q

The cast does not depend on which proof of the shape equality is used.

Shape equalities are proofs in a subsingleton, so this is provable rather than an axiom, and it is what lets two developments that derived the same equality differently share a lemma.

theorem TorchLean.Tensor.eqRec_eq_cast_shape {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) (h : source = target) : h ▸ tensor = tensor.castShape h

The ▸ rewrite and castShape are the same function.

Lean inserts ▸ on its own when a shape is rewritten in a tactic block, so without this bridge the castShape simp set would silently fail to fire on goals the elaborator produced.

theorem TorchLean.Tensor.eqRec_proof_irrel {α : Type} [Storage α] {source target : Spec.Shape} (tensor : Tensor α source) {p q : source = target} : p ▸ tensor = q ▸ tensor

cast_shape_proof_irrel in ▸ form, for goals the elaborator produced.

def Spec.shapeOf {α : Type} [TorchLean.Storage α] {shape : Shape} : TorchLean.Tensor α shape → Shape

Recover the statically known shape from a tensor value.

Indexing

def Spec.getSpec {α : Type} [TorchLean.Storage α] {shape : Shape} (tensor : TorchLean.Tensor α shape) (indices : List ℕ) : Option α

Try to read a scalar using a runtime list of coordinates.

@[simp]

theorem Spec.get_spec_scalar_nil {α : Type} [TorchLean.Storage α] (tensor : TorchLean.Tensor α (Shape.ofList [])) : getSpec tensor [] = some tensor.item

The empty coordinate list reads the item of a rank-zero tensor.

@[simp]

theorem Spec.get_spec_scalar_cons {α : Type} [TorchLean.Storage α] (tensor : TorchLean.Tensor α (Shape.ofList [])) (index : ℕ) (indices : List ℕ) : getSpec tensor (index :: indices) = none

A rank-zero tensor has no axis to index, so any nonempty coordinate list fails.

@[simp]

theorem Spec.get_spec_dim_nil {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) : getSpec tensor [] = none

A tensor with an axis is not a scalar, so the empty coordinate list fails.

@[simp]

theorem Spec.get_spec_dim_cons {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) (index : ℕ) (indices : List ℕ) : getSpec tensor (index :: indices) = if h : index < n then getSpec (tensor.unstack ⟨index, h⟩) indices else none

One step of runtime lookup: check the leading index against the axis, then recurse into the slice. This is the equation that turns getSpec on a literal coordinate list into a chain of unstacks, which is how the executable and proof-facing readings are kept in step.

@[simp]

theorem Spec.get_spec_castShape {α : Type} [TorchLean.Storage α] {source target : Shape} (tensor : TorchLean.Tensor α source) (h : source = target) (index : List ℕ) : getSpec (tensor.castShape h) index = getSpec tensor index

A shape cast does not move any data, so runtime lookup sees straight through it.

def TorchLean.Tensor.selectSpec {α : Type} [Storage α] (axis : ℕ) {shape : Spec.Shape} (tensor : Tensor α shape) [_h : Spec.Shape.AxisInBounds axis shape] : Fin (shape.axisSize axis) → Tensor α (shape.eraseAxis axis)

Select one coordinate along an arbitrary axis and remove that axis.

@[simp]

theorem TorchLean.Tensor.selectSpec_zero_dim {α : Type} [Storage α] {n : ℕ} {shape : Spec.Shape} (values : Fin n → Tensor α shape) (index : Fin n) : selectSpec 0 (dim values) index = values index

Selecting along axis zero is exactly the outer-axis slice.

def Spec.get {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) (index : Fin n) : TorchLean.Tensor α shape

Select one entry from the outermost tensor axis.

@[simp]

theorem Spec.get_dim {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (values : Fin n → TorchLean.Tensor α shape) (index : Fin n) : get (TorchLean.Tensor.dim values) index = values index

Indexing a stacked tensor returns the entry that was stacked.

@[instance_reducible, instance 10000]

instance Spec.instGetElemRepConsNatNilFinTrue {α : Type} [TorchLean.Storage α] {n : ℕ} : GetElem (TorchLean.Tensor α [n]) (Fin n) α fun (x : TorchLean.Tensor α [n]) (x_1 : Fin n) => True

Vector indexing returns a scalar directly.

This higher-priority instance also makes chained indexing natural: matrix[row][column] returns an entry, while the first lookup still returns the statically shaped row tensor.

@[instance_reducible]

instance Spec.instGetElemRepConsNatFinTensorOfListTrue {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : List ℕ} : GetElem (TorchLean.Tensor.Internal.Rep α (n :: shape)) (Fin n) (TorchLean.Tensor α (Shape.ofList shape)) fun (x : TorchLean.Tensor.Internal.Rep α (n :: shape)) (x_1 : Fin n) => True

@[instance_reducible, instance 10000]

instance Spec.instGetElemRepConsNatNilLt {α : Type} [TorchLean.Storage α] {n : ℕ} : GetElem (TorchLean.Tensor α [n]) ℕ α fun (x : TorchLean.Tensor α [n]) (index : ℕ) => index < n

Natural-number indexing of a vector returns one scalar and asks GetElem to discharge the static bound.

@[instance_reducible]

instance Spec.instGetElemRepConsNatTensorOfListLt {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : List ℕ} : GetElem (TorchLean.Tensor.Internal.Rep α (n :: shape)) ℕ (TorchLean.Tensor α (Shape.ofList shape)) fun (x : TorchLean.Tensor.Internal.Rep α (n :: shape)) (index : ℕ) => index < n

Natural-number indexing selects one slice along the outermost tensor axis.

Literal indices are checked during elaboration, so ordinary code can write matrix[0] without constructing a Fin value explicitly.

theorem TorchLean.Tensor.ext_getSpec {α : Type} [Storage α] {shape : Spec.Shape} {left right : Tensor α shape} (h : ∀ (index : List ℕ), Spec.getSpec left index = Spec.getSpec right index) : left = right

Runtime-list lookup is extensional.

theorem TorchLean.Tensor.ext_getSpec_iff {α : Type} [Storage α] {shape : Spec.Shape} {left right : Tensor α shape} : left = right ↔ ∀ (index : List ℕ), Spec.getSpec left index = Spec.getSpec right index

def TorchLean.Tensor.getScalar {α : Type} [Storage α] {n : ℕ} (tensor : Tensor α [n]) (index : Fin n) : α

Extract one scalar from a vector.

theorem TorchLean.Tensor.getScalar_eq_apply {α : Type} [Storage α] {n : ℕ} (tensor : Tensor α [n]) (index : Fin n) : tensor.getScalar index = Internal.Rep.get tensor (index, PUnit.unit)

Vector scalar lookup is ordinary coordinate evaluation.

@[inline]

def TorchLean.Tensor.Internal.getScalarDirect {α : Type} [Storage α] {n : ℕ} (tensor : Tensor α [n]) (index : Fin n) : α

Direct storage read used when compiling vector scalar lookup.

@[csimp]

theorem TorchLean.Tensor.getScalar_eq_getScalarDirect : @getScalar = @Internal.getScalarDirect

Compile scalar lookup without allocating the intermediate rank-zero slice.

@[simp]

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

Reading a vector filled by the packed constant constructor returns that constant.

@[simp]

theorem TorchLean.Tensor.getScalar_ofList {α : Type} [Storage α] (values : List α) (index : Fin values.length) : getScalar (Internal.Rep.ofList values) index = values.get index

Scalar lookup on a rank-one literal returns the corresponding source entry.

@[simp]

theorem TorchLean.Tensor.getScalar_dim_entry {α : Type} [Storage α] {n : ℕ} (values : Fin n → Tensor α Spec.Shape.scalar) (index : Fin n) : (dim values).getScalar index = (values index).item

Scalar lookup on a vector of scalar tensors reads the indexed entry.

@[simp]

theorem TorchLean.Tensor.vectorEquiv_apply {α : Type} [Storage α] {n : ℕ} (tensor : Tensor α [n]) (index : Fin n) : (vectorEquiv n) tensor index = tensor.getScalar index

The Tensor α [n] ≃ (Fin n → α) equivalence is scalar lookup on the nose.

Stating it keeps vectorEquiv usable in proofs without unfolding the two equivalences it is built from, and it is why a vector can be handed to Mathlib lemmas about functions on Fin n.

@[simp]

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

Building a vector from a function and reading it back returns the function.

theorem TorchLean.Tensor.ext_vector {α : Type} [Storage α] {n : ℕ} {left right : Tensor α [n]} (h : ∀ (index : Fin n), left.getScalar index = right.getScalar index) : left = right

Vectors agreeing at every scalar index are equal.

theorem TorchLean.Tensor.ext_vector_iff {α : Type} [Storage α] {n : ℕ} {left right : Tensor α [n]} : left = right ↔ ∀ (index : Fin n), left.getScalar index = right.getScalar index

def Spec.get2 {α : Type} [TorchLean.Storage α] {m n : ℕ} (tensor : TorchLean.Tensor α [m, n]) (row : Fin m) (column : Fin n) : α

Matrix element access.

theorem Spec.get2_eq_getScalar_get {α : Type} [TorchLean.Storage α] {m n : ℕ} (tensor : TorchLean.Tensor α [m, n]) (row : Fin m) (column : Fin n) : get2 tensor row column = (get tensor row).getScalar column

Matrix access is a row slice followed by a scalar read.

True by rfl, but worth a name: it is the rewrite that lets a matrix proof reuse every vector lemma about getScalar instead of duplicating them at rank two.

theorem Spec.get2_eq_apply {α : Type} [TorchLean.Storage α] {m n : ℕ} (tensor : TorchLean.Tensor α [m, n]) (row : Fin m) (column : Fin n) : get2 tensor row column = TorchLean.Tensor.Internal.Rep.get tensor (row, column, PUnit.unit)

Matrix scalar lookup is one read at the corresponding two-axis coordinate.

@[inline]

def Spec.Internal.get2Direct {α : Type} [TorchLean.Storage α] {m n : ℕ} (tensor : TorchLean.Tensor α [m, n]) (row : Fin m) (column : Fin n) : α

Direct storage read used when compiling matrix scalar lookup.

@[csimp]

theorem Spec.get2_eq_get2Direct : @get2 = @Internal.get2Direct

Compile matrix lookup without allocating an intermediate row or scalar tensor.

@[simp]

theorem Spec.get2_dim {α : Type} [TorchLean.Storage α] {m n : ℕ} (values : Fin m → Fin n → α) (row : Fin m) (column : Fin n) : get2 (TorchLean.Tensor.dim fun (i : Fin m) => TorchLean.Tensor.dim fun (j : Fin n) => TorchLean.Tensor.scalar (values i j)) row column = values row column

Reading back a matrix built from a two-argument function returns the function.

@[instance_reducible]

instance Spec.instGetElemTensorConsNatNilProdFinTrue {α : Type} [TorchLean.Storage α] {m n : ℕ} : GetElem (TorchLean.Tensor α [m, n]) (Fin m × Fin n) α fun (x : TorchLean.Tensor α [m, n]) (x_1 : Fin m × Fin n) => True

Total indexing and shape operations

def Spec.getAtOrZero {α : Type} [TorchLean.Storage α] [Zero α] {shape : Shape} (tensor : TorchLean.Tensor α shape) (indices : List ℕ) : α

Return zero when a runtime coordinate list is invalid.

@[simp]

theorem Spec.get_at_or_zero_scalar_nil {α : Type} [TorchLean.Storage α] [Zero α] (tensor : TorchLean.Tensor α (Shape.ofList [])) : getAtOrZero tensor [] = tensor.item

On a rank-zero tensor the empty coordinate list reads the item, no fallback needed.

@[simp]

theorem Spec.get_at_or_zero_scalar_cons {α : Type} [TorchLean.Storage α] [Zero α] (tensor : TorchLean.Tensor α (Shape.ofList [])) (index : ℕ) (indices : List ℕ) : getAtOrZero tensor (index :: indices) = 0

An over-long coordinate list on a rank-zero tensor falls back to zero.

@[simp]

theorem Spec.get_at_or_zero_dim_nil {α : Type} [TorchLean.Storage α] [Zero α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) : getAtOrZero tensor [] = 0

A too-short coordinate list falls back to zero.

@[simp]

theorem Spec.get_at_or_zero_dim_cons {α : Type} [TorchLean.Storage α] [Zero α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) (index : ℕ) (indices : List ℕ) : getAtOrZero tensor (index :: indices) = if h : index < n then getAtOrZero (tensor.unstack ⟨index, h⟩) indices else 0

One step of total lookup, with the out-of-range branch returning zero rather than failing.

The zero is what makes this function total, and it is also the reason the Zero α hypothesis is there: no shape argument can rule out a bad runtime coordinate list.

def Spec.tensorCast {α : Type} [TorchLean.Storage α] {source : Shape} (target : Shape) (h : source = target) : TorchLean.Tensor α source → TorchLean.Tensor α target

Cast a tensor along a shape equality.

@[simp]

theorem Spec.tensor_cast_eq_cast_shape {α : Type} [TorchLean.Storage α] {source target : Shape} (h : source = target) (tensor : TorchLean.Tensor α source) : tensorCast target h tensor = tensor.castShape h

tensorCast is castShape with the target shape written first.

def Spec.replicate {α : Type} [TorchLean.Storage α] {shape : Shape} : TorchLean.Tensor α Shape.scalar → TorchLean.Tensor α shape

Replicate a scalar tensor to any shape.

@[simp]

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

Every coordinate of a replicated tensor holds the source item.

@[simp]

theorem Spec.replicate_scalar_shape {α : Type} [TorchLean.Storage α] (tensor : TorchLean.Tensor α Shape.scalar) : replicate tensor = tensor

Replicating to rank zero returns the original scalar tensor.

@[simp]

theorem Spec.unstack_replicate {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α Shape.scalar) (index : Fin n) : (replicate tensor).unstack index = replicate tensor

Every slice of a replicated tensor is the replication of the same item.

@[simp]

theorem Spec.getScalar_replicate {α : Type} [TorchLean.Storage α] {n : ℕ} (tensor : TorchLean.Tensor α Shape.scalar) (index : Fin n) : (replicate tensor).getScalar index = tensor.item

Scalar lookup into a replicated vector returns the source item.

def TorchLean.Tensor.sliceAxisRangeCoordinate (axis : ℕ) {shape : Spec.Shape} [_h : Spec.Shape.AxisInBounds axis shape] (start count : ℕ) : start + count ≤ shape.axisSize axis → (shape.replaceAxis axis count).Coord → shape.Coord

Map an output coordinate of an axis slice back to its source coordinate.

def TorchLean.Tensor.sliceAxisRangeSpec {α : Type} [Storage α] (axis : ℕ) {shape : Spec.Shape} (tensor : Tensor α shape) [_h : Spec.Shape.AxisInBounds axis shape] (start count : ℕ) (hRange : start + count ≤ shape.axisSize axis) : Tensor α (shape.replaceAxis axis count)

Keep a contiguous coordinate range along an arbitrary axis.

The coordinate recursion above runs once per output element. The tensor itself is materialized in one packed pass, rather than recursively constructing and then restacking every outer slice.

@[simp]

theorem TorchLean.Tensor.sliceAxisRangeSpec_apply {α : Type} [Storage α] (axis : ℕ) {shape : Spec.Shape} (tensor : Tensor α shape) [_h : Spec.Shape.AxisInBounds axis shape] (start count : ℕ) (hRange : start + count ≤ shape.axisSize axis) (coordinate : (shape.replaceAxis axis count).Coord) : Internal.Rep.get (sliceAxisRangeSpec axis tensor start count hRange) coordinate = Internal.Rep.get tensor (sliceAxisRangeCoordinate axis start count hRange coordinate)

An axis slice reads the source coordinate selected by its checked range map.

def Spec.sliceRangeSpec {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) (start length : ℕ) (h : start + length ≤ n) : TorchLean.Tensor α (Shape.dim length shape)

Slice a contiguous range along the first axis.

def Spec.finZero {n : ℕ} (h : 0 < n) : Fin n

The first index of a nonempty axis.

def Spec.getHead {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) : Option (TorchLean.Tensor α shape)

First slice along the outer axis, or none when that axis is empty.

The Option is what an empty axis costs: n is a variable here, so no shape argument can promise there is a first slice, and returning none keeps the function total.

def Spec.getTail {α : Type} [TorchLean.Storage α] {n : ℕ} {shape : Shape} (tensor : TorchLean.Tensor α (Shape.dim n shape)) : Option (TorchLean.Tensor α (Shape.dim (n - 1) shape))

Everything after the first slice, or none when the outer axis is empty.

Pointwise operations and predicates

def TorchLean.Tensor.map {α β : Type} [Storage α] [Storage β] {shape : Spec.Shape} (f : α → β) (tensor : Tensor α shape) : Tensor β shape

Apply a scalar function pointwise while preserving the shape.

@[simp]

theorem TorchLean.Tensor.map_scalar {α β : Type} [Storage α] [Storage β] (f : α → β) (value : α) : map f (scalar value) = scalar (f value)

Mapping over a scalar tensor applies the function to its value.

@[simp]

theorem TorchLean.Tensor.map_dim {α β : Type} [Storage α] [Storage β] {n : ℕ} {shape : Spec.Shape} (f : α → β) (values : Fin n → Tensor α shape) : map f (dim values) = dim fun (index : Fin n) => map f (values index)

Mapping commutes with stacking, so a map pushes into every slice.

@[simp]

theorem TorchLean.Tensor.item_map {α β : Type} [Storage α] [Storage β] (f : α → β) (tensor : Tensor α Spec.Shape.scalar) : (map f tensor).item = f tensor.item

The item of a mapped scalar tensor is the function applied to the item.

@[simp]

theorem TorchLean.Tensor.unstack_map {α β : Type} [Storage α] [Storage β] {n : ℕ} {shape : Spec.Shape} (f : α → β) (tensor : Tensor α (Spec.Shape.dim n shape)) (index : Fin n) : (map f tensor).unstack index = map f (tensor.unstack index)

Slicing after a map is mapping after a slice.

@[simp]

theorem TorchLean.Tensor.getScalar_map {α β : Type} [Storage α] [Storage β] {n : ℕ} (f : α → β) (tensor : Tensor α [n]) (index : Fin n) : (map f tensor).getScalar index = f (tensor.getScalar index)

Scalar lookup after a map is the function applied to the lookup.

def TorchLean.Tensor.Forall {α : Type} [Storage α] (predicate : α → Prop) {shape : Spec.Shape} : Tensor α shape → Prop

Every scalar entry satisfies predicate.

def TorchLean.Tensor.Forall₂ {α β : Type} [Storage α] [Storage β] (relation : α → β → Prop) {shape : Spec.Shape} : Tensor α shape → Tensor β shape → Prop

Corresponding scalar entries satisfy relation.

@[simp]

theorem TorchLean.Tensor.forall_scalar {α : Type} [Storage α] {predicate : α → Prop} {value : α} : Forall predicate (scalar value) ↔ predicate value

Forall on a scalar tensor is the predicate on its value.

@[simp]

theorem TorchLean.Tensor.forall_dim {α : Type} [Storage α] {predicate : α → Prop} {n : ℕ} {shape : Spec.Shape} {values : Fin n → Tensor α shape} : Forall predicate (dim values) ↔ ∀ (index : Fin n), Forall predicate (values index)

Forall on a stacked tensor is Forall on every slice.

@[simp]

theorem TorchLean.Tensor.forall₂_scalar {α β : Type} [Storage α] [Storage β] {relation : α → β → Prop} {left : α} {right : β} : Forall₂ relation (scalar left) (scalar right) ↔ relation left right

Forall₂ on scalar tensors is the relation on the two values.

@[simp]

theorem TorchLean.Tensor.forall₂_dim {α β : Type} [Storage α] [Storage β] {relation : α → β → Prop} {n : ℕ} {shape : Spec.Shape} {left : Fin n → Tensor α shape} {right : Fin n → Tensor β shape} : Forall₂ relation (dim left) (dim right) ↔ ∀ (index : Fin n), Forall₂ relation (left index) (right index)

Forall₂ on stacked tensors is Forall₂ slicewise.

theorem TorchLean.Tensor.forall_true {α : Type} [Storage α] {shape : Spec.Shape} (tensor : Tensor α shape) : Forall (fun (x : α) => True) tensor

The trivial predicate holds of every tensor, at every shape.

theorem TorchLean.Tensor.forall_map {α β : Type} [Storage α] [Storage β] {predicate : α → Prop} {resultPredicate : β → Prop} {f : α → β} {shape : Spec.Shape} {tensor : Tensor α shape} (hTensor : Forall predicate tensor) (hMap : ∀ (value : α), predicate value → resultPredicate (f value)) : Forall resultPredicate (map f tensor)

Forall transports along map when the function respects the two predicates.

This is the workhorse for the numeric layers: a bound proved entrywise for the input survives an elementwise activation as long as the activation maps the input bound into the output one.

theorem TorchLean.Tensor.forall_replicate {α : Type} [Storage α] {predicate : α → Prop} {shape : Spec.Shape} {value : α} (hValue : predicate value) : Forall predicate (Spec.replicate (scalar value))

A predicate true of one value is true entrywise of the tensor replicating it.

def TorchLean.Tensor.prod {α : Type} [Storage α] [Mul α] [One α] {n : ℕ} (tensor : Tensor α [n]) : α

Multiply all vector entries in row-major order.

def Spec.pretty {α : Type} [TorchLean.Storage α] [ToString α] {shape : Shape} : TorchLean.Tensor α shape → String

Render a tensor recursively using the scalar ToString instance.