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

structure TorchLean.Tensor.Internal.WideQRState (α : Type) [Storage α] (rows columns : ℕ) : Type

Tensor buffers and the active basis width of the Gram-Schmidt sweep.

• count : Fin (min rows columns + 1)

  Number of populated basis columns; remaining columns stay zero.

• basis : Tensor α [rows, min rows columns]

  Reduced basis matrix.

• coefficients : Tensor α [min rows columns, columns]

  Coefficients for the source columns processed so far.

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 basis and coefficient buffers keep their final tensor shapes; count selects the populated basis columns. 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 therefore 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 theorem-backed specification computation with its dimensions presented in reduced form. 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 symmetric inputs with positive executable pivots, the specification layer proves A = L @ L.transpose. Inputs outside that 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.