Convolution

Arbitrary-rank convolution geometry and configuration records.

structure TorchLean.nn.Convolution.Geometry (d : ℕ) : Type

Kernel, stride, and padding shared by convolutional layers with different channel widths.

• kernelSize : Tensor ℕ [d]

  Kernel extent along each spatial axis.

• stride : Tensor ℕ [d]

  Step along each spatial axis.

• padding : Tensor ℕ [d]

  Symmetric zero-padding along each spatial axis.

def TorchLean.nn.Convolution.Geometry.outputSpatial {d : ℕ} (geometry : Geometry d) (input : Tensor ℕ [d]) : Tensor ℕ [d]

Output grid produced by this convolution geometry.

def TorchLean.nn.Convolution.Geometry.transposedOutputSpatial {d : ℕ} (geometry : Geometry d) (input : Tensor ℕ [d]) : Tensor ℕ [d]

Output grid produced when this geometry is used for transpose convolution.

def TorchLean.nn.Convolution.Geometry.samePadding {d : ℕ} (radius : Tensor ℕ [d]) : Geometry d

Unit-stride geometry with an odd kernel along each axis and padding equal to the kernel radius.

theorem TorchLean.nn.Convolution.Geometry.outputSpatial_samePadding {d : ℕ} (input radius : Tensor ℕ [d]) : (samePadding radius).outputSpatial input = input

Same-padding geometry preserves every input extent.

structure TorchLean.nn.Convolution.Config (d : ℕ) : Type

Configuration shared by arbitrary-dimensional convolution layers.

• outChannels : ℕ

  Number of output channels. Must be positive when the layer is validated.

• kernelSize : Tensor ℕ [d]

  Kernel extent along each spatial axis.

• stride : Tensor ℕ [d]

  Step along each spatial axis.

• padding : Tensor ℕ [d]

  Symmetric zero-padding along each spatial axis.

• weightInitialization : Init.Scheme

  Initialization scheme for the kernel weights.

def TorchLean.nn.Convolution.Config.outputSpatial {d : ℕ} (config : Config d) (input : Tensor ℕ [d]) : Tensor ℕ [d]

Output grid produced from an input grid by this convolution configuration.

def TorchLean.nn.Internal.validateConvolution {d : ℕ} (inputChannels outputChannels : ℕ) (input kernelSize stride output : Tensor ℕ [d]) (initialization : Init.Scheme) (kind : String) : Except String Unit

Shared convolution checks using the output geometry computed by the caller.

def TorchLean.nn.Convolution.Config.validate {d : ℕ} (config : Config d) (inputChannels : ℕ) (input : Tensor ℕ [d]) (kind : String := "Conv") : Except String Unit

Validate channel widths, spatial geometry, and kernel initialization.

def TorchLean.nn.Convolution.Geometry.convolution {d : ℕ} (geometry : Geometry d) (outChannels : ℕ) : Config d

Build a convolution configuration by adding an output-channel width to shared geometry.

@[simp]

theorem TorchLean.nn.Convolution.Geometry.convolution_outChannels {d : ℕ} (geometry : Geometry d) (outChannels : ℕ) : (geometry.convolution outChannels).outChannels = outChannels

Adding an output width to a geometry keeps that width.

@[simp]

theorem TorchLean.nn.Convolution.Geometry.convolution_outputSpatial {d : ℕ} (geometry : Geometry d) (outChannels : ℕ) (input : Tensor ℕ [d]) : (geometry.convolution outChannels).outputSpatial input = geometry.outputSpatial input

The spatial grid is the geometry's, so a shape proof can be discharged from the geometry alone without unfolding the configuration the builder produced.

structure TorchLean.nn.TransposedConvolution.Config (d : ℕ) : Type

Configuration shared by arbitrary-dimensional transposed-convolution layers.

• outChannels : ℕ

  Number of output channels. Must be positive when the layer is validated.

• kernelSize : Tensor ℕ [d]

  Kernel extent along each spatial axis.

• stride : Tensor ℕ [d]

  Step along each spatial axis.

• padding : Tensor ℕ [d]

  Symmetric zero-padding along each spatial axis.

• weightInitialization : Init.Scheme

  Initialization scheme for the kernel weights.

def TorchLean.nn.TransposedConvolution.Config.outputSpatial {d : ℕ} (config : Config d) (input : Tensor ℕ [d]) : Tensor ℕ [d]

Output grid produced from an input grid by this transpose-convolution configuration.

def TorchLean.nn.TransposedConvolution.Config.validate {d : ℕ} (config : Config d) (inputChannels : ℕ) (input : Tensor ℕ [d]) (kind : String := "ConvTranspose") : Except String Unit

Validate channel widths, spatial geometry, and kernel initialization.

def TorchLean.nn.Convolution.Geometry.transposedConvolution {d : ℕ} (geometry : Geometry d) (outChannels : ℕ) : TransposedConvolution.Config d

Build a transpose-convolution configuration from shared geometry.

@[simp]

theorem TorchLean.nn.Convolution.Geometry.transposedConvolution_outChannels {d : ℕ} (geometry : Geometry d) (outChannels : ℕ) : (geometry.transposedConvolution outChannels).outChannels = outChannels

Same for the transpose direction: the requested output width survives.

@[simp]

theorem TorchLean.nn.Convolution.Geometry.transposedConvolution_outputSpatial {d : ℕ} (geometry : Geometry d) (outChannels : ℕ) (input : Tensor ℕ [d]) : (geometry.transposedConvolution outChannels).outputSpatial input = geometry.transposedOutputSpatial input

Reusing one geometry for both directions is only sound if each direction keeps its own output rule, and it does: the transpose configuration's grid is Geometry.transposedOutputSpatial, never the forward Geometry.outputSpatial.