Residual Convolutional Classifier

The model accepts any batchShape and spatial rank. Each residual stage chooses its own channel widths, convolution geometry, and shortcut. Global average pooling reduces every spatial axis before the classifier head.

inductive TorchLean.nn.models.ResNet.Shortcut (d : ℕ) : Type

The shortcut added to a residual stage's two-convolution branch.

• identity {d : ℕ} : Shortcut d

  Reuse the input unchanged; the branch must preserve its complete feature shape.

• projection {d : ℕ} (convolution : Convolution.Config d) : Shortcut d

  Project the input with a separately configured convolution.

structure TorchLean.nn.models.ResNet.Stage.Config (d : ℕ) : Type

Two convolutions with a ReLU between them, an explicit shortcut, and a final ReLU.

• first : Convolution.Config d

  First branch convolution; its stride may downsample the input grid.

• second : Convolution.Config d

  Second branch convolution.

• shortcut : Shortcut d

  Shortcut whose output must match the branch's channels and spatial grid.

def TorchLean.nn.models.ResNet.Stage.Config.outputSpatial {d : ℕ} (stage : Config d) (spatial : Tensor ℕ [d]) : Tensor ℕ [d]

Grid after both branch convolutions.

@[reducible, inline]

abbrev TorchLean.nn.models.ResNet.Stage.Config.outputShape {d : ℕ} (stage : Config d) (spatial : Tensor ℕ [d]) (batchShape : Shape := []) : Shape

Feature shape after adding the branch and shortcut.

def TorchLean.nn.models.ResNet.Stage.Config.validate {d : ℕ} (stage : Config d) (inputChannels : ℕ) (spatial : Tensor ℕ [d]) : Except String Unit

Check both branch convolutions and the explicit shortcut before allocating parameters.

structure TorchLean.nn.models.ResNet.Config (d : ℕ) : Type

Configuration for a residual classifier over d spatial axes.

• inputChannels : ℕ

  Number of channels in each input sample.

• spatial : Tensor ℕ [d]

  Size of each input axis. Values such as [32, 32] work directly.

• stem : Convolution.Config d

  Convolutional stem, followed by a ReLU.

• stages : List (Stage.Config d)

  Residual stages in execution order. An empty list pools the stem output directly.

• classCount : ℕ

  Number of classifier logits per sample.

def TorchLean.nn.models.ResNet.Config.validate {d : ℕ} (config : Config d) : Except String Unit

Validate the complete residual classifier before allocating any branch parameters.

def TorchLean.nn.models.ResNet.Config.validate.validateStages {d : ℕ} (channels : ℕ) (spatial : Tensor ℕ [d]) (stages : List (Stage.Config d)) : Except String Unit

@[reducible, inline]

abbrev TorchLean.nn.models.ResNet.Config.inputShape {d : ℕ} (config : Config d) (batchShape : Shape := []) : Shape

Input tensor shape with an arbitrary batch shape.

@[reducible, inline]

abbrev TorchLean.nn.models.ResNet.Config.outputShape {d : ℕ} (config : Config d) (batchShape : Shape := []) : Shape

Classifier output shape with the same batch shape as the input.

def TorchLean.nn.models.ResNet.Internal.buildStage {d : ℕ} (channels : ℕ) (spatial : Tensor ℕ [d]) (stage : Stage.Config d) (batchShape : Shape) : Builder (Sequential (batchShape.concat ((spatial.to Shape).prependDim channels)) (stage.outputShape spatial batchShape))

Build one stage, retaining the branch-first parameter and addition order.

def TorchLean.nn.models.resnet {d : ℕ} (config : ResNet.Config d) (batchShape : Shape := []) : Builder (Sequential (config.inputShape batchShape) (config.outputShape batchShape))

Build the configured stem and residual stages, then global pooling and a linear classifier.

def TorchLean.nn.models.resnet.buildStages {d : ℕ} (config : ResNet.Config d) (batchShape : Shape) (channels : ℕ) (spatial : Tensor ℕ [d]) (stages : List (ResNet.Stage.Config d)) : Builder (Sequential (batchShape.concat ((spatial.to Shape).prependDim channels)) (config.outputShape batchShape))