Synthetic Data

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

• 2D tabular grids (cartesianGrid, linspace)
• simple regression/classification sample builders

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

Domain-specific datasets belong in their own modules. The band-classification example, for instance, lives in TorchLean.Data.Bands; this file contains only shape-independent generators.

Tabular 2D

def TorchLean.Data.Synthetic.affinePlane (w₁ w₂ b x₁ x₂ : Float) : Float

Affine function w₁x₁ + w₂x₂ + b for synthetic regression data.

def TorchLean.Data.Synthetic.singletonVectorFloat (y : Float) : Spec.Tensor Float (Spec.Shape.dim 1 Shape.scalar)

A length-1 float vector tensor.

def TorchLean.Data.Synthetic.pointVectorFloat (x y : Float) : Spec.Tensor Float (Spec.Shape.dim 2 Shape.scalar)

A length-2 float vector tensor.

def TorchLean.Data.Synthetic.cartesianGrid {m n : ℕ} (xs : Spec.Tensor Float (Spec.Shape.dim m Shape.scalar)) (ys : Spec.Tensor Float (Spec.Shape.dim n Shape.scalar)) : Spec.Tensor Float (Spec.Shape.dim (m * n) (Spec.Shape.dim 2 Shape.scalar))

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

cartesianGrid 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 TorchLean.Data.Synthetic.linspace (lo hi : Float) (count : ℕ) : Spec.Tensor Float (Spec.Shape.dim count 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 TorchLean.Data.Synthetic.rectangularGrid (xLo xHi yLo yHi : Float) (xCount yCount : ℕ) : Spec.Tensor Float (Spec.Shape.dim (xCount * yCount) (Spec.Shape.dim 2 Shape.scalar))

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

def TorchLean.Data.Synthetic.squareGrid (lo hi : Float) (count : ℕ) : Spec.Tensor Float (Spec.Shape.dim (count * count) (Spec.Shape.dim 2 Shape.scalar))

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

def TorchLean.Data.Synthetic.regressionTargetsFloat {n : ℕ} (X : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim 2 Shape.scalar))) (f : Float → Float → Float) : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim 1 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 TorchLean.Data.Synthetic.singletonVector {α : Type} [Context α] (cast : Float → α) (y : Float) : Spec.Tensor α (Spec.Shape.dim 1 Shape.scalar)

Casted version of singletonVectorFloat under an arbitrary scalar semantics α.

def TorchLean.Data.Synthetic.pointVector {α : Type} [Context α] (cast : Float → α) (x y : Float) : Spec.Tensor α (Spec.Shape.dim 2 Shape.scalar)

Casted version of pointVectorFloat under an arbitrary scalar semantics α.

Labels and Packing

def TorchLean.Data.Synthetic.oneHotFloat (classes label : ℕ) : Spec.Tensor Float (Spec.Shape.dim classes Shape.scalar)

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

def TorchLean.Data.Synthetic.oneHot {α : Type} [Context α] (cast : Float → α) (classes label : ℕ) : Spec.Tensor α (Spec.Shape.dim classes Shape.scalar)

Casted version of oneHotFloat.

def TorchLean.Data.Synthetic.classification {α : Type} [Context α] {σ : Shape} (cast : Float → α) (classes : ℕ) (xs : List (Spec.Tensor Float σ × ℕ)) : List (Spec.Tensor α σ × Spec.Tensor α (Spec.Shape.dim classes Shape.scalar))

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

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

def TorchLean.Data.Synthetic.supervised {α : Type} [Context α] {σ τ : Shape} (cast : Float → α) (xs : List (Spec.Tensor Float σ × Spec.Tensor Float τ)) : List (TensorPack α [σ, τ])

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

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

def TorchLean.Data.Synthetic.labeled {α : Type} [Context α] {σ : Shape} (cast : Float → α) (classes : ℕ) (xs : List (Spec.Tensor Float σ × ℕ)) : List (TensorPack α [σ, Spec.Shape.dim classes Shape.scalar])

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