Public Tensor Linear Algebra

User-facing matrix factorizations and solves on the canonical tensor type.

def TorchLean.Tensor.identity {α : Type} [Storage α] [Zero α] [One α] (n : ℕ) : Tensor α [n, n]

Construct the n x n identity matrix.

structure TorchLean.Tensor.QRFactors (α : Type) [Storage α] (m n : ℕ) : Type

The reduced QR factors of an m x n matrix, with reduced width min m n.

• q : Tensor α [m, min m n]

  Matrix containing the reduced basis-column candidates.

• r : Tensor α [min m n, n]

  Upper-trapezoidal factor.

@[instance_reducible]

instance TorchLean.Tensor.instReprQRFactors {α✝ : Type} {inst✝ : Storage α✝} {m✝ n✝ : ℕ} [Repr α✝] : Repr (QRFactors α✝ m✝ n✝)

def TorchLean.Tensor.instReprQRFactors.repr {α✝ : Type} {inst✝ : Storage α✝} {m✝ n✝ : ℕ} [Repr α✝] : QRFactors α✝ m✝ n✝ → ℕ → Std.Format

def TorchLean.Tensor.Internal.wideQR {α : Type} [Storage α] [Context α] {m n : ℕ} (matrix : Tensor α [m, n]) : QRFactors α m n

Reduced QR by classical Gram-Schmidt, sweeping source columns left to right.

The sweep keeps the populated basis columns and the finished coefficient columns in arrays and builds the two factor matrices once at the end. A dependent column does not consume a basis slot, so later independent columns can still enter. Each dot product and projection sums only active entries in their original order, starting from zero. Unused basis columns are zero and never introduce spurious 0 * NaN terms.

def TorchLean.Tensor.qr {α : Type} [Storage α] [Context α] {m n : ℕ} (matrix : Tensor α [m, n]) : QRFactors α m n

Compute a reduced QR factorization with classical Gram-Schmidt.

The result uses the NumPy/PyTorch reduced shapes q : Tensor α [m, min m n] and r : Tensor α [min m n, n]. For tall and square inputs, this is the specification computation with its dimensions presented in reduced form; its reconstruction and orthonormality theorems concern real scalars and require positive diagonal pivots. For wide inputs, linearly dependent source columns do not consume a basis column, so a later independent column can still enter the reduced basis. Any unused trailing basis columns are zero.

def TorchLean.Tensor.cholesky {α : Type} [Storage α] [Context α] {n : ℕ} (matrix : Tensor α [n, n]) : Tensor α [n, n]

Compute the lower-triangular Cholesky factor candidate of a square matrix.

For real symmetric inputs with positive pivots, the specification layer proves A = L @ L.transpose for its logical computation. Compilation substitutes an array implementation through implemented_by; equivalence to the logical computation is not proved. No exact reconstruction theorem is asserted for floating-point scalars. Inputs outside the intended domain follow the scalar backend's arithmetic behavior; for example, Float produces NaN after a negative square root.

def TorchLean.Tensor.solveRidge {α : Type} [Storage α] [Context α] {n : ℕ} (kernel : Tensor α [n, n]) (regularization : α) (target : Tensor α [n]) : Tensor α [n]

Solve (kernel + regularization * I) x = target through the Cholesky path.

The operation is intended for symmetric positive-semidefinite kernels and positive regularization. Its executable implementation is available across scalar backends supporting Context. The specification uses implemented_by substitutions for the compiled solve and Cholesky paths; their equivalence to the logical definitions is not proved.