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.minor_index_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 backend comparison det == 0 succeeds. No conditioning or finiteness check is performed; on floating-point backends, a nonzero or NaN determinant can therefore produce nonfinite entries.

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 : ℕ) (initial : TorchLean.Tensor α [n] := have raw := TorchLean.Tensor.ones [n]; have norm := MathFunctions.sqrt raw.squareSpec.sumSpec; if norm > 0 then raw.scaleSpec (1 / norm) else raw) : α × TorchLean.Tensor α [n]

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

The scalar is the final dot product v · (matrix v), which is the Rayleigh quotient when v has unit norm. Each normalization is attempted only when its computed norm is positive; finite-precision execution does not guarantee a unit vector. Convergence to a dominant eigenvector requires spectral assumptions on matrix and a suitable initial vector.

The default initial is the normalized all-ones vector. An explicitly supplied tensor is used as-is, so callers can retain their own initialization and normalization convention.

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.normalizeL2RegularizedSpec {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (vector : TorchLean.Tensor α [n]) (regularizer : α) (mean : Bool := false) : TorchLean.Tensor α [n]

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

The denominator is

sqrt (sumᵢ vector[i] ^ 2 + regularizer), or the mean square when mean := true.

Divide by a shared positive scale before squaring, and scale the regularizer by the same square. For a nonzero finite scale, the scaled entries have magnitude at most one before squaring. The scale is detached: its value cancels from the real function, so it need not contribute derivatives or introduce a max-selection kink.

Safe scaling of sums of squares is classical; see Anderson's Algorithm 978. Here the regularizer is scaled too, to preserve the epsilon-bearing formula. This does not guarantee finite output for every format: the reduction, its element-count cast, or a gradient can still exceed that format's range.

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.

When n = 0, the empty input is returned before forming a division. Otherwise the mean and variance divide by the scalar cast (n : α) without testing that cast for zero or finiteness. The final division occurs only when the computed standard deviation is positive; otherwise the mean-centered vector is returned. These guards do not guarantee finite output on every backend.