Pointwise and family tensor operations

Scalar maps, binary maps, finite tensor families, stacking, and rank-one list construction over native tensor storage.

def TorchLean.Tensor.Internal.sequenceFinM {m : Type → Type} [Monad m] {α : Type} {n : ℕ} (f : Fin n → m α) : m (Fin n → α)

Evaluate a finite family once per index in ascending order and retain indexed access.

The temporary buffer also supports heterogeneous tensor packs, which have no scalar Storage instance. Public construction APIs expose tensors or packs rather than this buffer.

@[inline]

unsafe def TorchLean.Tensor.Internal.Rep.constFast {α : Type u} [Storage α] {s : Shape} (a : α) : Rep α s

Native implementation of constant tensor construction.

@[implemented_by TorchLean.Tensor.Internal.Rep.constFast]

def TorchLean.Tensor.Internal.Rep.const {α : Type u} [Storage α] {s : Shape} (a : α) : Rep α s

The constant tensor.

@[inline]

unsafe def TorchLean.Tensor.Internal.Rep.mapFast {α : Type u} [Storage α] {β : Type v} [Storage β] {s : Shape} (f : α → β) (x : Rep α s) : Rep β s

Native implementation of pointwise scalar maps.

@[implemented_by TorchLean.Tensor.Internal.Rep.mapFast]

def TorchLean.Tensor.Internal.Rep.map {α : Type u} [Storage α] {β : Type v} [Storage β] {s : Shape} (f : α → β) (x : Rep α s) : Rep β s

Apply a scalar function pointwise.

@[inline]

unsafe def TorchLean.Tensor.Internal.Rep.zipWithFast {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {s : Shape} (f : α → β → γ) (x : Rep α s) (y : Rep β s) : Rep γ s

Native implementation of pointwise binary maps.

@[implemented_by TorchLean.Tensor.Internal.Rep.zipWithFast]

def TorchLean.Tensor.Internal.Rep.zipWith {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {s : Shape} (f : α → β → γ) (x : Rep α s) (y : Rep β s) : Rep γ s

Apply a binary scalar function pointwise.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instAdd {α : Type u} [Storage α] {s : Shape} [Add α] : Add (Rep α s)

Tensor addition applies scalar addition entrywise.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.const_apply {α : Type u} [Storage α] {s : Shape} (a : α) (i : Coord s) : (const a).get i = a

Evaluating a constant tensor returns its defining scalar.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.map_apply {α : Type u} [Storage α] {β : Type v} [Storage β] {s : Shape} (f : α → β) (x : Rep α s) (i : Coord s) : (map f x).get i = f (x.get i)

Evaluating a pointwise map applies the scalar function at that coordinate.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.zipWith_apply {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {s : Shape} (f : α → β → γ) (x : Rep α s) (y : Rep β s) (i : Coord s) : (zipWith f x y).get i = f (x.get i) (y.get i)

Evaluating a pointwise binary map combines the two entries at that coordinate.

@[simp]

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

Homogeneous tensor addition applies scalar addition pointwise.

Pointwise algebraic structure

Every algebraic operation on native tensors is the scalar operation applied coordinatewise. The instances below are the only 0, -, and • on Rep α s; together with + above they form the pointwise AddCommGroup and Module structures. The *_apply lemmas are the simp normal forms.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instZero {α : Type u} [Storage α] {s : Shape} [Zero α] : Zero (Rep α s)

The zero tensor holds the scalar zero at every coordinate.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instNeg {α : Type u} [Storage α] {s : Shape} [Neg α] : Neg (Rep α s)

Tensor negation negates every coordinate.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instSub {α : Type u} [Storage α] {s : Shape} [Sub α] : Sub (Rep α s)

Tensor subtraction subtracts coordinatewise.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instSMul {R : Type v} {α : Type u} [Storage α] {s : Shape} [SMul R α] : SMul R (Rep α s)

A scalar acts on a tensor by acting on every coordinate.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.zero_apply {α : Type u} [Storage α] {s : Shape} [Zero α] (i : Coord s) : get 0 i = 0

Every coordinate of the zero tensor is the scalar zero.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.neg_apply {α : Type u} [Storage α] {s : Shape} [Neg α] (x : Rep α s) (i : Coord s) : (-x).get i = -x.get i

Tensor negation is coordinatewise scalar negation.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.hSub_apply {α : Type u} [Storage α] {s : Shape} [Sub α] (x y : Rep α s) (i : Coord s) : (x - y).get i = x.get i - y.get i

Tensor subtraction is coordinatewise scalar subtraction.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.smul_apply {R : Type v} {α : Type u} [Storage α] {s : Shape} [SMul R α] (c : R) (x : Rep α s) (i : Coord s) : (c • x).get i = c • x.get i

A scalar acts on a tensor coordinatewise.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instAddCommMonoid {α : Type u} [Storage α] {s : Shape} [AddCommMonoid α] : AddCommMonoid (Rep α s)

Tensor addition is a commutative monoid, coordinatewise.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instAddCommGroup {α : Type u} [Storage α] {s : Shape} [AddCommGroup α] : AddCommGroup (Rep α s)

Tensor subtraction and negation form a commutative group, coordinatewise.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instModule {R : Type v} {α : Type u} [Storage α] {s : Shape} [Semiring R] [AddCommMonoid α] [Module R α] : Module R (Rep α s)

Tensors over a module are a module, coordinatewise.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.map_id {α : Type u} [Storage α] {s : Shape} (x : Rep α s) : map id x = x

Mapping the identity function leaves every tensor unchanged.

This is a deterministic simplification rule rather than a global e-matching rule. Combined with map composition, unrestricted congruence closure could otherwise manufacture arbitrarily many nested identity maps.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.map_map {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {s : Shape} (outer : β → γ) (inner : α → β) (x : Rep α s) : map outer (map inner x) = map (outer ∘ inner) x

Two pointwise maps fuse to one scalar composition.

The theorem belongs to the canonical simplifier, but intentionally not to the global grind set: composition-producing e-matching rules can repeatedly instantiate through equal identity-map terms.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.map_zipWith {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {δ : Type u_1} [Storage δ] {s : Shape} (outer : γ → δ) (combine : α → β → γ) (x : Rep α s) (y : Rep β s) : map outer (zipWith combine x y) = zipWith (fun (left : α) (right : β) => outer (combine left right)) x y

A scalar map after a pointwise binary operation fuses into that operation.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.zipWith_map_map {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {δ : Type u_1} {ε : Type u_2} [Storage δ] [Storage ε] {s : Shape} (combine : γ → δ → ε) (leftMap : α → γ) (rightMap : β → δ) (x : Rep α s) (y : Rep β s) : zipWith combine (map leftMap x) (map rightMap y) = zipWith (fun (left : α) (right : β) => combine (leftMap left) (rightMap right)) x y

Pointwise maps on both inputs fuse into one pointwise binary operation.

@[inline]

unsafe def TorchLean.Tensor.Internal.Rep.stackFast {α : Type u} [Storage α] {n : ℕ} {s : Shape} (components : Fin n → Rep α s) : Rep α (n :: s)

Native implementation of leading-axis stacking.

Materializing the family first ensures that components is evaluated once per leading index. Without this cache, constructing each scalar in the output could rebuild its entire component tensor.

@[implemented_by TorchLean.Tensor.Internal.Rep.stackFast]

def TorchLean.Tensor.Internal.Rep.stack {α : Type u} [Storage α] {n : ℕ} {s : Shape} (components : Fin n → Rep α s) : Rep α (n :: s)

Place a finite family of identically shaped tensors along a new leading axis.

The transparent definition is the proof semantics. Compiled code uses stackFast, which preserves these semantics while evaluating each component only once.

def TorchLean.Tensor.Internal.Rep.unstack {α : Type u} [Storage α] {n : ℕ} {s : Shape} (tensor : Rep α (n :: s)) (component : Fin n) : Rep α s

Select one leading-axis slice from a stacked tensor.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.stack_apply {α : Type u} [Storage α] {n : ℕ} {s : Shape} (components : Fin n → Rep α s) (coordinate : Coord (n :: s)) : (stack components).get coordinate = (components coordinate.1).get coordinate.2

Observing a stack selects the component named by its leading coordinate.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.unstack_apply {α : Type u} [Storage α] {n : ℕ} {s : Shape} (tensor : Rep α (n :: s)) (component : Fin n) (coordinate : Coord s) : (tensor.unstack component).get coordinate = tensor.get (component, coordinate)

Observing a leading-axis slice fixes that axis to the selected component.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.unstack_const {α : Type u} [Storage α] {n : ℕ} {s : Shape} (value : α) (component : Fin n) : (const value).unstack component = const value

Every leading-axis slice of a constant tensor is the same constant tensor.

theorem TorchLean.Tensor.Internal.Rep.map_stack {α : Type u} [Storage α] {β : Type v} [Storage β] {n : ℕ} {s : Shape} (f : α → β) (components : Fin n → Rep α s) : map f (stack components) = stack fun (component : Fin n) => map f (components component)

Pointwise scalar maps commute with stacking a finite tensor family.

theorem TorchLean.Tensor.Internal.Rep.zipWith_stack {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {n : ℕ} {s : Shape} (f : α → β → γ) (x : Fin n → Rep α s) (y : Fin n → Rep β s) : zipWith f (stack x) (stack y) = stack fun (component : Fin n) => zipWith f (x component) (y component)

Pointwise binary operations commute with stacking matching families.

theorem TorchLean.Tensor.Internal.Rep.map_unstack {α : Type u} [Storage α] {β : Type v} [Storage β] {n : ℕ} {s : Shape} (f : α → β) (x : Rep α (n :: s)) (component : Fin n) : map f (x.unstack component) = (map f x).unstack component

Pointwise scalar maps commute with selecting a leading-axis slice.

theorem TorchLean.Tensor.Internal.Rep.zipWith_unstack {α : Type u} [Storage α] {β : Type v} [Storage β] {γ : Type w} [Storage γ] {n : ℕ} {s : Shape} (f : α → β → γ) (x : Rep α (n :: s)) (y : Rep β (n :: s)) (component : Fin n) : zipWith f (x.unstack component) (y.unstack component) = (zipWith f x y).unstack component

Pointwise binary operations commute with matching leading-axis slices.

def TorchLean.Tensor.Internal.Rep.stackList {α : Type u} [Storage α] {s : Shape} (components : List (Rep α s)) : Rep α (components.length :: s)

Stack the tensors in a list along a new leading axis.

For example, two tensors of shape [3] give a tensor of shape [2, 3]. The first component's entries come before the second's in row-major storage.

stack asks for components by index. We cache the list as an array so each lookup takes constant time. Reading the list directly would walk from its front again for each component.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.stackList_apply {α : Type u} [Storage α] {s : Shape} (components : List (Rep α s)) (coordinate : Coord (components.length :: s)) : (stackList components).get coordinate = (components.get coordinate.1).get coordinate.2

The leading coordinate chooses a list entry; the remaining coordinates index that tensor.

def TorchLean.Tensor.Internal.Rep.ofList {α : Type u} [Storage α] (values : List α) : Rep α [values.length]

Turn a list into a one-dimensional tensor in the same order.

For example, [x, y, z] gives shape [3], with x at coordinate zero. We cache the list as an array before Storage.ofFn copies its entries into the buffer selected by Storage α. Without the cache, requesting indices 0, ..., n - 1 would follow n * (n - 1) / 2 list links in total. The array makes each indexed read constant time.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.ofList_apply {α : Type u} [storage : Storage α] (values : List α) (index : Fin values.length) : (ofList values).get (index, PUnit.unit) = values.get index

A rank-one tensor built from a list reads the corresponding list entry.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.data_ofList {α : Type u} [storage : Storage α] (values : List α) : (ofList values).data = values.toArray

Observing a list-built tensor returns the original values in row-major order.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Rep.instCoeDepListTensor {α : Type u} [Storage α] (values : List α) : CoeDep (List α) values (Rep α [values.length])

Ordinary list notation constructs a rank-one tensor when the literal length matches the expected static dimension. Each list entry is copied into the tensor's storage in order.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.unstack_stack {α : Type u} [Storage α] {n : ℕ} {s : Shape} (components : Fin n → Rep α s) (component : Fin n) : (stack components).unstack component = components component

Selecting a component after stacking recovers the original component.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.stack_unstack {α : Type u} [Storage α] {n : ℕ} {s : Shape} (tensor : Rep α (n :: s)) : stack tensor.unstack = tensor

Stacking every leading-axis slice reconstructs the original tensor.

def TorchLean.Tensor.Internal.Rep.ofFlatFnM {m : Type → Type} [Monad m] {α : Type} [Storage α] {s : Shape} (f : Fin s.size → m α) : m (Rep α s)

Fill a temporary finite buffer in row-major effect order, then materialize native storage.

def TorchLean.Tensor.Internal.Rep.stackM {m : Type → Type} [Monad m] {α : Type} [Storage α] {n : ℕ} {s : Shape} (components : Fin n → m (Rep α s)) : m (Rep α (n :: s))

Sequence a finite family of component actions once each before stacking their native buffers.