Logistic regression (spec model)

This file implements a small, deterministic logistic regression baseline.

Model (binary classification):

• logits: z = X w + b
• probabilities: p = σ(z) where σ is the logistic sigmoid

PyTorch analogue:

• parameters correspond to nn.Linear(p, 1) (weights + bias),
• probabilities correspond to torch.sigmoid(logits),
• training is a simple gradient-descent loop (similar to torch.optim.SGD), written in a simple, explicit style rather than tuned for performance.

Notes:

• We augment the input matrix with a column of ones to represent the intercept term.
• This is reference/spec code: it prioritizes clarity and auditability over performance.

Numerical note: PyTorch often uses BCEWithLogitsLoss for stability (it works directly on logits without forming sigmoid explicitly). Here we keep the math explicit.

Implementation status

No API builder implements this model, and no theorem is proved about it. It is a reference definition only.

structure LogisticRegression (p : ℕ) (α : Type) [TorchLean.Storage α] : Type

Parameters for logistic regression: a weight vector w and scalar intercept b.

We store intercept : α separately rather than folding it into weights, but fitLogistic internally learns (p + 1) parameters by augmenting the input with a trailing column of ones.

• weights : TorchLean.Tensor α [p]

  p-dimensional weight vector w.

• intercept : α

  Scalar intercept term b.

def augmentWithOnes {α : Type} [TorchLean.Storage α] [Context α] {n p : ℕ} (X : TorchLean.Tensor α [n, p]) : TorchLean.Tensor α [n, p + 1]

Augment an n × p design matrix with a final column of ones.

This lets us represent the affine model X w + b as a single matrix-vector product with a (p + 1)-vector of parameters.

def computeLogGradient {α : Type} [TorchLean.Storage α] [Context α] {n p : ℕ} (X : TorchLean.Tensor α [n, p + 1]) (y : TorchLean.Tensor α [n]) (w : TorchLean.Tensor α [p + 1]) : TorchLean.Tensor α [p + 1]

Gradient of the logistic negative log-likelihood, expressed as Xᵀ (σ(Xw) - y).

This is the standard expression used for (unregularized) logistic regression under labels y ∈ {0,1}. We do not divide by n here; callers can rescale if they want the mean loss.

inductive LogisticRegression.FitError : Type

A training label outside the binary encoding expected by logistic regression.

• invalidLabel (row : ℕ) : FitError

  The zero-based row whose label is neither 0 nor 1.

@[instance_reducible]

instance LogisticRegression.instReprFitError : Repr FitError

def LogisticRegression.instReprFitError.repr : FitError → ℕ → Std.Format

def LogisticRegression.instBEqFitError.beq : FitError → FitError → Bool

@[instance_reducible]

instance LogisticRegression.instBEqFitError : BEq FitError

def fitLogistic {α : Type} [TorchLean.Storage α] [Context α] {n p : ℕ} (X : TorchLean.Tensor α [n, p]) (y : TorchLean.Tensor α [n]) (learningRate : α) (iterations : ℕ) : Except LogisticRegression.FitError (LogisticRegression p α)

Fit binary logistic regression, checking the label encoding before any gradient step.

Each target must equal 0 or 1 under the scalar context's equality operation. In particular, signed SVM labels and soft targets are rejected here. The lower-level computeLogGradient remains the explicit mathematical expression for callers studying other target conventions.

The objective is a sum over observations, so duplicating the dataset doubles the gradient. An empty dataset has zero gradient and returns the zero initial parameters.

def fitLogistic.gradientDescent {α : Type} [TorchLean.Storage α] [Context α] {n p : ℕ} (y : TorchLean.Tensor α [n]) (learningRate : α) (augmentedInputs : TorchLean.Tensor α [n, p + 1]) (iter : ℕ) (weights : TorchLean.Tensor α [p + 1]) : TorchLean.Tensor α [p + 1]

def LogisticRegression.predictProba {α : Type} [TorchLean.Storage α] [Context α] {batch p : ℕ} (model : LogisticRegression p α) (X : TorchLean.Tensor α [batch, p]) : TorchLean.Tensor α [batch]

Predict the probability of label 1 for each row of X.

Only the number of features must agree with the fitted weights. The prediction batch may have any number of rows; an empty batch returns an empty probability tensor.

def LogisticRegression.predict {α : Type} [TorchLean.Storage α] [Context α] {batch p : ℕ} (model : LogisticRegression p α) (X : TorchLean.Tensor α [batch, p]) (threshold : α := 1 / 2) : TorchLean.Tensor α [batch]

Predict binary labels for a batch, using 0.5 as the default probability threshold.

A probability strictly above the threshold gives label 1; equality gives label 0. The inference batch may have any number of rows, independently of the training batch.

def LogisticRegression.predictProbaOne {α : Type} [TorchLean.Storage α] [Context α] {p : ℕ} (model : LogisticRegression p α) (x : TorchLean.Tensor α [p]) : α

Predict the probability of label 1 for one feature vector.

This uses the one-row batch operation, so its scalar arithmetic and rounding order agree with predictProba on the same observation.

def LogisticRegression.predictOne {α : Type} [TorchLean.Storage α] [Context α] {p : ℕ} (model : LogisticRegression p α) (x : TorchLean.Tensor α [p]) (threshold : α := 1 / 2) : α

Predict one binary label, with the same threshold and tie rule as predict.