Tensor Numerical Algorithms

Reference implementations shared by classical models, graph specifications, and runtime checks:

• matrix minors, determinants, inverses, and power iteration;
• distances between vectors;
• vector normalization.

Intent / tradeoffs

These definitions prioritize:

• mathematical clarity, and
• shape safety (via TorchLean.Tensor), over performance.

In particular, determinantSpec uses Laplace expansion, which is exponentially expensive and is only meant for small matrices (for example, 2 x 2 or 3 x 3) and proof-oriented reference code. For large-scale linear algebra, use the runtime layer with array-backed kernels.

theorem Spec.minorIndex_lt {n : ℕ} (skip : Fin n) (i : Fin (n - 1)) : (if ↑i < ↑skip then ↑i else ↑i + 1) < n

The index in Fin n corresponding to i : Fin (n - 1) after skipping one position.

def Spec.matrixMinorSpec {α : Type} [TorchLean.Storage α] {n : ℕ} (matrix : TorchLean.Tensor α [n, n]) (row col : Fin n) : TorchLean.Tensor α [n - 1, n - 1]

Matrix minor: delete row and col from an n × n matrix, producing an (n-1) × (n-1) matrix.

This is used by determinantSpec (Laplace expansion) and the adjugate-based inverse below.

def Spec.determinantSpec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} : TorchLean.Tensor α [n, n] → TorchLean.Tensor α Shape.scalar

Determinant of an n × n matrix (spec-level reference implementation).

This uses Laplace expansion (cofactor expansion) along the first row, with special-cased base cases for n = 0, 1, 2. It is mathematically clear but exponentially slow, so it is intended only for very small n and/or proof-oriented reference code.

def Spec.inverseSpec? {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (matrix : TorchLean.Tensor α [n, n]) : Option (TorchLean.Tensor α [n, n])

Matrix inverse via the adjugate formula (spec-level reference implementation).

The result is none when the determinant is zero. Returning an unrelated matrix for a singular input would make downstream statistical formulas appear defined when they are not.

PyTorch analogue: torch.linalg.inv, with failure represented explicitly by Option.

def Spec.powerIterationLeadingEigenpairSpec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (matrix : TorchLean.Tensor α [n, n]) (iterations : ℕ) : α × TorchLean.Tensor α [n]

Approximate the leading eigenpair by a caller-selected number of power-iteration steps.

The scalar is the final Rayleigh quotient and the tensor is the corresponding normalized iterate. This definition does not claim to compute a full eigendecomposition. Convergence to a dominant eigenvector requires the usual spectral assumptions on matrix and a suitable initial vector.

@[irreducible]

def Spec.powerIterationLeadingEigenpairSpec.powerIteration {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (matrix : TorchLean.Tensor α [n, n]) (v : TorchLean.Tensor α [n]) (iter : ℕ) : TorchLean.Tensor α [n] × α

def Spec.euclideanDistanceSpec {α : Type} [TorchLean.Storage α] [Context α] {nFeatures : ℕ} (x y : TorchLean.Tensor α [nFeatures]) : α

Euclidean (L2) distance between two feature vectors.

PyTorch analogue: torch.linalg.vector_norm(x - y) or torch.cdist (batched).

def Spec.squaredEuclideanDistanceSpec {α : Type} [TorchLean.Storage α] [Context α] {nFeatures : ℕ} (x y : TorchLean.Tensor α [nFeatures]) : α

Squared Euclidean distance (avoids the final square root).

def Spec.manhattanDistanceSpec {α : Type} [TorchLean.Storage α] [Context α] {nFeatures : ℕ} (x y : TorchLean.Tensor α [nFeatures]) : α

Manhattan (L1) distance between two feature vectors.

def Spec.cosineDistanceSpec {α : Type} [TorchLean.Storage α] [Context α] {nFeatures : ℕ} (x y : TorchLean.Tensor α [nFeatures]) : α

Cosine distance 1 - cos(theta) between two feature vectors.

If either vector has zero norm, this returns 1.

def Spec.minkowskiDistanceSpec {α : Type} [TorchLean.Storage α] [Context α] {nFeatures : ℕ} (p : α) (_hp : p > 0) (x y : TorchLean.Tensor α [nFeatures]) : α

Minkowski distance of order p between two feature vectors.

This generalizes L1 (Manhattan) and L2 (Euclidean). The explicit positivity hypothesis rules out the undefined order-zero and negative-order cases.

def Spec.normalizeByPositiveSumSpec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (values : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n]

Divide a vector by its sum when that sum is positive.

If the sum is not positive, this returns the uniform vector. When the input entries are nonnegative, the positive-sum branch is a probability distribution.

PyTorch analogue: probs / probs.sum() (with an explicit zero-sum guard).

def Spec.normalizeL2Spec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (vector : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n]

L2-normalize a vector.

If the norm is 0, this returns the input unchanged.

def Spec.normalizeL2RegularizedSpec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (vector : TorchLean.Tensor α [n]) (regularizer : α) : TorchLean.Tensor α [n]

L2-normalize a vector with an additive regularizer under the square root.

The denominator is

sqrt (sumᵢ vector[i] ^ 2 + regularizer).

Unlike normalizeL2Spec, this operation has no zero-norm branch. Callers are responsible for choosing a regularizer that makes the denominator meaningful in their scalar context. This is the normalization convention used by several attention and recurrent architectures, where the exact regularizer is part of the model specification.

def Spec.normalizeZscoreSpec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (vector : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n]

Z-score normalization: subtract the mean and divide by the population standard deviation.

Zero denominators follow the same convention as normalizeL2Spec and normalizeByPositiveSumSpec: each denominator is tested before it is used. When n = 0 there is nothing to normalize and the empty input is returned without ever forming sum / n. When the standard deviation is 0, the mean-centered vector is returned.