TorchLean Public Samples

Public sample types and constructors for supervised datasets.

@[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} {σ τ : Shape} (x : Tensor.T α σ) (y : Tensor.T α τ) : Supervised α σ τ

Build a supervised sample (x, y).

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

Build a batched supervised sample (xBatch, yBatch).

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

Extract the input tensor x from a supervised sample.

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

Extract the target tensor y from a supervised sample.

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

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

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

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

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

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

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

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

def TorchLean.Sample.repeatBatch {α : Type} {σ τ : Shape} (batch : ℕ) (s : Supervised α σ τ) : Supervised α (Spec.Shape.dim batch σ) (Spec.Shape.dim batch τ)

Repeat one supervised sample across a fixed batch axis.

Use this for examples that naturally produce one (x, y) pair but need a model whose input/output shapes already include a batch dimension.

def TorchLean.Samples.vec1 {α : Type} [Runtime.TensorScalar α] [Runtime.Scalar α] (y : Float) : Tensor.T α (Shape.vec 1)

A length-1 tensor, casting host Float into the selected runtime scalar.

def TorchLean.Samples.vec2 {α : Type} [Runtime.TensorScalar α] [Runtime.Scalar α] (x1 x2 : Float) : Tensor.T α (Shape.vec 2)

A length-2 tensor, casting host Float coordinates into the selected runtime scalar.