Vector tensors (Spec.Vec)

TorchLean’s spec tensor type is shape-indexed:

Spec.Tensor α s

For many developments we need the special case “a length-n vector of scalars”, i.e.

Spec.Tensor α (.dim n .scalar).

This file packages that case up as Spec.Vec n α and provides basic, representation-agnostic helpers:

• convert to/from functions Fin n → α,
• coordinate access, and
• total “update one coordinate” / “remove one coordinate” operations.

These utilities are used by learning-theory code (datasets as vectors of examples) and are also generally handy for connecting tensor-shaped objects to Fin-indexed mathlib APIs.

References / analogies:

• This is the shape-indexed tensor analogue of the function type Fin n -> α (a dependent Pi), packaged so we can reuse Tensor infrastructure while still interoperating with mathlib's Fin-indexed APIs.
• Lean core / mathlib building blocks used here: Fin, Function.update, and Fin.succAbove.

@[reducible, inline]

abbrev Spec.Vec (n : ℕ) (α : Type) : Type

A length-n vector of scalar entries α as a spec tensor.

@[reducible, inline]

abbrev Spec.Vec.toFn {n : ℕ} {α : Type} (v : Vec n α) : Fin n → α

View a vector tensor as a function Fin n → α.

@[reducible, inline]

abbrev Spec.Vec.ofFn {n : ℕ} {α : Type} (f : Fin n → α) : Vec n α

Build a vector tensor from a function Fin n → α.

@[simp]

theorem Spec.Vec.toFn_ofFn {n : ℕ} {α : Type} (f : Fin n → α) : (ofFn f).toFn = f

@[simp]

theorem Spec.Vec.ofFn_toFn {n : ℕ} {α : Type} (v : Vec n α) : ofFn v.toFn = v

@[reducible, inline]

abbrev Spec.Vec.get {n : ℕ} {α : Type} (v : Vec n α) (i : Fin n) : α

Coordinate access for vector tensors.

@[simp]

theorem Spec.Vec.get_ofFn {n : ℕ} {α : Type} (f : Fin n → α) (i : Fin n) : (ofFn f).get i = f i

def Spec.Vec.update {n : ℕ} {α : Type} [DecidableEq (Fin n)] (v : Vec n α) (i : Fin n) (a' : α) : Vec n α

Update one coordinate (total, using Fin indices).

def Spec.Vec.removeAt {n : ℕ} {α : Type} (v : Vec (n + 1) α) (i : Fin (n + 1)) : Vec n α

Remove one coordinate from a vector of length n+1.

This uses Fin.succAbove to reindex the remaining entries into Fin n.