Synthetic Samples and Small Datasets

This module provides small deterministic data generators used by examples and tests:

• 2D tabular grids (grid2, linspace)
• simple regression/classification sample builders
• a small "band image" generator (2D patterns) for CHW examples

These helpers are simple and in-memory. They keep tutorial code focused on models and verification rather than data-loading infrastructure.

Tabular 2D

@[reducible, inline]

abbrev NN.API.Samples.affine2 (w1 w2 b x1 x2 : Float) : Float

2D affine synthetic target function generator (re-exported from the runtime helper module).

def NN.API.Samples.vec1Float (y : Float) : Spec.Tensor Float (Spec.Shape.dim 1 Spec.Shape.scalar)

A length-1 float vector tensor.

def NN.API.Samples.vec2Float (x1 x2 : Float) : Spec.Tensor Float (Spec.Shape.dim 2 Spec.Shape.scalar)

A length-2 float vector tensor.

def NN.API.Samples.grid2 {m n : ℕ} (xs : Spec.Tensor Float (Spec.Shape.dim m Spec.Shape.scalar)) (ys : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.Tensor Float (Spec.Shape.dim (m * n) (Spec.Shape.dim 2 Spec.Shape.scalar))

Cartesian product of two float vectors (batched tensor of points).

grid2 xs ys produces a tensor X : (m*n, 2) containing all pairs (x, y) with:

• x taken from xs : (m,)
• y taken from ys : (n,)

Ordering is row-major: for each x in xs (outer loop), we sweep all y in ys (inner loop).

PyTorch analogue: torch.cartesian_prod(xs, ys) (up to shape).

def NN.API.Samples.linspace (lo hi : Float) (count : ℕ) : Spec.Tensor Float (Spec.Shape.dim count Spec.Shape.scalar)

Linearly spaced points including endpoints.

linspace lo hi count returns a vector tensor of shape (count,):

• empty if count = 0
• [lo] if count = 1
• otherwise count points from lo to hi (inclusive).

PyTorch analogue: torch.linspace.

def NN.API.Samples.grid2Rect (xLo xHi yLo yHi : Float) (xCount yCount : ℕ) : Spec.Tensor Float (Spec.Shape.dim (xCount * yCount) (Spec.Shape.dim 2 Spec.Shape.scalar))

Rectangular grid over [xLo, xHi] x [yLo, yHi].

def NN.API.Samples.grid2Square (lo hi : Float) (count : ℕ) : Spec.Tensor Float (Spec.Shape.dim (count * count) (Spec.Shape.dim 2 Spec.Shape.scalar))

Square grid over [lo, hi] x [lo, hi].

def NN.API.Samples.regression2to1Float {n : ℕ} (X : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim 2 Spec.Shape.scalar))) (f : Float → Float → Float) : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim 1 Spec.Shape.scalar))

Compute 2D→1D regression targets for a batched grid.

Input X has shape (n,2) and the output Y has shape (n,1).

def NN.API.Samples.vec1 {α : Type} [Context α] (cast : Float → α) (y : Float) : Spec.Tensor α (Spec.Shape.dim 1 Spec.Shape.scalar)

Casted version of vec1Float under an arbitrary scalar semantics α.

def NN.API.Samples.vec2 {α : Type} [Context α] (cast : Float → α) (x1 x2 : Float) : Spec.Tensor α (Spec.Shape.dim 2 Spec.Shape.scalar)

Casted version of vec2Float under an arbitrary scalar semantics α.

Image 2D (Synthetic CHW Pixels)

inductive NN.API.Samples.Image2D.Axis : Type

Which axis a synthetic "band" varies along.

We use this to build small labeled image datasets without depending on any external image format.

• row : Axis
• col : Axis

@[implicit_reducible]

instance NN.API.Samples.Image2D.instReprAxis : Repr Axis

def NN.API.Samples.Image2D.instReprAxis.repr : Axis → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.Samples.Image2D.instDecidableEqAxis : DecidableEq Axis

def NN.API.Samples.Image2D.Axis.name : Axis → String

Human-readable axis name (useful in example titles / sample names).

def NN.API.Samples.Image2D.renderCHWFloat (c h w : ℕ) (pixel : Fin c → Fin h → Fin w → Float) : Spec.Tensor Float (Tensor.Shape.CHW c h w)

Render a CHW c h w image tensor from a pixel function.

The pixel function is indexed by Fin indices that are guaranteed to be in-bounds.

def NN.API.Samples.Image2D.binaryCHWFloat (c h w : ℕ) (on : Fin c → Fin h → Fin w → Bool) (onValue : Float := 1.0) (offValue : Float := 0.0) : Spec.Tensor Float (Tensor.Shape.CHW c h w)

Binary image tensor renderer in CHW layout.

Pixels satisfying on c row col get onValue; the rest get offValue.

def NN.API.Samples.Image2D.bandCHWFloat (h w : ℕ) (axis : Axis) (offset : ℕ) (thickness : ℕ := 2) (onValue : Float := 1.0) (offValue : Float := 0.0) : Spec.Tensor Float (Tensor.Shape.CHW 1 h w)

Render a thick horizontal or vertical band into an h x w image tensor.

This is used to create small classification datasets where the label is "horizontal" vs "vertical".

Returns a single-channel CHW 1 h w image tensor (channel-first, PyTorch style).

structure NN.API.Samples.Image2D.BandClass : Type

Label metadata for a class of synthetic band images.

• axis : Axis

  Axis.

• label : ℕ

  Label.

• name : String

  Name.

def NN.API.Samples.Image2D.verticalClass (label : ℕ := 0) (name : String := "vertical") : BandClass

Convenience constructor for a "vertical band" class.

def NN.API.Samples.Image2D.horizontalClass (label : ℕ := 1) (name : String := "horizontal") : BandClass

Convenience constructor for a "horizontal band" class.

def NN.API.Samples.Image2D.bandDatasetCHWFloat (h w : ℕ) (classes : List BandClass) (offsets : List ℕ) (thickness : ℕ := 2) : List (Spec.Tensor Float (Tensor.Shape.CHW 1 h w) × ℕ)

Generate labeled band samples for a list of classes and offsets.

This produces a list of (x, label) pairs where x is a typed CHW 1 h w tensor.

def NN.API.Samples.Image2D.namedBandSamplesCHWFloat (h w : ℕ) (specs : List (BandClass × ℕ)) (thickness : ℕ := 2) : List (String × Spec.Tensor Float (Tensor.Shape.CHW 1 h w) × ℕ)

Like bandDatasetCHWFloat, but keep a human-readable name for each sample.

Each entry is (name, x, label) where x is a typed CHW 1 h w tensor.

Labels and Packing

def NN.API.Samples.oneHotFloat (classes label : ℕ) : Spec.Tensor Float (Tensor.Shape.Vec classes)

One-hot encode a label as a float vector of shape Vec classes.

def NN.API.Samples.oneHot {α : Type} [Context α] (cast : Float → α) (classes label : ℕ) : Spec.Tensor α (Tensor.Shape.Vec classes)

Casted version of oneHotFloat.

def NN.API.Samples.classification {α : Type} [Context α] {σ : Spec.Shape} (cast : Float → α) (classes : ℕ) (xs : List (Spec.Tensor Float σ × ℕ)) : List (Spec.Tensor α σ × Spec.Tensor α (Tensor.Shape.Vec classes))

Convert (x, label) pairs into (x, oneHot(label)) pairs.

This is a pure preprocessing step that keeps the data in-memory.

def NN.API.Samples.supervised {α : Type} [Context α] {σ τ : Spec.Shape} (cast : Float → α) (xs : List (Spec.Tensor Float σ × Spec.Tensor Float τ)) : List (Runtime.Autograd.Torch.TList α [σ, τ])

Pack (x, y) tensor pairs into TorchLean supervised TList samples.

This is the common sample representation used by the training helpers.

def NN.API.Samples.labeled {α : Type} [Context α] {σ : Spec.Shape} (cast : Float → α) (classes : ℕ) (xs : List (Spec.Tensor Float σ × ℕ)) : List (Runtime.Autograd.Torch.TList α [σ, Tensor.Shape.Vec classes])

Convert (x, label) pairs into TorchLean TList samples with one-hot targets.

CHW Parsing

def NN.API.Samples.imageCHWFloat (c h w : ℕ) (xs : List Float) : Except String (Spec.Tensor Float (Tensor.Shape.CHW c h w))

Interpret a flat list of floats as an image tensor of shape CHW c h w.

Fails if xs.length ≠ c*h*w.

def NN.API.Samples.imageCHW {α : Type} [Context α] (cast : Float → α) (c h w : ℕ) (xs : List Float) : Except String (Spec.Tensor α (Tensor.Shape.CHW c h w))

Casted version of imageCHWFloat.