Tensor Packs

Shape-indexed tensor packs and supervised samples.

Main declarations:

• TorchLean.TensorPack: a typed tuple of tensors.
• TorchLean.tensorpack.*: constructors, projections, mapping, zipping, append, and split.
• TorchLean.Sample.*: supervised (x, y) samples and minibatch wrappers.

These operations preserve the shapes carried by the underlying tensor-pack representation.

@[reducible, inline]

abbrev TorchLean.TensorPack (α : Type) (shapes : List Spec.Shape) : Type

A heterogeneous tensor tuple whose list of shapes is tracked in its type.

@[reducible, inline]

abbrev TorchLean.tensorpack.singleton {α : Type} {s : Spec.Shape} (x : Spec.Tensor α s) : TensorPack α [s]

Construct a one-element tensor pack.

@[reducible, inline]

abbrev TorchLean.tensorpack.pair {α : Type} {s₁ s₂ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) : TensorPack α [s₁, s₂]

Construct a two-element tensor pack.

@[reducible, inline]

abbrev TorchLean.tensorpack.triple {α : Type} {s₁ s₂ s₃ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) : TensorPack α [s₁, s₂, s₃]

Construct a three-element tensor pack.

@[reducible, inline]

abbrev TorchLean.tensorpack.quad {α : Type} {s₁ s₂ s₃ s₄ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) (x₄ : Spec.Tensor α s₄) : TensorPack α [s₁, s₂, s₃, s₄]

Construct a four-element tensor pack.

def TorchLean.tensorpack.map {α β : Type} (f : {s : Spec.Shape} → Spec.Tensor α s → Spec.Tensor β s) {ss : List Spec.Shape} : TensorPack α ss → TensorPack β ss

Map each tensor entry (shape-preserving).

def TorchLean.tensorpack.zipWith {α β γ : Type} (f : {s : Spec.Shape} → Spec.Tensor α s → Spec.Tensor β s → Spec.Tensor γ s) {ss : List Spec.Shape} : TensorPack α ss → TensorPack β ss → TensorPack γ ss

Zip two tensor packs pointwise (shape-preserving).

def TorchLean.tensorpack.append {α : Type} {ss₁ ss₂ : List Spec.Shape} : TensorPack α ss₁ → TensorPack α ss₂ → TensorPack α (ss₁ ++ ss₂)

Append two tensor packs.

def TorchLean.tensorpack.split {α : Type} {ss₁ ss₂ : List Spec.Shape} : TensorPack α (ss₁ ++ ss₂) → TensorPack α ss₁ × TensorPack α ss₂

Split a tensor pack into its prefix and suffix.

def TorchLean.tensorpack.first {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} : TensorPack α (s :: ss) → Spec.Tensor α s

First element of a non-empty tensor pack.

def TorchLean.tensorpack.second {α : Type} {s₀ s₁ : Spec.Shape} {ss : List Spec.Shape} : TensorPack α (s₀ :: s₁ :: ss) → Spec.Tensor α s₁

Second element of a tensor pack with at least two entries.

def TorchLean.tensorpack.third {α : Type} {s₀ s₁ s₂ : Spec.Shape} {ss : List Spec.Shape} : TensorPack α (s₀ :: s₁ :: s₂ :: ss) → Spec.Tensor α s₂

Third element of a tensor pack with at least three entries.

def TorchLean.tensorpack.fourth {α : Type} {s₀ s₁ s₂ s₃ : Spec.Shape} {ss : List Spec.Shape} : TensorPack α (s₀ :: s₁ :: s₂ :: s₃ :: ss) → Spec.Tensor α s₃

Fourth element of a tensor pack with at least four entries.

def TorchLean.tensorpack.unpackSingleton {α : Type} {s : Spec.Shape} : TensorPack α [s] → Spec.Tensor α s

Unpack a one-element tensor pack.

def TorchLean.tensorpack.unpackPair {α : Type} {s₁ s₂ : Spec.Shape} : TensorPack α [s₁, s₂] → Spec.Tensor α s₁ × Spec.Tensor α s₂

Unpack a two-element tensor pack into a Lean pair.

def TorchLean.tensorpack.unpackTriple {α : Type} {s₁ s₂ s₃ : Spec.Shape} : TensorPack α [s₁, s₂, s₃] → Spec.Tensor α s₁ × Spec.Tensor α s₂ × Spec.Tensor α s₃

Unpack a three-element tensor pack into a Lean triple.

def TorchLean.tensorpack.unpackQuad {α : Type} {s₁ s₂ s₃ s₄ : Spec.Shape} : TensorPack α [s₁, s₂, s₃, s₄] → Spec.Tensor α s₁ × Spec.Tensor α s₂ × Spec.Tensor α s₃ × Spec.Tensor α s₄

Unpack a four-element tensor pack into a Lean tuple.

def TorchLean.tensorpack.septuple {α : Type} {s₁ s₂ s₃ s₄ s₅ s₆ s₇ : Spec.Shape} (x₁ : Spec.Tensor α s₁) (x₂ : Spec.Tensor α s₂) (x₃ : Spec.Tensor α s₃) (x₄ : Spec.Tensor α s₄) (x₅ : Spec.Tensor α s₅) (x₆ : Spec.Tensor α s₆) (x₇ : Spec.Tensor α s₇) : TensorPack α [s₁, s₂, s₃, s₄, s₅, s₆, s₇]

Construct a seven-element tensor pack.

@[reducible, inline]

abbrev TorchLean.Sample.Supervised (α : Type) (σ τ : Spec.Shape) : Type

A supervised sample (x, y) with input shape σ and target shape τ.

@[reducible, inline]

abbrev TorchLean.Sample.Batch (α : Type) (n : ℕ) (σ τ : Spec.Shape) : Type

A fixed-size minibatch of supervised samples.

def TorchLean.Sample.mk {α : Type} {σ τ : Spec.Shape} (x : Spec.Tensor α σ) (y : Spec.Tensor α τ) : Supervised α σ τ

Build a supervised sample (x, y) as a two-tensor pack.

def TorchLean.Sample.batch {α : Type} {n : ℕ} {σ τ : Spec.Shape} (x : Spec.Tensor α (Spec.Shape.dim n σ)) (y : Spec.Tensor α (Spec.Shape.dim n τ)) : Batch α n σ τ

Build a batched supervised sample (xBatch, yBatch).

def TorchLean.Sample.x {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α σ

Extract the input tensor x from a supervised sample.

def TorchLean.Sample.y {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α τ

Extract the target tensor y from a supervised sample.

def TorchLean.Sample.toPair {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α σ × Spec.Tensor α τ

Unpack a supervised sample as the ordinary pair (x, y).

@[simp]

theorem TorchLean.Sample.x_mk {α : Type} {σ τ : Spec.Shape} (xT : Spec.Tensor α σ) (yT : Spec.Tensor α τ) : x (mk xT yT) = xT

x of a constructed supervised sample mk x y is x.

@[simp]

theorem TorchLean.Sample.y_mk {α : Type} {σ τ : Spec.Shape} (xT : Spec.Tensor α σ) (yT : Spec.Tensor α τ) : y (mk xT yT) = yT

y of a constructed supervised sample mk x y is y.

@[simp]

theorem TorchLean.Sample.toPair_mk {α : Type} {σ τ : Spec.Shape} (xT : Spec.Tensor α σ) (yT : Spec.Tensor α τ) : toPair (mk xT yT) = (xT, yT)

def TorchLean.Sample.mapX {α : Type} {σ τ : Spec.Shape} (f : Spec.Tensor α σ → Spec.Tensor α σ) (s : Supervised α σ τ) : Supervised α σ τ

Map a function over the input tensor x, leaving the target y unchanged.

def TorchLean.Sample.mapY {α : Type} {σ τ : Spec.Shape} (f : Spec.Tensor α τ → Spec.Tensor α τ) (s : Supervised α σ τ) : Supervised α σ τ

Map a function over the target tensor y, leaving the input x unchanged.

def TorchLean.Sample.mapXY {α : Type} {σ τ : Spec.Shape} (fx : Spec.Tensor α σ → Spec.Tensor α σ) (fy : Spec.Tensor α τ → Spec.Tensor α τ) (s : Supervised α σ τ) : Supervised α σ τ

Map functions over both x and y in a supervised sample.

@[reducible, inline]

abbrev TorchLean.SupervisedSample (α : Type) (σ τ : Spec.Shape) : Type

One supervised-learning observation containing an input tensor and its target tensor.