Linear layer (spec layer)

This file defines a fully‑connected layer and its gradients:

• forward: y = W x + b
• backward: ∂L/∂W, ∂L/∂b, ∂L/∂x

Definitions are purely functional and shape‑indexed, suitable for both proofs and reuse by autograd wrappers in NN/Spec/Autograd.

structure Spec.LinearSpec (α : Type) [TorchLean.Storage α] (inDim outDim : ℕ) : Type

Linear layer specification (pure, shape-indexed).

This is the spec-level analogue of PyTorch torch.nn.Linear / torch.nn.functional.linear:

• weights has shape [outDim, inDim],
• bias has shape [outDim].

• weights : TorchLean.Tensor α [outDim, inDim]

  Weight matrix with rows indexed by output features.

• bias : TorchLean.Tensor α [outDim]

  Bias vector added to each output feature.

def Spec.linearSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {inDim outDim : ℕ} (m : LinearSpec α inDim outDim) (input : TorchLean.Tensor α [inDim]) : TorchLean.Tensor α [outDim]

Unbatched forward pass: y = W x + b.

PyTorch analogue: torch.nn.functional.linear.

def Spec.linearWeightsDerivSpec {α : Type} [TorchLean.Storage α] [Mul α] {inDim outDim : ℕ} (input : TorchLean.Tensor α [inDim]) (gradOutput : TorchLean.Tensor α [outDim]) : TorchLean.Tensor α [outDim, inDim]

Gradient w.r.t. weights: ∂L/∂W = (∂L/∂y) ⊗ x (outer product).

This is the standard linear-layer backward formula for y = W x + b.

def Spec.linearBiasDerivSpec {α : Type} [TorchLean.Storage α] {inDim outDim : ℕ} (_dW : TorchLean.Tensor α [outDim, inDim]) (gradOutput : TorchLean.Tensor α [outDim]) (_input : TorchLean.Tensor α [inDim]) : TorchLean.Tensor α [outDim]

Gradient w.r.t. bias: ∂L/∂b = ∂L/∂y.

Since y = W x + b, the Jacobian of y w.r.t. b is the identity.

def Spec.linearInputDerivSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {inDim outDim : ℕ} (weights : TorchLean.Tensor α [outDim, inDim]) (gradOutput : TorchLean.Tensor α [outDim]) : TorchLean.Tensor α [inDim]

Gradient w.r.t. input: ∂L/∂x = Wᵀ (∂L/∂y).

This is the standard "matmul by the transpose" rule for y = W x + b.

structure Spec.LinearParameterGradients (α : Type) [TorchLean.Storage α] (inDim outDim : ℕ) : Type

Gradients for the parameters of a linear layer y = W x + b.

LinearSpec stores weights and bias, so this bundle names its fields the same way with a Gradient suffix. The LSTM output head in NN/Spec/Module/LstmModels.lean and the seq2seq decoder projection in NN/Spec/Models/Seq2seq.lean each used to declare a private copy of exactly this record, which meant a gradient produced by one model could not be read by code written against the other. One shared record fixes that.

PyTorch analogue: (layer.weight.grad, layer.bias.grad) for torch.nn.Linear.

• weightGradient : TorchLean.Tensor α [outDim, inDim]

  Gradient with respect to the weight matrix W.

• biasGradient : TorchLean.Tensor α [outDim]

  Gradient with respect to the bias vector b.

@[instance_reducible]

instance Spec.instReprLinearParameterGradients {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {inDim✝ outDim✝ : ℕ} [Repr α✝] : Repr (LinearParameterGradients α✝ inDim✝ outDim✝)

def Spec.instReprLinearParameterGradients.repr {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {inDim✝ outDim✝ : ℕ} [Repr α✝] : LinearParameterGradients α✝ inDim✝ outDim✝ → ℕ → Std.Format

structure Spec.LinearGradients (α : Type) [TorchLean.Storage α] (inDim outDim : ℕ) (inputShape : Shape) : Type

Everything a linear backward pass produces: the two parameter gradients, plus the gradient that keeps travelling backwards into the layer's input.

inputShape is a parameter because the same rule serves the unbatched case ([inDim]) and the batched one (leading.appendDim inDim). The three fields are spelled out rather than inherited from LinearParameterGradients: a structure that extends another prints its parent as a nested toLinearParameterGradients := ..., and these records get #eval'd in the guide, where a flat line is what a reader wants to compare against the formula. LinearGradients.parameters recovers the parameter pair for model-level gradient records.

Convolution returns its gradients the same way, as Spec.ConvGradients.

• weightGradient : TorchLean.Tensor α [outDim, inDim]

  Gradient with respect to the weight matrix W.

• biasGradient : TorchLean.Tensor α [outDim]

  Gradient with respect to the bias vector b.

• inputGradient : TorchLean.Tensor α inputShape

  Gradient with respect to the layer input.

@[instance_reducible]

instance Spec.instReprLinearGradients {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {inDim✝ outDim✝ : ℕ} {inputShape✝ : Shape} [Repr α✝] : Repr (LinearGradients α✝ inDim✝ outDim✝ inputShape✝)

def Spec.instReprLinearGradients.repr {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {inDim✝ outDim✝ : ℕ} {inputShape✝ : Shape} [Repr α✝] : LinearGradients α✝ inDim✝ outDim✝ inputShape✝ → ℕ → Std.Format

def Spec.LinearGradients.parameters {α : Type} [TorchLean.Storage α] {inDim outDim : ℕ} {inputShape : Shape} (gradients : LinearGradients α inDim outDim inputShape) : LinearParameterGradients α inDim outDim

Forget the input gradient and keep the two parameter gradients, which is what a model-level gradient record stores for a layer whose input gradient has already been consumed.

def Spec.linearDerivSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] [Inhabited α] {leading : Shape} {inDim outDim : ℕ} (hLeading : 0 < leading.size) (weights : TorchLean.Tensor α [outDim, inDim]) (input : TorchLean.Tensor α (leading.appendDim inDim)) (gradOutput : TorchLean.Tensor α (leading.appendDim outDim)) : LinearGradients α inDim outDim (leading.appendDim inDim)

Linear derivatives over any nonempty leading shape.

The leading axes are flattened only while accumulating the parameter gradients:

• d_weights = (gradOutputᵀ) · input,
• d_bias = sum(gradOutput) over every leading coordinate,
• d_input = gradOutput · weights.

def Spec.linearBackwardSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {inDim outDim : ℕ} (layer : LinearSpec α inDim outDim) (input : TorchLean.Tensor α [inDim]) (gradOutput : TorchLean.Tensor α [outDim]) : LinearGradients α inDim outDim [inDim]

Complete unbatched backward pass for a linear layer.

Returns ∂L/∂W, ∂L/∂b and ∂L/∂x given the layer params, input x, and output gradient ∂L/∂y.

def Spec.timeDistributedLinearBackward {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {seqLen inDim outDim : ℕ} (layer : LinearSpec α inDim outDim) (inputs : TorchLean.Tensor α [seqLen, inDim]) (gradOutputs : TorchLean.Tensor α [seqLen, outDim]) : LinearGradients α inDim outDim [seqLen, inDim]

Backward pass for a linear layer applied at every position of a sequence.

The layer is shared across positions, so its parameter gradients accumulate over the sequence while each position gets its own input gradient. This is the rule behind both the LSTM output head (Spec.Lstm.Model.backward) and the seq2seq decoder projection (Spec.Seq2SeqDecoderSpec.backwardTeacherForcing); those two files each carried a byte-identical copy of it under different binder names until the record above gave them a common vocabulary.

PyTorch analogue: backprop through nn.Linear applied inside a loop over timesteps, where weight.grad sums the per-step contributions.

def Spec.linearGradientAccumulateSpec {α : Type} [TorchLean.Storage α] [Add α] {inDim outDim : ℕ} (grad1 grad2 : TorchLean.Tensor α [outDim, inDim]) : TorchLean.Tensor α [outDim, inDim]

Accumulate two weight gradients by addition.

This is a small helper used by batching/training code.

def Spec.linearGradientScaleSpec {α : Type} [TorchLean.Storage α] [Mul α] {inDim outDim : ℕ} (grad : TorchLean.Tensor α [outDim, inDim]) (scaleFactor : α) : TorchLean.Tensor α [outDim, inDim]

Scale a weight gradient by a scalar factor (e.g. learning-rate adjustment).