Convolution Specifications

This file defines channels-first convolution and transpose convolution over an arbitrary spatial rank. The core specification handles one sample; batched interfaces map it over their leading dimensions.

PyTorch analogy: the grouped, dilated core corresponds to torch.nn.Conv{d}d with:

• arbitrary positive groups,
• per-axis dilation and stride,
• independent zero padding before and after each spatial axis,
• and the usual output-size formula (floor division, like PyTorch):

For each axis a : Fin d:

out[a] = (in[a] + 2*padding[a] - kernel[a]) / stride[a] + 1

The weight tensor has shape (outC × inC × kernel[0] × ... × kernel[d-1]) and the bias has shape (outC).

Implementation notes:

• Convolution uses natural nested loops (outer axes first) and one foldl accumulator. This fixes an explicit evaluation order for executable scalar models.
• Padding semantics are implemented via getAtOrZero plus an explicit guard for the left/top/front padding region (to avoid negative indices, which Nat cannot represent).

Index helpers

def Spec.Conv.Internal.foldlIndices {β : Type} (dims : List ℕ) (init : β) (f : β → List ℕ → β) : β

Fold over every coordinate of the rectangular index box dims.

Convolution sums over a kernel whose rank is a variable, so the sum is a fold over a list of extents rather than nested Fin loops. The pooling spec has its own copy for the same reason; keeping them apart lets each one use the index order its own definitions were written against.

def Spec.Conv.Internal.mkInputIdx? (outIdx kIdx stride padding : List ℕ) : Option (List ℕ)

Given:

• an output index tuple outIdx,
• a kernel index tuple kIdx,
• per-axis stride and padding, compute the corresponding input index tuple (into the unpadded input), or return none if we are in the left/top/front padding region on some axis.

Right/bottom/back padding is handled by getAtOrZero when the computed index is out of bounds.

def Spec.Conv.Internal.mkDilatedInputIdx? (outIdx kIdx stride dilation paddingBefore : List ℕ) : Option (List ℕ)

Convolution input-index map with per-axis dilation.

theorem Spec.Conv.Internal.mkDilatedInputIdx?_replicate_one (outIdx kernelIdx stride padding : List ℕ) : mkDilatedInputIdx? outIdx kernelIdx stride (List.replicate stride.length 1) padding = mkInputIdx? outIdx kernelIdx stride padding

Unit dilation reduces the dilated convolution index map to the dense index map.

def Spec.Conv.Internal.mkTransposeInputIdx? (outIdx kIdx stride padding : List ℕ) : Option (List ℕ)

Given:

• an output index tuple outIdx,
• a kernel index tuple kIdx,
• per-axis stride and padding, compute the corresponding input index tuple for transpose convolution, or none if the equality out + padding = in * stride + k cannot be satisfied on some axis.

Implementation detail: for each axis we solve

in = (out + padding - k) / stride

and require divisibility (% stride = 0) plus out + padding ≥ k. Out-of-bounds input indices are handled by getAtOrZero at the call site.

def Spec.Conv.Internal.matchesInputPos (outIdx kIdx stride padding inIdx : List ℕ) : Bool

Whether an output coordinate and kernel offset land on a given input coordinate.

The per-axis condition is out * stride + k = in + padding, which is the correlation index relation PyTorch implements. Writing it as a decidable test on coordinate lists is what makes the gradient specs sums over "the taps that hit this input" without inverting the relation.

Spec definition

structure Spec.ConvSpec (d inC outC : ℕ) (kernel stride padding : TorchLean.Tensor ℕ [d]) (α : Type) [TorchLean.Storage α] : Type

Parameters for an arbitrary-rank dense convolution, in channels-first layout.

• kernel : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

  Kernel weights, shape (outC, inC, kernel[0], ..., kernel[d-1]).

• bias : TorchLean.Tensor α [outC]

  Bias, shape (outC).

def Spec.convOutSpatialDilated {d : ℕ} (inSpatial kernel stride dilation paddingBefore paddingAfter : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Output spatial sizes for grouped/dilated convolution with asymmetric zero padding.

def Spec.convOutSpatial {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Output spatial sizes, one extent for each spatial axis.

@[simp]

theorem Spec.convOutSpatialDilated_one_symmetric {d : ℕ} (input kernel stride padding : TorchLean.Tensor ℕ [d]) : convOutSpatialDilated input kernel stride (TorchLean.Tensor.full [d] 1) padding padding = convOutSpatial input kernel stride padding

Dilated convolution geometry reduces to the symmetric, unit-dilation case.

theorem Spec.convOutSpatial_unit {d : ℕ} (spatial : TorchLean.Tensor ℕ [d]) : convOutSpatial spatial (TorchLean.Tensor.full [d] 1) (TorchLean.Tensor.full [d] 1) (TorchLean.Tensor.full [d] 0) = spatial

A unit kernel with unit stride and no padding preserves every spatial extent.

theorem Spec.convOutSpatial_same {d : ℕ} (spatial radius : TorchLean.Tensor ℕ [d]) : convOutSpatial spatial (TorchLean.Tensor.map (fun (p : ℕ) => 2 * p + 1) radius) (TorchLean.Tensor.full [d] 1) radius = spatial

Unit-stride convolution with an odd kernel and padding equal to the kernel radius preserves every spatial extent.

def Spec.convOutShape {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Shape

Output spatial shape Shape.ofList [out0, ..., out(d-1)].

def Spec.convMultiOutShape {d : ℕ} (_inC outC : ℕ) (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Shape

Output shape including channels: Shape.ofList (outC :: [out0, ..., out(d-1)]).

def Spec.Conv.Internal.convCoreWith {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel inSpatial outSpatial : TorchLean.Tensor ℕ [d]} (channelsPerOutput : ℕ) (inputChannel : Fin outC → Fin channelsPerOutput → ℕ) (inputIndex? : List ℕ → List ℕ → Option (List ℕ)) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data outSpatial).toList))

The grouped bilinear contraction shared by arbitrary-rank convolutions.

def Spec.groupedConvCoreSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

The grouped, dilated contraction for an arbitrary-rank convolution, with weights in the block-diagonal dense layout (outC, inC, k...).

Output channel oc belongs to group oc / (outC / groups) and reads only the input channels of that group, so only the block-diagonal part of weights is ever consulted. PyTorch stores grouped weights packed as (outC, inC / groups, k...); use groupedConvPackedCoreSpec for that layout, or groupedConvDenseWeights to expand a packed tensor into this one.

The definition is total. It is meaningful only when groups ∣ inC and groups ∣ outC; otherwise the trailing inC % groups input channels are never read. groups = 0 reads no channels at all.

def Spec.Conv.Internal.groupedConvCoreWith {α : Type} [TorchLean.Storage α] [Context α] {d inC outC weightC : ℕ} {kernel inSpatial outSpatial : TorchLean.Tensor ℕ [d]} (channelsPerOutput : ℕ) (inputChannel : Fin outC → Fin channelsPerOutput → ℕ) (inputIndex? : List ℕ → List ℕ → Option (List ℕ)) (weights : TorchLean.Tensor α (Shape.ofList (outC :: weightC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data outSpatial).toList))

The grouped bilinear contraction with weights packed per group, so that the channel axis of weights is indexed by the position of an input channel inside its group rather than by the global input channel.

def Spec.groupedConvPackedCoreSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC / groups :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

The grouped, dilated contraction with weights in PyTorch's packed layout (outC, inC / groups, k...), which is how torch.nn.Conv{1,2,3}d(groups=g).weight is stored.

Output channel oc belongs to group g = oc / (outC / groups) and reads input channels g * (inC / groups) + j for j < inC / groups, weighting each by weights[oc, j, k...].

The definition is total but only meaningful when groups ∣ inC and groups ∣ outC. When the divisibility fails the trailing inC % groups input channels are never read, and groups = 0 reads no channels at all (the output is then the bias alone once it is added).

def Spec.groupedConvDenseWeights {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC / groups :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

Expand packed grouped weights (outC, inC / groups, k...) into the block-diagonal dense layout (outC, inC, k...) read by groupedConvCoreSpec and groupedConvSpec.

Entry [oc, ic, k...] is weights[oc, ic - g * (inC / groups), k...] when input channel ic lies in the group g of output channel oc, and 0 otherwise. This is the remap a PyTorch checkpoint needs before it can be fed to the dense-layout grouped convolution.

def Spec.convCoreSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

The bilinear kernel/input contraction underlying an arbitrary-rank dense convolution.

theorem Spec.castShape_groupedConvCoreSpec_one_symmetric {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : (groupedConvCoreSpec 1 weights input).castShape ⋯ = convCoreSpec weights input

The grouped convolution contraction reduces to dense convolution for one group, unit dilation, and symmetric padding. The explicit cast transports the dilated output shape across the geometric specialization theorem.

def Spec.Conv.Internal.convBiasBroadcastWith {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} (outSpatial : TorchLean.Tensor ℕ [d]) (bias : TorchLean.Tensor α [outC]) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data outSpatial).toList))

Broadcast one channel value over a supplied spatial shape.

def Spec.convBiasBroadcastSpec {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

Broadcast a convolution bias over every output spatial position.

def Spec.convBiasBroadcastDilatedSpec {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

Add a channel bias to a dilated convolution output.

theorem Spec.castShape_convBiasBroadcastDilatedSpec_one_symmetric {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (bias : TorchLean.Tensor α [outC]) : (convBiasBroadcastDilatedSpec bias).castShape ⋯ = convBiasBroadcastSpec bias

Dilated-output bias broadcasting reduces to dense bias broadcasting in the symmetric case.

def Spec.groupedConvSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (bias : TorchLean.Tensor α [outC]) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

Numerical semantics for grouped, dilated convolution with asymmetric zero padding, with weights in the block-diagonal dense layout (outC, inC, k...).

This is the entry point used by the IR evaluator and the lowering passes, whose payloads carry a dense ConvSpec kernel. PyTorch checkpoints store grouped weights packed as (outC, inC / groups, k...); either expand them with groupedConvDenseWeights or use groupedConvPackedSpec directly. Both forms assume groups ∣ inC and groups ∣ outC.

def Spec.groupedConvPackedSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride dilation paddingBefore paddingAfter inSpatial : TorchLean.Tensor ℕ [d]} (groups : ℕ) (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC / groups :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (bias : TorchLean.Tensor α [outC]) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatialDilated inSpatial kernel stride dilation paddingBefore paddingAfter)).toList))

Grouped, dilated convolution with asymmetric zero padding and PyTorch's packed weight layout (outC, inC / groups, k...).

PyTorch analogue: torch.nn.functional.conv{1,2,3}d(input, weight, bias, stride, padding, dilation, groups) on one unbatched sample, with weight used as stored. The divisibility requirement groups ∣ inC ∧ groups ∣ outC is documented on groupedConvPackedCoreSpec.

def Spec.convSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

Arbitrary-rank dense convolution on a single channels-first input (no batch dimension).

Mathematically, for output channel oc and output spatial index o : Tensor Nat [d]:

y[oc,o] = Σ_{ic, k} x_pad[ic, o*stride + k] * W[oc,ic,k] + b[oc]

where k ranges over the kernel window and x_pad is input with zero-padding.

theorem Spec.castShape_groupedConvSpec_one_symmetric {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (bias : TorchLean.Tensor α [outC]) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : (groupedConvSpec 1 weights bias input).castShape ⋯ = convSpec { kernel := weights, bias := bias } input

Grouped convolution reduces to dense convolution for its canonical dense configuration.

def Spec.convJvpSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer tangentLayer : ConvSpec d inC outC kernel stride padding α) (input tangentInput : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))

Directional derivative formula for convolution in its kernel, bias, and input arguments.

def Spec.convKernelDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (_layer : ConvSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

Gradient of convolution output w.r.t. the kernel weights (given gradOutput).

def Spec.convBiasDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (_layer : ConvSpec d inC outC kernel stride padding α) (_input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α [outC]

Gradient of convolution output w.r.t. the bias (sum over spatial positions).

def Spec.convInputDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvSpec d inC outC kernel stride padding α) (_input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Gradient of convolution output w.r.t. the input (the "input-gradient" / transpose-convolution map).

This is stated once for arbitrary spatial rank d; there are no rank-specific variants.

structure Spec.ConvGradients (α : Type) [TorchLean.Storage α] (kernelShape biasShape inputShape : Shape) : Type

Named reverse-mode result of a convolution.

The three gradients used to travel as a bare triple. Every caller then opened it with a positional let (dK, dB, dX) := ..., and the adjoint theorem had to project the components out by position, which made a three-term equation hard to check against the sentence describing it. Affine normalization already returns a named NormalizationGradients; this is the same idea one layer over.

• kernelGradient : TorchLean.Tensor α kernelShape

  Gradient with respect to the kernel weights.

• biasGradient : TorchLean.Tensor α biasShape

  Gradient with respect to the per-output-channel bias.

• inputGradient : TorchLean.Tensor α inputShape

  Gradient with respect to the layer input.

def Spec.instReprConvGradients.repr {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {kernelShape✝ biasShape✝ inputShape✝ : Shape} [Repr α✝] : ConvGradients α✝ kernelShape✝ biasShape✝ inputShape✝ → ℕ → Std.Format

@[instance_reducible]

instance Spec.instReprConvGradients {α✝ : Type} {inst✝ : TorchLean.Storage α✝} {kernelShape✝ biasShape✝ inputShape✝ : Shape} [Repr α✝] : Repr (ConvGradients α✝ kernelShape✝ biasShape✝ inputShape✝)

def Spec.convBackwardSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convOutSpatial inSpatial kernel stride padding)).toList))) : ConvGradients α (Shape.ofList (outC :: inC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList)) [outC] (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Convolution backward pass: the kernel, bias, and input gradients under their own names.

Transpose convolution

structure Spec.ConvTransposeSpec (d inC outC : ℕ) (kernel stride padding : TorchLean.Tensor ℕ [d]) (α : Type) [TorchLean.Storage α] : Type

Parameters for an arbitrary-rank transpose convolution, in channels-first layout.

PyTorch analogy: this is torch.nn.ConvTranspose{d}d with:

• output_padding = 0,
• dilation = 1,
• groups = 1,
• per-axis stride and padding,
• and weight layout (inC, outC, k0, ..., k(d-1)).

• kernel : TorchLean.Tensor α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

  Kernel weights, shape (inC, outC, kernel[0], ..., kernel[d-1]).

• bias : TorchLean.Tensor α [outC]

  Bias, shape (outC).

def Spec.convTransposeOutDim (inDim kDim stride padding : ℕ) : ℕ

Output size along one transpose-convolution axis with output_padding = 0.

For positive input, kernel, and stride this is (input - 1) * stride + kernel - 2 * padding. A zero input, kernel, or stride is treated as an invalid axis and has size zero; excessive padding also saturates the final subtraction at zero. The addition precedes subtraction intentionally: Nat subtraction in (input - 1) * stride - 2 * padding + kernel does not represent the integer formula.

def Spec.convTransposeOutSpatial {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : TorchLean.Tensor ℕ [d]

Output spatial sizes (Tensor Nat [d]) for transpose convolution (output_padding = 0).

def Spec.convTransposeOutShape {d : ℕ} (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Shape

Output spatial shape Shape.ofList [out0, ..., out(d-1)] (transpose convolution).

def Spec.convTransposeMultiOutShape {d : ℕ} (_inC outC : ℕ) (inSpatial kernel stride padding : TorchLean.Tensor ℕ [d]) : Shape

Output shape including channels: Shape.ofList (outC :: [out0, ..., out(d-1)]).

def Spec.convTransposeSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvTransposeSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))

Arbitrary-rank transpose convolution on a single channels-first input (no batch dimension).

For output channel oc and output spatial index o : Tensor Nat [d] we define:

y[oc,o] = Σ_{ic, k} x[ic, (o + padding - k) / stride] * W[ic,oc,k] + b[oc]

where each axis must satisfy out + padding ≥ k and divisibility by stride (% stride = 0).

def Spec.convTransposeKernelDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))

Gradient of transpose convolution output w.r.t. the kernel weights (given gradOutput).

def Spec.convTransposeBiasDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α [outC]

Gradient of transpose convolution output w.r.t. the bias (sum over spatial positions).

def Spec.convTransposeInputDerivSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (weights : TorchLean.Tensor α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Gradient of transpose convolution output w.r.t. the input (given gradOutput).

def Spec.convTransposeBackwardSpec {α : Type} [TorchLean.Storage α] [Context α] {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : ConvTransposeSpec d inC outC kernel stride padding α) (input : TorchLean.Tensor α (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))) (gradOutput : TorchLean.Tensor α (Shape.ofList (outC :: (TorchLean.Tensor.Internal.Rep.data (convTransposeOutSpatial inSpatial kernel stride padding)).toList))) : ConvGradients α (Shape.ofList (inC :: outC :: (TorchLean.Tensor.Internal.Rep.data kernel).toList)) [outC] (Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList))

Transpose convolution backward pass, reported with the same named fields as the forward convolution's ConvGradients. Only the kernel layout differs: transpose weights are stored (inC, outC, ...).