@[reducible, inline]

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

Public name for TorchLean's shape-indexed tensor-pack / typed tuple representation.

@[reducible, inline]

abbrev NN.API.tensorpack.mk1 {α : Type} {s : Spec.Shape} (x : Spec.Tensor α s) : TensorPack α [s]

Construct a 1-element tensor pack.

@[reducible, inline]

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

Construct a 2-element tensor pack.

@[reducible, inline]

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

Construct a 3-element tensor pack.

@[reducible, inline]

abbrev NN.API.tensorpack.mk4 {α : 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 4-element tensor pack.

def NN.API.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 NN.API.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 NN.API.tensorpack.append {α : Type} {ss₁ ss₂ : List Spec.Shape} : TensorPack α ss₁ → TensorPack α ss₂ → TensorPack α (ss₁ ++ ss₂)

Append two tensor packs.

def NN.API.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 NN.API.tensorpack.get0 {α : Type} {s : Spec.Shape} {ss : List Spec.Shape} : TensorPack α (s :: ss) → Spec.Tensor α s

First element of a non-empty tensor pack.

def NN.API.tensorpack.get1 {α : 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 NN.API.tensorpack.get2 {α : 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 NN.API.tensorpack.get3 {α : 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 NN.API.tensorpack.unpack1 {α : Type} {s : Spec.Shape} : TensorPack α [s] → Spec.Tensor α s

Unpack a one-element tensor pack.

def NN.API.tensorpack.unpack2 {α : 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 NN.API.tensorpack.unpack3 {α : 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 NN.API.tensorpack.unpack4 {α : 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 4-tuple.

@[reducible, inline]

abbrev NN.API.sample.Supervised (α : Type) (σ τ : Spec.Shape) : Type

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

@[reducible, inline]

abbrev NN.API.sample.Batch (α : Type) (n : ℕ) (σ τ : Spec.Shape) : Type

A fixed-size minibatch of supervised samples.

def NN.API.sample.mk {α : Type} {σ τ : Spec.Shape} (x : Spec.Tensor α σ) (y : Spec.Tensor α τ) : Supervised α σ τ

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

def NN.API.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 NN.API.sample.x {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α σ

Extract the input tensor x from a supervised sample.

def NN.API.sample.y {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α τ

Extract the target tensor y from a supervised sample.

def NN.API.sample.toPair {α : Type} {σ τ : Spec.Shape} (s : Supervised α σ τ) : Spec.Tensor α σ × Spec.Tensor α τ

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

@[simp]

theorem NN.API.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 NN.API.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 NN.API.sample.toPair_mk {α : Type} {σ τ : Spec.Shape} (xT : Spec.Tensor α σ) (yT : Spec.Tensor α τ) : toPair (mk xT yT) = (xT, yT)

def NN.API.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 NN.API.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 NN.API.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 NN.API.SupervisedSample (α : Type) (σ τ : Spec.Shape) : Type

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